EXISTENTIAL QUANTIFICATION

-type represents existential quantification, encoding the existence of a witness satisfying a property . It is a dependent sum, interpreted as a coproduct or disjoint union, truncated to a proposition.

In this system, -types are foundational for defining sets, measures, and classical logical statements, aligning with Schwartz’s analysis framework.

Formation

(-Formation, Dependent Sum). The existential type is indexed over a type with a family , formed as a 0-truncated dependent sum.

type exp =
  | Exists of string * exp * exp  (* ∃ (x : A), B(x) *)

Introduction

(Witness Pair). A pair where and introduces a term proving .

let pair (a : exp) (b : exp) : exp =
  Pair (a, b)  (* (a, b) *)

Elimination

(Projections). The projections and extract the witness and proof from an existential term.

let fst (p : exp) : exp = Fst p  (* p.1 *)
let snd (p : exp) : exp = Snd p  (* p.2 *)

Computation

(-Computation). The β-rules for projections reduce pairs to their components.

let reduce env ctx = function
  | Fst (Pair (a, _)) -> a
  | Snd (Pair (_, b)) -> b
  | _ -> ...

Uniqueness

(-Uniqueness). As a proposition, is 0-truncated, so any two proofs are equal up to propositional equality.

(* Implicit in Prop truncation *)
let equal env ctx p q = true  (* For Prop terms *)

Theorems

(Classical Logic). If holds, there exists some such that is true, validated by Z3 reduction.

(Axiom of Choice). If for all there exists such that , then a choice function exists.

let ac (a : exp) (b : exp) (r : exp) =
  Exists ("f", Forall ("x", a, Exists ("y", b, r)),
        Forall ("x", a, r))