PROPOSITIONAL UNIVERSE

-type is the universe of propositions, 0-truncated types that represent logical statements with at most one proof. It is the foundation for logical reasoning and set predicates in this system.

In Schwartz’s framework, supports classical logic constructs like , , and , with Z3 verifying their truth.

Formation

(-Formation). The propositional universe classifies terms that are propositions, distinct from higher universes like .

type exp =
  | Prop  (* Prop *)

Introduction

(-Introduction). A proposition is introduced via logical constructs like , , , or inequalities, typed as .

let prop_leq (a : exp) (b : exp) : exp =
  RealIneq (Lte, a, b)

Elimination

(-Elimination). A term can be used in logical rules (e.g., modus ponens) or reduced to /.

let infer env ctx p =
  check env ctx p Prop; Prop

Computation

(-Computation). Propositions reduce via logical rules or Z3 verification, yielding or in decidable cases.

let reduce env ctx = function
  | RealIneq (Lte, RealNum a, RealNum b) -> if a <= b then True else False
  | p -> smt_verify_iff ctx_z3 p True

Uniqueness

(-Uniqueness). All proofs of a proposition are equal, due to 0-truncation, ensuring propositional extensionality.

let equal env ctx p q =
  check env ctx p Prop; check env ctx q Prop; true

Theorems

(Classical Logic). supports excluded middle: for any , , aligning with Z3’s classical reasoning.

(Set Predicate). A set is defined by a predicate , where .

let set_predicate (a : exp) (p : exp) =
  Set (Lam ("x", a, p))