SUPREMUM

-type computes the supremum of a set of real numbers, the least upper bound, essential for defining limits and integrals in analysis. It leverages the completeness of in this system.

In Schwartz’s framework, supports constructive and classical analysis, grounding properties like boundedness and convergence.

Formation

(-Formation). The supremum is defined over a set , yielding a real number.

type exp =
  | Sup of exp  (* Sup S *)

Introduction

(-Introduction). The supremum of a set is introduced as , assuming is non-empty and bounded above.

let sup_a : exp =
  Sup (Set (Lam ("x", Real, RealIneq (Gt, Var "x", Zero))))

Elimination

(-Elimination). The supremum serves as an upper bound, provable via its defining properties.

let upper_bound (s : exp) (sup_s : exp) =
  Forall ("x", Real, RealIneq (Lte, Var "x", sup_s))

Computation

(-Computation). The supremum does not reduce directly but is characterized by its least upper bound property, verifiable via Z3 for concrete sets.

let infer env ctx (Sup s) = check env ctx s (Set Real); Real

Uniqueness

(-Uniqueness). The supremum of a set is unique in , as any two least upper bounds must be equal.

let equal env ctx (Sup s1) (Sup s2) =
  equal env ctx s1 s2

Theorems

(Completeness). Every non-empty set of real numbers bounded above has a supremum in , ensured by this system’s design.

(Sequence Supremum). For a sequence , exists if the sequence is bounded above.

let seq_sup (s : exp) =
  Sup (Set (Lam ("x", Real,
    Exists ("n", Nat,
      RealIneq (Eq, Var "x",
        App (s, Var "n"))))))