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

Axiom ax-11 1285
Description: Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The final consequent x(x = yφ) is a way of expressing "y substituted for x in wff φ " (cf. sb6 1592). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases.

In classical logic, ax-11o 1512 can be derived from this axiom, as can be seen at ax11o 1511. However, the current proof of ax11o 1511 is not valid intuitionistically.

In classical logic, this axiom is metalogically independent from the others, but not logically independent. Lack of logical independence means that if the wff expression substituted for φ contains no wff variables, the resulting statement can be proved without invoking this axiom. The current proofs of this are not valid in intuitionistic logic, however. Specifically, we can prove any wff-variable-free instance of axiom ax-11o 1512 (from which the ax-11 1285 instance follows by theorem ax11 1513.) The proof is by induction on formula length, using ax11eq 1811 and ax11el 1812 for the basis steps and ax11indn 1813, ax11indi 1814, and ax11inda 1818 for the induction steps. Many of those theorems rely on classical logic for their proofs.

Variants of this axiom which are equivalent in classical logic but which have not been shown to be equivalent for intuitionistic logic are ax11v 1590, ax11v2 1509 and ax-11o 1512. (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-11 (x = y → (yφx(x = yφ)))

Detailed syntax breakdown of Axiom ax-11
StepHypRef Expression
1 vx . . 3 set x
2 vy . . 3 set y
31, 2weq 1280 . 2 wff x = y
4 wph . . . 4 wff φ
54, 2wal 1231 . . 3 wff yφ
63, 4wi 4 . . . 4 wff (x = yφ)
76, 1wal 1231 . . 3 wff x(x = yφ)
85, 7wi 4 . 2 wff (yφx(x = yφ))
93, 8wi 4 1 wff (x = y → (yφx(x = yφ)))
Colors of variables: wff set class
This axiom is referenced by:  ax10o  1426  equs5a  1484  sbcof2  1498  ax11o  1511  ax11v  1590  ax4  1809
  Copyright terms: Public domain W3C validator