| 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 4080, ax-cnv 4081,
ax-1c 4082, ax-sset 4083, ax-si 4084, ax-ins2 4085, ax-ins3 4086, and
ax-typlower 4087 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 
  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. (Contributed by SF,
12-Jan-2015.) |
"){kind=small}
