ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax4 Unicode version

Theorem ax4 1810
Description: Theorem showing that in classical logic ax-4 1271 can be derived from ax-5 1215, ax-gen 1218, ax-8 1266, ax-9 1283, ax-11 1268, and ax-17 1280. This makes ax-4 1271 redundant in a classical system including these axioms, but we do not have a corresponding result (or proof of independence) for intuitionistic logic yet. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114.

This theorem should not be referenced in any proof. Instead, we will use ax-4 1271 so that explicit uses of ax-4 1271 can be more easily identified. In particular, this will more cleanly separate out the theorems of "pure" predicate calculus that don't involve equality or distinct variables. A beginner may wish to accept ax-4 1271 a priori, so that the proof of this theorem (ax4 1810), which involves equality as well as the distinct variable requirements of ax-17 1280, can be put off until those axioms are studied.

Note: In set.mm, predicate calculus axioms introduced from ax4 forward are redundant. We are still in the process of figuring out the analogous situation in intuitionistic logic. Specifically, some or all of axioms ax-4 1271, ax-5o 1288, ax-6o 1291, ax-9o 1391, ax-10o 1406, ax-11o 1491, ax-15 1662, and ax-16 1481 may be proved by theorems ax4 1810, ax5o 1287, ax6o 1290, ax9o 1390, ax10o 1405, ax11o 1490, ax15 1661, and ax16 1480. Except for the ones suffixed with o (ax-5o 1288 etc.), we never reference those theorems directly. Instead, we use the axiom version that immediately follows it. This allow us to better isolate the uses of the redundant axioms for easier study of subsystems containing them.

(Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.)

Assertion
Ref Expression
ax4

Proof of Theorem ax4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax-9 1283 . 2
2 ax-9 1283 . . . . . . . . . 10
3 ax-8 1266 . . . . . . . . . . . . . 14
43pm2.43i 41 . . . . . . . . . . . . 13
54con3i 542 . . . . . . . . . . . 12
65ax-gen 1218 . . . . . . . . . . 11
7 ax-17 1280 . . . . . . . . . . 11
8 ax-5 1215 . . . . . . . . . . 11
96, 7, 8mpsyl 57 . . . . . . . . . 10
102, 9mt3 1758 . . . . . . . . 9
11 ax-8 1266 . . . . . . . . 9
1210, 11mpi 14 . . . . . . . 8
13 ax-17 1280 . . . . . . . 8
14 ax-11 1268 . . . . . . . 8
1512, 13, 14syl2im 32 . . . . . . 7
16 con2 550 . . . . . . . . . . 11
1716ax-gen 1218 . . . . . . . . . 10
18 ax-5 1215 . . . . . . . . . 10
1917, 18ax-mp 7 . . . . . . . . 9
20 ax-5 1215 . . . . . . . . 9
2119, 20syl 13 . . . . . . . 8
222, 21mtoi 568 . . . . . . 7
2315, 22syl6 27 . . . . . 6
2423con4d 715 . . . . 5
2524con3i 542 . . . 4
2625ax-gen 1218 . . 3
27 ax-17 1280 . . 3
28 ax-5 1215 . . 3
2926, 27, 28mpsyl 57 . 2
301, 29mt3 1758 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1214
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-in1 526  ax-in2 527  ax-3 714  ax-5 1215  ax-gen 1218  ax-ie2 1255  ax-8 1266  ax-11 1268  ax-17 1280  ax-i9 1282
This theorem depends on definitions:  df-bi 108  df-tru 1192  df-fal 1193
  Copyright terms: Public domain W3C validator