PREDICATE-BASED SETS

-type defines a set as a predicate over a base type, capturing the classical notion of a collection via propositional conditions. It serves as the foundation for topology, measure theory, and real analysis in this system, blending type theory with set-theoretic intuition.

Sets are constructed as , where is a proposition, and are used to model intervals, measurable sets, and spaces in Schwartz’s framework.

Formation

(-Formation). A set is formed over a base type with a predicate , yielding a term-level set type.

type exp =
  | Set of exp  (* Set (Lam ("x", A, P(x))) *)

Introduction

(-Introduction). A set is introduced by a lambda abstraction , where defines membership for all .

let interval_a_b (a : exp) (b : exp) : exp =
  Set (Lam ("x", Real, And (RealIneq (Lte, a, Var "x"), RealIneq (Lte, Var "x", b))))

Elimination

(-Elimination). Membership in a set is tested by applying to an element , yielding the proposition .

let member (s : exp) (a : exp) : exp =
  App (s, a)  (* S a *)

Computation

(-Computation). Applying a set to an element reduces to the predicate with substitution.

let reduce env ctx = function
  | App (Set (Lam (x, _, body)), arg) -> subst x arg body
  | _ -> ...

Uniqueness

(-Uniqueness). Two sets and are equal if their predicates are propositionally equivalent, i.e., .

(* Handled by SetEq and Z3 *)

Theorems

(Set Comprehension). Any predicate defines a valid set , with membership .

(Power Set). The power set of a type is the set of all subsets, represented as .

let power (a : exp) : exp = Power a