LOGICAL CONJUNCTION

-type represents logical conjunction, combining two propositions into a single proposition that holds if both are true. It is a building block for predicate definitions and set operations in this system.

In Schwartz’s framework, underpins interval definitions and compound conditions, with Z3 ensuring propositional consistency.

Formation

(-Formation). Conjunction is formed over two propositions , yielding their logical "and".

type exp =
  | And of exp * exp  (* P ∧ Q *)

Introduction

(-Introduction). Conjunction is introduced by providing proofs of both and .

let conj (p : exp) (q : exp) : exp =
  And (p, q)

Elimination

(-Elimination). From , one can derive or individually, reflecting classical conjunction rules.

let fst_conj (p : exp) = match p with
  | And (p1, _) -> p1
  | _ -> ...
let snd_conj (p : exp) = match p with
  | And (_, p2) -> p2
  | _ -> ...

Computation

(-Computation). Conjunction reduces to if both and are , otherwise , verifiable by Z3.

let reduce env ctx = function
  | And (True, True) -> True
  | And (p, q) -> smt_verify_iff ctx_z3 (And (p, q)) True
  | _ -> ...

Uniqueness

(-Uniqueness). As a proposition, is unique in , with all proofs equal due to 0-truncation.

Theorems

(Commutativity). Conjunction is commutative: , provable by logical equivalence.

(Intersection Definition). For sets , membership in is defined as , using .

let intersect_member (s : exp) (t : exp) (x : exp) =
  And (App (s, x), App (t, x))