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

Axiom ax-bnd 1333
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 zz = x ¬ zz = x. 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. zz = x holds if z and x are the same variable, likewise for z and y, and xz(x = yzx = y) holds if z 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 is similar to ax-i12 1332, but appears to be stronger. At least for now, we keep them both as distinct axioms, but they serve similar purposes.

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-bnd (z z = x (z z = y xz(x = yz x = y)))

Detailed syntax breakdown of Axiom ax-bnd
StepHypRef Expression
1 vz . . . 4 set z
2 vx . . . 4 set x
31, 2weq 1326 . . 3 wff z = x
43, 1wal 1267 . 2 wff z z = x
5 vy . . . . 5 set y
61, 5weq 1326 . . . 4 wff z = y
76, 1wal 1267 . . 3 wff z z = y
82, 5weq 1326 . . . . . 6 wff x = y
98, 1wal 1267 . . . . . 6 wff z x = y
108, 9wi 4 . . . . 5 wff (x = yz x = y)
1110, 1wal 1267 . . . 4 wff z(x = yz x = y)
1211, 2wal 1267 . . 3 wff xz(x = yz x = y)
137, 12wo 608 . 2 wff (z z = y xz(x = yz x = y))
144, 13wo 608 1 wff (z z = x (z z = y xz(x = yz x = y)))
Colors of variables: wff set class
This axiom is referenced by:  nfsbxy  1717  nfsbxyt  1718  sbcomxyyz  1745  dvelimor  1791
  Copyright terms: Public domain W3C validator