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

Theorem ax4 1915
Description: Theorem showing that in classical logic ax-4 1333 can be derived from ax-5 1267, ax-gen 1269, ax-8 1328, ax-9 1354, ax-11 1330, and ax-17 1349. This makes ax-4 1333 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.

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 1333, ax-5o 1913, ax-10o 1489, ax-11o 1579, ax-15 1917, and ax-16 1570 may be proved by theorems ax4 1915, ax5o 1912, ax9o 1474, ax10o 1488, ax11o 1578, ax15 1916, and ax16 1569. Except for the ones suffixed with o (ax-5o 1913 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 (xφφ)

Proof of Theorem ax4
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 ax-9 1354 . 2 ¬ y ¬ y = x
2 ax-9 1354 . . . . . . . . . 10 ¬ x ¬ x = y
3 ax-8 1328 . . . . . . . . . . . . . 14 (x = y → (x = yy = y))
43pm2.43i 41 . . . . . . . . . . . . 13 (x = yy = y)
54con3i 542 . . . . . . . . . . . 12 y = y → ¬ x = y)
65ax-gen 1269 . . . . . . . . . . 11 xy = y → ¬ x = y)
7 ax-17 1349 . . . . . . . . . . 11 y = yx ¬ y = y)
8 ax-5 1267 . . . . . . . . . . 11 (xy = y → ¬ x = y) → (x ¬ y = yx ¬ x = y))
96, 7, 8mpsyl 57 . . . . . . . . . 10 y = yx ¬ x = y)
102, 9mt3 1853 . . . . . . . . 9 y = y
11 ax-8 1328 . . . . . . . . 9 (y = x → (y = yx = y))
1210, 11mpi 14 . . . . . . . 8 (y = xx = y)
13 ax-17 1349 . . . . . . . 8 φy ¬ φ)
14 ax-11 1330 . . . . . . . 8 (x = y → (y ¬ φx(x = y → ¬ φ)))
1512, 13, 14syl2im 32 . . . . . . 7 (y = x → (¬ φx(x = y → ¬ φ)))
16 con2 550 . . . . . . . . . . 11 ((x = y → ¬ φ) → (φ → ¬ x = y))
1716ax-gen 1269 . . . . . . . . . 10 x((x = y → ¬ φ) → (φ → ¬ x = y))
18 ax-5 1267 . . . . . . . . . 10 (x((x = y → ¬ φ) → (φ → ¬ x = y)) → (x(x = y → ¬ φ) → x(φ → ¬ x = y)))
1917, 18ax-mp 7 . . . . . . . . 9 (x(x = y → ¬ φ) → x(φ → ¬ x = y))
20 ax-5 1267 . . . . . . . . 9 (x(φ → ¬ x = y) → (xφx ¬ x = y))
2119, 20syl 13 . . . . . . . 8 (x(x = y → ¬ φ) → (xφx ¬ x = y))
222, 21mtoi 568 . . . . . . 7 (x(x = y → ¬ φ) → ¬ xφ)
2315, 22syl6 27 . . . . . 6 (y = x → (¬ φ → ¬ xφ))
2423con4d 721 . . . . 5 (y = x → (xφφ))
2524con3i 542 . . . 4 (¬ (xφφ) → ¬ y = x)
2625ax-gen 1269 . . 3 y(¬ (xφφ) → ¬ y = x)
27 ax-17 1349 . . 3 (¬ (xφφ) → y ¬ (xφφ))
28 ax-5 1267 . . 3 (y(¬ (xφφ) → ¬ y = x) → (y ¬ (xφφ) → y ¬ y = x))
2926, 27, 28mpsyl 57 . 2 (¬ (xφφ) → y ¬ y = x)
301, 29mt3 1853 1 (xφφ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wal 1266
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 719  ax-5 1267  ax-gen 1269  ax-ie2 1315  ax-8 1328  ax-11 1330  ax-17 1349  ax-i9 1353
This theorem depends on definitions:  df-bi 108  df-tru 1201  df-fal 1202
  Copyright terms: Public domain W3C validator