# Experimental interface for Peano arithmetic
# We conjecture the following properties about this interface, with at
# this point only a moderate amount of confidence:
#
# * It encapsulates PA soundly and completely.
# * It is possible to interpret in a set.mm universe.
# * It is reasonably useful.
#
# There are two extensions that may improve usefulness: classes and
# ax-11. The latter would enable a substitution operator with all the
# expected properties. However, it makes the syntactic interpretation
# in set.mm problematic.
param (PROP prop.ghi () "")
param (PEANO_MIN peano_min.ghi (PROP) "")
tvar (wff ph ps ch)
tvar (nat A B C D)
var (nat x y z)
# Definition of exists - could be done through def instead of axiom here.
term (wff (E. x ph))
## Definition of ∃
## right('Equivalence', '∀')
stmt (df-ex () () (<-> (E. x ph) (-. (A. x (-. ph)))))
# Exists-unique is handy for iota def, but could be expanded there
term (wff (E! x ph))
stmt (df-eu ((ph y)) ()
(<-> (E! x ph) (E. y (A. x (<-> ph (= x y))))))
term (nat (1))
stmt (df-1 () () (= (1) (S (0))))
# Definition of less than or equal to.
term (wff (<= A B))
stmt (df-le ((A x) (B x)) ()
(<-> (<= A B) (E. x (= (+ A x) B))))
term (wff (< A B))
stmt (df-lt () ()
(<-> (< A B) (/\ (<= A B) (-. (= A B)))))
term (wff ([/] A x ph) (x A))
stmt (df-subst ((A z) (ph z)) ()
(<-> ([/] A x ph) (E. z (/\ (= z A) (E. x (/\ (= x z) ph))))))
term (wff (rwff x ph))
stmt (df-rwff () ()
(<-> (rwff x ph) (A. x (<-> ph ([/] x x ph)))))
# iota is a draft at this point.
# term (nat (iota x ph))
#stmt (ax-iota ((ph y)) ()
# (-> (E! x ph)
# (E. y (/\ (= y (iota x ph))
# (E. x (/\ (= x y) ph))))))