New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-nin Unicode 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 have the same number, and any formulas of the form have as one less than . 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
Distinct variable group:   ,,,

Detailed syntax breakdown of Axiom ax-nin
StepHypRef Expression
1 vw . . . . 5
2 vz . . . . 5
31, 2wel 1401 . . . 4
4 vx . . . . . 6
51, 4wel 1401 . . . . 5
6 vy . . . . . 6
71, 6wel 1401 . . . . 5
85, 7wnand 1258 . . . 4
93, 8wb 173 . . 3
109, 1wal 1322 . 2
1110, 2wex 1327 1
 Colors of variables: wff set class This axiom is referenced by:  ninexg  3199
 Copyright terms: Public domain W3C validator