SET COMPLEMENT

-type constructs the complement of a set with respect to its base type, defining elements not in the original set via predicate negation. It is crucial for -algebra closure and measure theory operations.

In this system, integrates with and , using logical negation and Z3 to ensure consistency in set definitions.

Formation

(-Formation). The complement of a set with respect to forms a new set of elements not in .

type exp =
  | Complement of exp * exp  (* A \ S *)

Introduction

(-Introduction). The complement of in is introduced as .

let complement_set (a : exp) (s : exp) : exp =
  Complement (a, s)

Elimination

(-Elimination). Membership in holds if an element is in but not in , expressed as negation.

let reduce env ctx = function
  | App (Complement (_, Set (Lam (x, _, p))), a) ->
      Not (subst x a p)
  | _ -> ...

Computation

(-Computation). Applying to an element reduces to the negation of ’s predicate, verifiable by Z3 for concrete cases.

let infer env ctx (Complement (a, s)) =
  check env ctx s (Set a); Set a

Uniqueness

(-Uniqueness). The complement is uniquely determined by its predicate, equal to another set if , provable via .

let equal env ctx (Complement (a1, s1)) (Complement (a2, s2)) =
  equal env ctx a1 a2 && equal env ctx s1 s2

Theorems

(Double Complement). For a set , the double complement equals the original set: .

(Measure of Complement). For a measure with finite total measure , , assuming .

let measure_complement (mu : exp) (a : exp) (s : exp) =
  SetEq (App (mu, Complement (a, s)),
         RealOps (Minus, App (mu, a), App (mu, s)))