File: peano.mm

package info (click to toggle)
metamath-databases 0.0.0~20210101.git55fe226-2
  • links: PTS, VCS
  • area: main
  • in suites: bookworm, bullseye, sid
  • size: 48,584 kB
  • sloc: makefile: 7; sh: 6
file content (859 lines) | stat: -rw-r--r-- 27,842 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
  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 20-January-07 $)
$( Replaces prior version of 13-July-04 $)
$( 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 $.
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: $)