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

Axiom ax-nin 3180
Description: State the axiom of anti-intersection. Axiom P1 of {{Hailperin}}. This axiom sets up boolean operations on sets.

Note on this and the following axioms: this axiom, ax-xp 3181, ax-cnv 3182, ax-1c 3183, ax-sset 3184, ax-si 3185, ax-ins2 3186, ax-ins3 3187, and ax-typlower 3188 are from {{Hailperin}}, and are designed to implement the Stratification Axiom from {{Quine2}}.

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.

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 1401 . . . 4 wff w z
4 vx . . . . . 6 set x
51, 4wel 1401 . . . . 5 wff w x
6 vy . . . . . 6 set y
71, 6wel 1401 . . . . 5 wff w y
85, 7wnand 1258 . . . 4 wff (w x w y)
93, 8wb 173 . . 3 wff (w z ↔ (w x w y))
109, 1wal 1322 . 2 wff w(w z ↔ (w x w y))
1110, 2wex 1327 1 wff zw(w z ↔ (w x w y))
Colors of variables: wff set class
This axiom is referenced by:  ninexg  3199
  Copyright terms: Public domain W3C validator