# Ghilbert Pax # Interface file for predicate calculus param (PROP pax/prop () "") kind (type) kind (val) kind (var) var (wff ph ps ch) var (type T T') var (val A B C) var (var x y z) term (val (cv var)) term (wff (istype type)) term (wff (A. var type wff)) term (wff (= type val val)) # Basic predicate calculus axioms term (wff (nfi var type wff)) stmt (df-nfi ((T x)) () (<-> (nfi x T ph) (<-> ph (A. x T ph)))) stmt (nfi_dv ((ph x) (T x)) ((istype T)) (nfi x T ph)) stmt (nfi_bound ((T x)) ((istype T)) (nfi x T (A. x T ph))) stmt (nfi_not ((T x)) ((nfi x T ph) (istype T)) (nfi x T (-. ph))) stmt (nfi_im ((T x)) ((nfi x T ph) (nfi x T ps) (istype T)) (nfi x T (-> ph ps))) stmt (nfi_al ((T x y) (T' x)) ((nfi x T ph) (istype T) (istype T')) (nfi x T (A. y T' ph))) term (wff (E. var type wff)) stmt (df-ex ((T x)) () (<-> (E. x T ph) (-. (A. x T (-. ph))))) term (wff (: val type)) stmt (df-ty ((T x) (A x)) () (<-> (: A T) (E. x T (= T (cv x) A)))) stmt (gen ((T x)) ((istype T) (-> (: (cv x) T) ph)) (A. x T ph)) # Margaris A4 stmt (alim ((T x)) ((istype T)) (-> (A. x T (-> ph ps)) (-> (A. x T ph) (A. x T ps)))) # roughly Margaris A5, but without the subst stmt (spec-var ((T x)) ((istype T)) (-> (A. x T ph) (-> (: (cv x) T) ph))) stmt (eqcom () ((istype T)) (<-> (= T A B) (= T B A))) stmt (ax-eqtr () ((istype T)) (-> (/\ (= T A B) (= T B C)) (= T A C))) # Norm's ax-11 (actually strengthened to bi) stmt (ax-subst ((T x) (A x)) ((istype T)) (-> (: A T) (-> (= T (cv x) A) (<-> ph (A. x T (-> (= T (cv x) A) ph)))))) # Exists unique, definition from set.mm term (wff (E! var type wff)) stmt (df-eu ((T x) (ph y)) () (<-> (E! x T ph) (E. y T (A. x T (<-> ph (= T (cv x) (cv y))))))) term (val (iota var type wff)) stmt (iota-ax ((T x y) (ph y)) ((istype T)) (-> (E! x T ph) (E. y T (/\ (= T (cv y) (iota x T ph)) (E. x T (/\ (= T (cv x) (cv y)) ph)))))) # We've proved a guarded version of this, but this unguarded version should # be valid in all models. stmt (Nfi_iota_bound ((T x y) (ph y)) ((istype T)) (nfi x T (= T (cv y) (iota x T ph)))) stmt (Nfi_iota ((T x y z) (T' x y z) (ph y)) ((nfi x T ph) (istype T) (istype T')) (nfi x T (= T' (cv y) (iota z T' ph)))) # A weaker form, where E! x ph, should be provable from the main axiom. # But this form is far more convenient for making definitions. # In fact, this axiom is problematic in some models; specifically # those in which iota x ph may take the value of "bottom" when -. E! x # ph, and for which -. bottom = bottom. If it's ok to exclude such # models, then we might as well posit the reflexivity of equality (as # opposed to eqid, which is guarded by A:T). If it's not ok to exclude # such models, then we should get rid of this axiom and make all iota # definitions guarded by existential quantification. stmt (iota-alphaconvt ((T x y)) ((istype T) (nfi y T ph) (nfi x T ps)) (-> (A. x T (A. y T (-> (= T (cv x) (cv y)) (<-> ph ps)))) (= T (iota x T ph) (iota y T ps)))) # Useful defs that could be split off into their own interface; proof # fragments in pred-defs.gh term (wff (E* var type wff)) stmt (df-mo () () (<-> (E* x T ph) (-> (E. x T ph) (E! x T ph)))) term (wff ([:=] var type val wff)) stmt (df-subst ((T x z)) ((istype T)) (<-> ([:=] x T A ph) (E. z T (/\ (= T (cv z) A) (E. x T (/\ (= T (cv x) (cv z)) ph)))))) term (val (if type wff val val)) stmt (df-if ((T x) (A x) (B x) (ph x)) ((istype T)) (= T (if T ph A B) (iota x T (\/ (/\ (= T (cv x) A) ph) (/\ (= T (cv x) B) (-. ph))))))