LOGICAL DISJUNCTION

-type represents logical disjunction, combining two propositions into a single proposition that holds if at least one is true. It supports set unions and alternative conditions in this system.

In Schwartz’s framework, defines union predicates and closure properties, with Z3 ensuring logical consistency.

Formation

(-Formation). Disjunction is formed over two propositions , yielding their logical "or".

type exp =
  | Or of exp * exp  (* P ∨ Q *)

Introduction

(-Introduction). Disjunction is introduced by providing a proof of either or .

let disj (p : exp) (q : exp) : exp =
  Or (p, q)

Elimination

(-Elimination). From and proofs that and , one derives , reflecting classical disjunction.

let or_elim (p_or_q : exp) (p_to_r : exp) (q_to_r : exp) : exp =
  match p_or_q with
  | Or (p, q) -> If (p, p_to_r, q_to_r)
  | _ -> ...

Computation

(-Computation). Disjunction reduces to if either or is , verifiable by Z3.

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

Uniqueness

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

let equal env ctx (Or (p1, q1)) (Or (p2, q2)) =
  equal env ctx p1 p2 && equal env ctx q1 q2

Theorems

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

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

let union_member (s : exp) (t : exp) (x : exp) =
  Or (App (s, x), App (t, x))