NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-nin Structured version   GIF version

Axiom ax-nin 4078
Description: State the axiom of anti-intersection. Axiom P1 of [Hailperin] p. 6. This axiom sets up boolean operations on sets.

Note on this and the following axioms: this axiom, ax-xp 4079, ax-cnv 4080, ax-1c 4081, ax-sset 4082, ax-si 4083, ax-ins2 4084, ax-ins3 4085, and ax-typlower 4086 are from Hailperin and are designed to implement the Stratification Axiom of Quine.

A well-formed formula using only propositional symbols, predicate symbols, and is "stratified" iff you can make a (metalogical) mapping from the variables to the natural numbers such that any formulas of the form x = y have the same number, and any formulas of the form x y have x as one less than y. Quine's stratification axiom states that there is a set corresponding to any stratified formula.

Since we cannot state stratification from within the logic, we use Hailperin's axioms and prove existence of stratified sets using Hailperin's algorithm. (Contributed by SF, 12-Jan-2015.)

Assertion
Ref Expression
ax-nin zw(w z ↔ (w x w y))
Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Axiom ax-nin
StepHypRef Expression
1 vw . . . . 5 set w
2 vz . . . . 5 set z
31, 2wel 1711 . . . 4 wff w z
4 vx . . . . . 6 set x
51, 4wel 1711 . . . . 5 wff w x
6 vy . . . . . 6 set y
71, 6wel 1711 . . . . 5 wff w y
85, 7wnan 1287 . . . 4 wff (w x w y)
93, 8wb 176 . . 3 wff (w z ↔ (w x w y))
109, 1wal 1540 . 2 wff w(w z ↔ (w x w y))
1110, 2wex 1541 1 wff zw(w z ↔ (w x w y))
Colors of variables: wff set class
This axiom is referenced by:  ninexg  4097
  Copyright terms: Public domain W3C validator