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

Axiom ax-bndl 1486
 Description: Axiom of bundling. The general idea of this axiom is that two variables are either distinct or non-distinct. That idea could be expressed as ∀𝑧𝑧 = 𝑥 ∨ ¬ ∀𝑧𝑧 = 𝑥. However, we instead choose an axiom which has many of the same consequences, but which is different with respect to a universe which contains only one object. ∀𝑧𝑧 = 𝑥 holds if 𝑧 and 𝑥 are the same variable, likewise for 𝑧 and 𝑦, and ∀𝑥∀𝑧(𝑥 = 𝑦 → ∀𝑧𝑥 = 𝑦) holds if 𝑧 is distinct from the others (and the universe has at least two objects). As with other statements of the form "x is decidable (either true or false)", this does not entail the full Law of the Excluded Middle (which is the proposition that all statements are decidable), but instead merely the assertion that particular kinds of statements are decidable (or in this case, an assertion similar to decidability). This axiom implies ax-i12 1485 as can be seen at axi12 1494. Whether ax-bndl 1486 can be proved from the remaining axioms including ax-i12 1485 is not known. The reason we call this "bundling" is that a statement without a distinct variable constraint "bundles" together two statements, one in which the two variables are the same and one in which they are different. (Contributed by Mario Carneiro and Jim Kingdon, 14-Mar-2018.)
Assertion
Ref Expression
ax-bndl (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))

Detailed syntax breakdown of Axiom ax-bndl
StepHypRef Expression
1 vz . . . 4 setvar 𝑧
2 vx . . . 4 setvar 𝑥
31, 2weq 1479 . . 3 wff 𝑧 = 𝑥
43, 1wal 1329 . 2 wff 𝑧 𝑧 = 𝑥
5 vy . . . . 5 setvar 𝑦
61, 5weq 1479 . . . 4 wff 𝑧 = 𝑦
76, 1wal 1329 . . 3 wff 𝑧 𝑧 = 𝑦
82, 5weq 1479 . . . . . 6 wff 𝑥 = 𝑦
98, 1wal 1329 . . . . . 6 wff 𝑧 𝑥 = 𝑦
108, 9wi 4 . . . . 5 wff (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
1110, 1wal 1329 . . . 4 wff 𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
1211, 2wal 1329 . . 3 wff 𝑥𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)
137, 12wo 697 . 2 wff (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
144, 13wo 697 1 wff (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑥𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
 Colors of variables: wff set class This axiom is referenced by:  axi12  1494  nfsbxy  1915  nfsbxyt  1916  sbcomxyyz  1945  dvelimor  1993  oprabidlem  5802
 Copyright terms: Public domain W3C validator