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.) |