peano.mm

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
  Metamath source file: axioms for Peano arithmetic
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$( Copyright (GPL) 2004 Robert Solovay, PO Box 5949, Eugene OR, 97405   $)
$( Comments welcome; email to:  solovay at gmail dot com $)

$( Version of 22-Jun-2021 $)
$( Replaces prior version of 13-July-04 $)
$( 22-Jun-2021 (Patrick Brosnan) - Add missing distinct variable constraints
   to pa_ax7 $)
$( 7-Oct-2004 (N. Megill) - Minor fixes to conform to strict Metamath spec $)
$( 11-Oct-2004 (N. Megill) - "$a implies" --> "$a |- implies" at line 224 $)
$( 24-Jun-2006 (N. Megill) - Made label and math symbol names spaces
       disjoint, as required by the 24-Jun-2006 modification of the Metamath
       specification.  Specifically, the labels binop, logbinop, binpred,
       and quant were changed to binop_, logbinop_, binpred_, and quant_
       respectively. $)
$( 11-Nov-2014 (N. Megill) - updated R. Solovay's email address $)

$( This file is a mixture of two sorts of things:

1) Formal metamath axioms and supporting material. [$f and $d
   statements for example.]

2) Informal metamathematical arguments that show our axioms suffice to
   "do Peano in metamath".

All our metamathematical arguments are quite constructive and
certainly could be formalized in Primitive Recursive Arithmetic. $)

$( We shall slightly deviate from the treatment in Appendix C of the
metamath book. We assume that for each constant c an infinite subset
of the variables is preassigned to that constant.

In particular we will have a constant var. Among our other constants
will be all the symbols of Peano arithmetic except the variables. The
variables of the formal language of Peano Arithmetic will be
identified with the variables attached to the constant symbol var. In
this way each well formed formula or term of PA will *be* a certan
metamath expression. $)

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
            Syntax
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$c |-  wff term var $.

$( The next set of axioms will give the inductive definition of
terms. We will be using Polish notation in our formal development of
the syntax of PA. $)

$v s t u s0 s1 t0 t1 $.

ts $f term s $.
tt $f term t $.
tu $f term u $.
ts0 $f term s0 $.
ts1 $f term s1 $.
tt0 $f term t0 $.
tt1 $f term t1 $.

$v v x y z $.
varv $f var v $.
varx $f var x $.
vary $f var y $.
varz $f var z $.

$c 0 S + * $.

$( It is often possible to treat + and * in parallel. The following
device allows us to do this. $)

$c BINOP $.
$v binop $.
binop_ $f BINOP binop $.
binop_plus $a BINOP + $.
binop_times $a BINOP * $.

tvar $a term v $.
tzero $a term 0 $.
tsucc $a term S s $.
tbinop $a term binop s t $.

$( The next set of axioms will give the inductive definition of wff $)

$c not or and implies iff $.
$c LOGBINOP $.
$v logbinop $.
logbinop_ $f LOGBINOP logbinop $.
logbinopor $a LOGBINOP or $.
logbinopand $a LOGBINOP and $.
logbinopimplies $a LOGBINOP implies $.
logbinopiff $a LOGBINOP iff $.

$c = < $.
$c BINPRED $.
$v binpred $.
binpred_ $f BINPRED binpred $.
binpred_equals $a BINPRED = $.
binpred_less_than $a BINPRED < $.

$c forall exists $.
$c QUANT $.
$v quant $.
quant_ $f QUANT quant $.
quant_all $a QUANT forall $.
quant_ex $a QUANT exists $.

$v phi psi chi $.
wff_phi $f wff phi $.
wff_psi $f wff psi $.
wff-chi $f wff chi $.

wff_atom $a wff binpred s t $.
wff_not $a wff not psi $.
wff_logbinop $a wff logbinop psi phi $.
wff_quant $a wff quant v phi $.

$( This completes our description of the syntactic categories of wff
and term $)

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
            "Correct" axioms
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$( In the various sections of this file we will be adding various
axioms [$a statements]. The crucial correctness property that they
will have is the following:

     Consider a substitution instance of the axiom such that the only
     variables remaining in the instance [in either hypothesis or
     conclusion] are of type var. Then if all the hypotheses [$e
     statements] have the form
          |- phi
     [where phi is a theorem of PA] then the conclusion is also a
     theorem of PA.

     The verification that the various axioms we add are correct in
     this sense will be "left to the reader". Usually the proof that I
     have in mind is a semantic one based upon the consideration of
     models of PA. $)
$( I will give a discussion at the end of this document as to why
     sticking with this correctness condition on axioms suffices to
     guarantee that only correct theorems of Peano arithmetic are
     proved.
$)

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
         Propositional logic
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$( We follow closely the treatment in set.mm. We do have to change the
axioms "into Polish". $)

ax-1 $a |- implies phi implies psi phi $.

ax-2 $a |- implies
              implies phi implies psi chi
              implies
                 implies phi psi
                 implies phi chi  $.
ax-3 $a |- implies
              implies not phi not psi
              implies psi phi $.

$( Modus ponens: $)
${
   min $e |- phi $.
   maj $e |- implies phi psi $.
   ax-mp $a |- psi $.
$}

bi1 $a |- implies
          iff phi psi
          implies phi psi $.
bi2 $a |- implies
          iff phi psi
          implies psi phi $.
bi3 $a |- implies
          implies phi psi
          implies
             implies psi phi
             iff phi psi $.
df-an $a |- iff
               and phi psi
               not implies phi not psi $.
df-or $a |- iff
               or phi psi
               implies not phi psi $.

$( Equality axioms $)

$( From here on out, I won't make an effort to cordinate labels
between my axioms and those of set.mm $)

eq-refl $a |- = t t $.
eq-sym $a |- implies = s t = t s $.
eq-trans $a |- implies
                and = s t = t u
                = s u $.
eq-congr $a |- implies
            and = s0 s1 = t0 t1
            iff binpred s0 t0 binpred s1 t1 $.

$( The next two axioms were missing in the previous draft of
peano.mm. They are definitely needed. $)

eq-suc $a |- implies
                  = s t
                  = S s S t $.
eq-binop $a |- implies
                  and = s0 s1 = t0 t1
                  = binop s0 t0 binop s1 t1 $.

$( Lemma 1 $)

$( Lemma 1 of the 2004 version of this document was not needed in the
subsequent development and has been deleted. I decided not to change
the numbering of subsequent lemmas. $)


$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
             Free and bound variables; alpha equivalence
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$( It will be useful to warm up with some familiar concepts. Let PHI
   be a well-formed formula of Peano arithmetic. Then Phi is a finite
   sequence of symbols, s_1 ... s_n.

   Following Shoenfield's treatment in "Mathematical Logic" we use the
   term "designator" for a sequence of symbols that is either a term
   or a wff. A basic result says that each s_i is the initial symbol
   of precisely one subsequence of s_1 ... s_n which is a designator.

   Suppose that s_i is a variable. We say that s_i is bound in PHI if
   there is a subformula of PHI containing s_i whose initial symbol is
   a quantifier and whose second symbol is the same variable as s_i.

   [Otherwise s_i is *free* in PHI.]

   If s_i is a bound variable, then there is a shortest subformula of
   PHI in which s_i is bound. The quantifier beginning this subformula
   is the quantifier that *binds* s_i. $)

$( alpha equivalence $)

$( Let Phi_1 and Phi_2 be well-formed formulas of PA. Say Phi_1 is s_1
... s_n and Phi_2 is t_1 ... t_m.

    We say that Phi_1 and Phi_2 are alpha-equialent if:

1) n = m.

2) Let 1 <= i <= n. Then s_i is a constant iff t_i is; in that case,
   they are the *same* constant.

3) Let 1 <= i <= n. Suppose that s_i is a variable. [So t_i is a
   variable as well.] Then s_i is free in Phi_1 iff t_i is free in
   Phi_2. If s_i is free in Phi_1, then s_i = t_i.

4) Let 1 <= i <= n. Suppose that s_i is a variable that is bound in
   Phi_1. [It follows that t_i is a variable that is bound in Phi_2.]
   Let s_j be the quantifier that binds s_i. Then t_j is the
   quantifier that binds t_i.

[This ends the definition of alpha-equivalence.]

It is indeed true that alpha-equivalence is an equivalence relation.
$)

$( Trim formulas $)

$( The following concept is non-standard. A well-formed formula of PA
is *trim* if:

   1) No variable occurs both free and bound in Phi.

   2) Distinct quantifiers bind distinct variables.

[So
exists x exists x = x x
is not trim since the two quantifiers both bind the variable x.]

   Clearly every formula is alpha-equivalent to some trim
   formula. Moreover, we can assume that the bound variables of this
   trim equivalent avoid some specified finite set of variables.
$)

$( Here is the next Lemma we are heading toward. We can add a finite
number of correct axioms to our file so that once this is done, if
Phi_1 and Phi_2 are alpha-equivalent formulas then [subject to the
requirement that any pair of distinct  variables appearing in Phi_1 or
Phi_2 is declared disjoint]

      |- iff Phi_1 Phi_2
is a theorem of Metmath [i.e. follows from the given axioms].

In view of the remarks about trim formulas, we are reduced to the
following special case: Phi_2 is trim and no bound variable of Phi_2
appears [free or bound] in Phi_1.

We fix Phi_1 and Phi_2 subject to this restriction. We will develop
the axioms we need in the course of the proof. Of course, the reader
should verify that we could have specified them in advance. In
particular the additional axioms we list will not depend on Phi_1 or Phi_2. $)

$( Our proof strategy is as follows;

To each subformula Psi of Phi_1, we shall attach a claim C(Psi) [which
will also be a well-formed formula of PA]. We will prove in Metamath
the various claims C(Psi). The construction of these proofs will be an
inductive one [by induction on the length of the subformula,
say]. From the claim C(Phi_1), the desired equivalence of Phi_1 and
Phi_2 will easily follow. $)

$( Weak alpha-equivalence $)

$( Before describing the claims C(Psi), I need to introduce the notion
of weak alpha-equivalence. Let Psi_1 and Psi_2 be two well-formed
formulas of PA.

Say Psi_1 is s_1 ... s_m and Psi_2 is t_1 ... t_n.

Then Psi_1 and Psi_2 are weakly alpha equivalent iff:

1) m = n;

2) Let 1 <= i <= n. Then s_i is a constant iff t_i is; in that case,
   they are the *same* constant.

3) Let 1 <= i <= n. Suppose that s_i is a variable. [So t_i is a
   variable as well.] Then s_i is free in Psi_1 iff t_i is free in
   Psi_2.

3a) Let 1 <= i < j <= n. Suppose that s_i and s_j are variables free
in Psi_1. [It follows that t_i and t_j are free variables in Psi_2.]
Then s_i = s_j iff t_i = t_j.

4) Let 1 <= i <= n. Suppose that s_i is a variable that is bound in
   Psi_1. [It follows that t_i is a variable that is bound in Psi_2.]
   Let s_j be the quantifier that binds s_i. Then t_j is the
   quantifier that binds t_i.

[This ends the definition of weak alpha-equivalence.] $)

$( I need a pedantic fact:

   Proposition 2.1. Let Phi_1 = s_1,..., s_m and Phi_2 = t_1...t_m be
   as above. Let 1 <= i <= j <= m. Then s_i ... s_j is a term
   [formula] iff t_i ... t_j is.

   The proof is by induction on j - i and is straightforward. [It
   splits into cases according to what s_i is.] $)

$( The following explains the importance of "weak alpha equivalence":

   Proposition 2.2.
   Let Psi_1 be a subformula of Phi_1, and Psi_2 the corresponding
   subformula of Phi_2. (Cf. the "pedantic fact" just above.) Then
   Psi_1 and Psi_2 are weakly alpha equivalent.

   Only clause 3a) of the definition of weak alpha equivalence
   requires discussion:

   Say Psi_1 occupies positions i ... j of Phi_1. Let i <= a < b <= j
   and let s_a and s_b be the same variable x. We suppose that s_a and
   s_b are free in Psi_1. We shall show that t_a = t_b. {This will
   prove one direction of the iff; the other direction is proved
   similarly.}

   If s_a and s_b are both free in Phi_1 then our claim is clear since
   Phi_1 and Phi_2 are alpha equivalent. If not, let Theta_1 be the
   smallest subformula of Phi_1 in which one of s_a and s_b is
   bound. Then both s_a and s_b are bound by the quantifer that begins
   Theta_1.

   Let Theta_2 be the subformula of Phi_2 that corresponds to
   Theta_1. Using the alpha equivalence of Phi_1 and Phi_2 we see that
   both t_a and t_b are bound by the quantifer that begins
   Theta_2. Hence t_a = t_b.

   $)

   $( We are now able to begin the definition of C(Psi_1) for Psi_1 a
   subformula of Phi_1. It will have the form

   implies H(Psi_1)
           iff Psi_1 Psi_2

   where Psi_2 is the subformula of Phi_2 that corresponds to Psi_1.

  It remains to describe H(Psi_1):

  Let w be a variable that does not appear [free or bound] in either
  Phi_1 or Phi_2. Let x_1 ... x_r be the free variables appearing in
  Psi_1 [listed without repetitions]. Because Psi_1  is weakly alpha
  equivalent to Psi_2, we can define a bijection between the free
  variables of Psi_1 and those of Psi_2 thus. If x_i appears freely in
  position j of Psi_1 then the corresponding free variable of Psi_2,
  say y_i, appears in position j of Psi_2.

  H(Psi_1) is the conjunction of the following equalities:

  1) = w w ;

  2) = x_i y_i (for i = 1 ... r).

  This completes our description of C(Psi_1). $)

  $( Consider first C(Phi_1). Because Phi_1 is alpha equivalent to
  Phi_2, H(Phi_1) is the conjunction of equalities of the form = a a .
  Hence Metamath can prove H(Phi_1) and can see that C(Phi_1) is
  equivalent to the equivalence:

      iff Phi_1 Phi_2
  $)

$( So it will be sufficient to see that Metamath [after enrichment with
some additional correct axioms] can prove C(Psi_1) for every
subformula Psi_1 of Phi_1. The proof of this proceeds by induction on
the length of Psi_1.

If Psi_1 is atomic, our claim is easily proved using the equality
axioms.

The cases when Psi_1 is built up from smaller formulas using propositional
connectives are easily handled since Metamath knows propositional
logic.

$)

$( It remains to consider the case when Psi_1 has the form Q x Chi_1
where Q is a quantifier.

It is clear that Psi_2 has the form Q y Chi_2 [where Chi_2 is the
subformula of Phi_2 that corresponds to Chi_1]. We will consider two
cases;

Case A: x = y;

Case B: x != y. $)

$( To handle Case A we adjoin the following axiom [which the reader
should verify is correct]. $)

${ $d phi x $.
   alpha_hyp1 $e |- implies phi
              iff psi chi $.
   alpha_1 $a |- implies phi
              iff quant x psi
                  quant x chi $. $}

$( We apply this axiom with H(Psi_1) in the role of phi and Q in the
role of quant. Chi_1 is in the role of psi and Chi_2 is in the role of
chi.

To see that the needed instance of alpha_hyp1 holds, note that
H(Chi_1) is either H(Psi_1) [up to a possible rearrangement of
conjuncts] or the conjunction of H(Psi_1) with the conjunct
= x x

So our needed instance follows from C(Chi_1), equality axioms and
propositional logic $)

$( We turn to case B. It is worthwhile to remind the reader that Phi_2
has been chosen so that no bound variable of Phi_2 appears either free
or bound in Phi_1.

Proposition 2.3. y does not appear [free or bound] in Psi_1. x does
not appear [free or bound] in Psi_2.

Proof: y appears bound in Psi_2. Hence it doesn't even appear [free or
bound] in Phi_1.

Suppose that x appears in Psi_2. Then this appearence must be free in
Phi_2. {Otherwise, x would not appear in Phi_1 but it is the second
symbol of Psi_1.} So at the same spot in Psi_1 x also appears, and
this occurrence is free in Phi_1. {This follows from the fact that
Phi_1 and Phi_2 are alpha equivalent.} But clearly this occurrence of
x in Psi_1 will be bound by the quantifier that starts
Psi_1. Contradiction! $)

$( Proposition 2.3 has the following immediate consequence:

Proposition 2.4: Neither of the variables x or y occurs in H(Psi_1).

      Also it is easy to check that [up to propositional logic]
      H(Chi_1) is either H(Psi_1) or the conjunction of H(Psi_1)
      with
                    = x y

It follows that from C(Chi_1) one can deduce [using propositonal
logic] the following:

(A) implies H(Psi_1)
            implies = x y
            iff Chi_1 Chi_2 $)

$( Next we introduce the following Metamath axiom [which the reader
should verify is correct] $)

${ $d phi x $.

   alpha_hyp2 $e |- implies phi chi $.
   alpha_2    $a |- implies phi forall x chi $.
$}

$( Using this axiom we can deduce from (A) and Proposition 2.4
the following:

(B) implies H(Psi_1)
            forall x forall y implies = x y
                                      iff Chi_1 Chi_2
$)

$( We need to introduce another axiom [which the reader should verify
is correct] $)

${ $d phi y $.
   $d psi x $.
   $d x y $.
   alpha_3 $a |- implies forall x forall y implies = x y
                                   iff phi psi
                         iff quant x phi quant y psi $.
$}

$( From this axiom, (B) and Proposition 2.3 we easily deduce:

(C) implies H(Psi_1)
            iff Psi_1 Psi_2

which is C(Psi_1) $)

$( The following lemma should now be clear to the reader:

Lemma 2. Let Phi and Phi* be alpha equivalent formulas of PA. Then
using the axioms so far introduced, we can prove in Metamath the
sequence

|- iff Phi_1 Phi_2

from the disjointness assumption that all the distinct variables
appearing in Phi_1 or Phi_2 are asserted to be distinct in a $d
assumption.  $)

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
                Axioms and inference rules of predicate logic
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$( Our next task is to prove the rule of inference and the axiom
associated to the "forall" quantifier. $)

$( Let's start with the rule of inference. We have to show that if

|- implies phi chi

and phi does not contain x free then also

|- implies phi forall x chi.

   But this is easy. In view of what we have just shown, it is ok to
   replace phi by an alpha-equivalent formula that does not contain x
   at all. {In both our hypothesis and conclusion.}

   But then we just need to invoke the axiom alpha_2. $)

$( We now turn to the axiom of "forall elimination". To state it we
introduce the familiar notion of substituting a term for the free
occurrences of a variable. So let phi be a formula, x a variable and t
a term. By phi[t/x] we mean the formula obtained by simultaneously
replacing each free occurrence of x in phi by a copy of the term t. {A
more rigorous definition would proceed by induction on the structure
of phi.}

   We say that t is substitutable for x at the free occurrence of x in
   phi [or just "substitutable" if we are being terse] if no variable
   occuring in t falls under the scope of any quantifer of
   phi. {Again, I am presuming this notion known; otherwise, I'd be
   more careful with this definition.}

   The final group of axioms of predicate calculus that we need to
   derive have the following form:

(*)   implies
        forall x phi
        phi[t/x]

   **where** t is substitutable for x in phi.

Our next step is to show that it suffices to prove the following
special case of this axiom. phi x and t satisfy the following three
conditions:


        (1) The variable x does not appear in the term t.

        (2) No bound variable of phi appears in t.

        (3) The variable x does not appear bound in phi.

We can see this as follows. We can clearly find a formula
   forall y psi
which is alpha equivalent to forall x phi such that:
     (1') The variable y does not appear in the term t;
     (2') No bound variable of psi appears in t;
     (3') The variable y does not appear bound in psi.

Using the fact that t is substitutable for x in phi we easily see that
phi[t/x] is alpha equivalent to psi[t/y]. It follows that (*) is
alpha-equivalent to:
(**)  implies
        forall y psi
        psi[t/y]

Hence Metamath can prove the equivalence of (*) and (**). But in view
of (1') through (3'), the instance (**) of for all elimination meets
our additional requirements (1) through (3).

In the remainder of our discussion we shall assume then that phi, x
and t meet the requirements (1) through (3). Note that it follows from
(2) that t is substitutable for x in phi.

[N.B. We cannot assume that the variables appearing in t do not appear
in phi.]

Here is the key idea of our approach: The formula phi[t/x] (under the
hypotheses (1) -- (3) just given) is equivalent to:

forall x implies
            = x t
            phi

$)

$( We start by adding the following [correct!] axiom $)

${ $d x t $.
   all_elim $a |- implies
                   forall x phi
                   forall x implies
                              = x t
                              phi $.
$}

$( Using this axiom we can reduce our proof that Metamath proves all
instances of "all elimination" to the following lemma:

Lemma 3. Let t be a term of PA and phi a formula of PA. We assume:
1) The variable x does not occur in t;
2) No bound variable of phi appears in t.
3) The variable x does not occur bound in phi.

Then [after adding finitely many additional correct axioms whose
choice does not depend on phi] we can prove in Metamath:

|- iff
     forall x implies
        = x t
        phi
    phi[t/x]

$)

$( We shall need a preliminary result:

Proposition 3.1 Let phi t and x obey our standing hypotheses 1) --
3). Let psi be a subformula of phi.

Then [after adding finitely many additional correct axioms whose
choice does not depend on phi] we can prove in Metamath:

|- implies = x t
           iff psi psi[t/x]

The construction of such proofs [like many previous arguments] is by
induction on the tree of subformulas of phi. $)

$( The first case is when psi is atomic. This case is easily handled
using the equality axioms.

The second case is when the principal connective of psi is a
propositional connective. This case follows easily using propositional
logic from our inductive hypotheses concerning the subformulas of psi.

$)

$( The final case is when the principal connective of psi is a
quantifier. This case is handled using the following axiom: $)

${ $d x y $.
   $d y t $.
   all_elim_hyp2 $e |- implies = x t
                    iff phi chi $.
   all_elim2 $a |- implies = x t
                   iff quant y phi
                       quant y chi $.
$}

$( The proof of Proposition 3.1 is now complete. We apply it to phi
and get that Metamath proves:
|- implies = x t
           iff phi phi[t/x]

Here phi and t stand for the particular wff and term of t under
discussion and are not literal metavariables of Metamath.

We also know at this point that Metamath proves:

|- implies forall x phi
           forall x implies = x t
                    phi

We would be done if we could prove in Metamath:

|- implies forall x implies = x t
                            phi
           phi[t/x]

But this will follow easily from the next axiom [which is inelegant
but correct].

 $)

${
$d x chi $.
$d x t $.

 all_elim3_hyp1 $e |- implies = x t
                           iff phi chi $.
all_elim3 $a |- implies forall x implies = x t
                                         phi
                     chi $. $}

$( This completes our discussion of "forall-elimination". $)
$( It is time to introduce the definition of the
"exists" quantifier $)

exists_def $a |- iff
              exists x phi
              not forall x not phi $.

$( Of course, the axiom and rule of inference for "exists" follow from
this definition and the corresponding inference rule or axiom scheme
for "forall". $)

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
         The non-logical axioms of Peano Arithmetic
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$( At this point, we know that Metamath can prove any logically valid
wff of PA. It remains to add the axioms of PA. $)

$( First we give the particular axioms of PA. Then we discuss the
induction scheme $)

pa_ax1 $a |- not = 0 S x $.
pa_ax2 $a |- implies = S x S y
                     = x y $.
pa_ax3 $a |- = x
               + x 0 $.
pa_ax4 $a |- = S + x y
               + x S y $.
pa_ax5 $a |- = 0
               * x 0 $.
pa_ax6 $a |- = + * x y x
               * x S y $.
${
  $d z x $.  $d z y $.
  pa_ax7 $a |- iff
               < x y
               exists z = y + x S z $.
$}

$( It suffices to give the induction axiom for the case when phi does
not contain x free. For the usual form of the axiom follows from this
special case by first order logic. $)

${
$d phi x $.
$d x y $.
induction $a
|- implies
   and forall y implies = y 0 phi
       forall x implies forall y implies = y x phi
                        forall y implies = y S x phi
   forall x forall y implies = y x phi $.
$}

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
           Discussion of correctness
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

$(
Let's agree that when I say "Metamath proves PHI" I mean "Metamath"
enriched with all the preceding axioms in this document.

The issue is the following. For what formulas Phi is there a proof in
Metamath from no $e type assumptions of the sequencce
    |- Phi.

(Recall that I am identifying the well-formed formulas of Peano with
certain of the Metamath strings of symbols. This is done by
identifying the object variables of our language with the
metavariables of type var.)

The claim is that these are precisely those Phi which are theorems of
the usual formulation of Peano Arithmetic.

One direction should be clear by this point. We have developed the
first order predicate calculus within Metamath and included the usual
axioms of Peano arithmetic [or equivalents]. So any theorem of Peano
Arithmetic [as usually formulated] can be proved in Metamath.

To go in the other direction, suppose that there is a proof in
Metamath of |- Phi. So the final line of the proof contains only
variables of type var. But there might well be variables of other
kinds in the body of the proof. For example, there might be a variable
phi of kind wff.

The critical such variables are those that appear in lines of the
proof beginning with |-.  What we do is replace such variables (of
kind different than var) [one by one] by sequences of constants of the
same type.  (So phi might be replaced by the three symbol string "= 0
0".) It is not hard to see that after this substitution the result can
be massaged to a correct proof. There are two points to notice.

     a) Since the string by which we replaced the variable contains no
     variables itself the process converges and no disjointness
     conditions [$d restrictions] are violated.

     b) We may have to add a trivial few lines to prove the "type
     assertion". In our example, the line "wff phi" will be replaced
     by the line "wff = 0 0". This line is no longer immediate but
     must be proved by a four line argument.

At the end, there results a proof where all the lines that begin with
"|-" contain only variables of type var. But now our correctness
assumptions allow us to verify step by step that each such line is a
theorem of Peano arithmetic.
$)

$( For Emacs $)
$( Local Variables: $)
$( eval:'(show-paren-mode t) $)
$( End: $)