PA Axioms - Hikkihiki/LogicVerifier GitHub Wiki
PA Axioms
Define N(x) as x \in N, is a proposition.
Note that we are not defining PA Axioms with Set Theory, we are defining it with proposition only. You could replace the proposition x \in N to whatever make sense for you.
Define E(x, y) as x = y, is a proposition.
P(0)\ \forall x, P(x), E(x,x)\ \forall x,y, E(x,y) \implies E(y,x)\ \forall x,y,z, E(x,y) \wedge E(y,z) \implies E(x,z)\ \forall x,y, P(x) \wedge E(x,y) \implies P(y)\ \forall x, P(x) \implies P(S(x))\ \forall x, y, P(x) \wedge P(y), E(x,y) \iff E(S(x), S(y))\ \forall x P(x), \neg S(x) = 0