zf2.nql

/*

# Premise

This is a specification of a Turing machine which searches for
contradictions in ZF set theory and halts iff one exists.

# Underlying logic

Our starting point is Tarski's system S2 [Tar65], the axioms and inference
rules (detachment and generalization) of which are reproduced below.  ph, ps,
and ch range over formulae; x, y, and z range over set variables; v_0, v_1,
v_2, and v_3 are specific set variables; -> -. A. = e. E. /\ <-> represent
respectively implication, negation, universal quantification, equality, set
membership (here an opaque predicate of rank 2), existential quantification,
biconditional, and conjunction respectively.

This is similar to a subset of the logic used by the metamath.org computer
proof system; the notation for formulas and most of the ZF axioms are taken
from there.

Tar65: Tarski, Alfred, "A Simplified Formalization of Predicate Logic with
Identity," Archiv für Mathematische Logik und Grundlagenforschung, 7:61-79
(1965)

    DET ph
            where ( ph -> ps ) and ps are previously proved
    GEN A. x ph
            where ph is previously proved

    B1  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
    B2  ( ( -. ph -> ph ) -> ph )
    B3  ( ph -> ( -. ph -> ps ) )
    B4  ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
    B5  ( A. x ph -> ph )
    B6  ( ph -> A. x ph )
            where x does not appear syntactically in ph
    B7  E. x x = y
            where x and y are different variables
    B8  ( x = y -> ( ph -> ps ) )
            where ph and ps are atomic formulas and ps is obtained from ph
            by replacing a single instance of x with y

State count is affected strongly by logic but much less so by the lengths of
axioms, so we want to move as much complexity as possible into axioms and out
of side conditions.  S2 is already much better for us than most systems, as it
avoids the notions of free variable and proper substitution (or more precisely
these notions are implicit and emergent: suitable universal closures of ph ->
A. x ph fill the role of "x is not free in ph", and suitable closures of ( x =
y -> ( ph <-> ps ) ) fill the role of "substituting x for y in ph produces
ps"); we can do do better for axioms B5, B6, B7, and B8 however.

Axiom B5 is simply unneeded; it was proven redundant by KM65.

KM65: Kalish, D. and R. Montague, "On Tarski's formalization of predicate logic
with identity," Archiv für Mathematische Logik und Grundlagenforschung,
7:81-101 (1965)

B6 requires a recursive decomposition of the formula ph.  We can simplify this
by providing axioms to cover the cases and requiring the recursion to be done
in the proof; there are five cases that need to be covered:

    B6 I    ( x = y -> A. z x = y )
            where z != x, z != y
    B6 II   ( x e. y -> A. z x e. y )
            where z != x, z != y
    B6 III  ( A. z ( ph -> A. z ph ) -> ( A. z ( ps -> A. z ps ) ->
                ( ( ph -> ps ) -> A. z ( ph -> ps ) ) ) )
    B6 IV   ( A. z ( ph -> A. z ph ) -> ( -. ph -> A. z -. ph ) )
    B6 V    ( A. x ( ph -> A. z ph ) -> ( A. x ph -> A. z A. x ph ) )

This recursive scheme is used in the Metamath system to handle cases where x is
free in ph but not syntactically absent.  Here we use it merely to avoid the
complexity of syntactic absence.  We do not need an axiom for B6(III) as it can
be proven from B6(IV), B4, and propositional logic; likewise shorter axioms can
be found which prove IV and V over the remainder of the system.  I and II are
combined to share their conditional clause.  Thus we replace B6 with:

    B6a ( x = y -> A. z x = y /\ x e. y -> A. z x e. y )
            where x != z, y != z
    B6b ( A. x A. y ph -> A. y A. x ph )
    B6c ( E. x A. x ph -> ph )

The constraint on B7 reduces the number of axioms generated by the scheme, but
it is not necessary for soundness so we omit it.  Our B7 becomes:

    B7  E. x x = y

B8 as written has four cases, since we have two primitive relations (equality
and membership) and each relation can be substituted on either side.  It is not
necessary to provide substitutions for both sides of the equality predicate
since equality is commutative.  Some care is needed because B8 is used to prove
commutativatity of equality, and the form that is provided must suffice for
that proof; B8a below suffices for Lemma 3 of KM65.  B8 becomes:

    B8a ( x = y -> ( x = z -> y = z ) )
    B8b ( x = y -> ( x e. z -> y e. z ) )
    B8c ( x = y -> ( z e. x -> z e. y ) )

# Set theory

The ZF axioms of extensionality, replacement, power set, and union are taken
from the Metamath system (ax-ext, ax-rep, ax-pw, ax-un), except that where the
Metamath axioms are schemes over an arbitrary choice of logical variables, we
require use of v_0 through v_3 to avoid requiring distinct variable conditions
on any axiom besides B6a and to prevent requiring more than 3 parameters to
any primitive scheme.

Replacement is still a scheme over a formula variable ph, which is protected as
"A. v_1 ph" to avoid false-capture issues.  Replacement is expressed sharply
with a biconditional such that there are no extraneous sets in the replacement
result, thus a distinct separation axiom is not needed; power set and union
take advantage of this by allowing extraneous sets, the true union or power set
can be proved to exist via separation.

Regularity and Choice are omitted as they do not affect the consistency
strength of the system.

The Metamath system provides two versions of the axiom of infinity.  ax-inf
states that there exists a nonempty set which is a subset of its union; this is
one of the shorter axioms but requires both regularity and replacement to
derive useful properties.  The other, ax-inf2, directly states the existence of
a set which contains all finite ordinals; this is much longer but can be used
in subsystems with only separation.  Since we have replacement but not
regularity, we use neither; INF below is a form of Zermelo's axiom of infinity,
describing a set which contains all iterated singletons of some element.

Our final axiom set is:

    DET | MAJOR ( ph -> ps )
        | MINOR ph
        | ps

    GEN | FROM ph
        | A. x ph

    B1  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
    B2  ( ( -. ph -> ph ) -> ph )
    B3  ( ph -> ( -. ph -> ps ) )
    B4  ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
    B6a ( x = y -> A. z x = y /\ x e. y -> A. z x e. y )
            where x != z, y != z
    B6b ( A. x A. y ph -> A. y A. x ph )
    B6c ( E. x A. x ph -> ph )
    B7  E. x x = y
    B8a ( x = y -> ( x = z -> y = z ) )
    B8b ( x = y -> ( x e. z -> y e. z ) )
    B8c ( x = y -> ( z e. x -> z e. y ) )

    EXT ( A. v_2 ( v_2 e. v_0 <-> v_2 e. v_1 ) -> v_0 = v_1 )
    REP ( A. v_3 E. v_1 A. v_2 ( A. v_1 ph -> v_2 = v_1 ) ->
        E. v_1 A. v_2 ( v_2 e. v_1 <-> E. v_3 ( v_3 e. v_0 /\ A. v_1 ph ) ) )
    POW E. v_1 A. v_2 ( A. v_3 ( v_3 e. v_2 -> v_3 e. v_0 ) -> v_2 e. v_1 )
    UNI E. v_1 A. v_2 ( E. v_3 ( v_2 e. v_3 /\ v_3 e. v_0 ) -> v_2 e. v_1 )
    INF E. v_1 ( v_0 e. v_1 /\ A. v_0 ( v_0 e. v_1 -> E. v_2 ( v_2 e. v_1 /\
        A. v_1 ( v_1 e. v_2 <-> v_1 = v_0 ) ) ) )

# Encoding wffs and proofs as integers

Define (X . Y) as X + (X + Y) * (X + Y + 1) / 2.  This is the Cantor pairing
function; it takes nonnegative integer values and is bijective, in particular
(X . Y) = 0 iff X = Y = 0, and Y < (X . Y) if (X . Y) != 0.  Extend the
notation as follows:

    (X Y Z) = (X . (Y Z))
    (Z)     = (Z . 0)
    (X; Y)  = (X . (; Y)) = (X . 1 + (Y . 0))

There are a countable infinity of set variables, numbered in the most direct
way.

Wffs are numbered recursively using the pairing function:

    | v_i = v_j  |      ( ( i . j ) . 0 )
    | v_i e. v_j |      ( ( i . j ) . 1 )
    | ph -> ps   |      ( ( |ph| . |ps| ) . 2 )
    | -. ph      |      ( |ph| . 3 )
    | A. v_i ph  |      ( ( i . |ph| ) . 4 )

No checking is done to verify that a wff has one of these forms before creating
a substitution instance of an axiom, so other forms will exist during
execution.  They may consistently be treated as vacuous or unsatisfiable.

The wff with numeric value 0 is |v_0 = v_0|.  This is a theorem of ZF, and may
be substituted anywhere a theorem is required.  The wff with numeric value 1 is
|v_0 e. v_0|; this is not a theorem, as its universal closure states that all
sets contain themselves.  It serves as the canonical contradiction; the search
stops when a proof of 1 is found.

A proof is a list of integers taken in repeating groups of 4, each an axiom
code followed by three parameters, such as (ACa P1a P2A P3a; ACb P1b P2b P3b;
...).  A proof manipulates a stack of proved theorems.  A step in the proof
corresponding to an inference rule pops one or two theorems from the stack;
every step pushes a new theorem.  Invalid steps push the moot theorem |v_0 =
v_0|.  Execution halts if at any point |v_0 e. v_0| is pushed.  The stack is
not cleared between "proofs" and it is possible for one proof to see theorems
left on the stack by previous proofs; however the stack contains only theorems,
so a false halt cannot occur by this reason.  Stack underflow returns proofs
of |v_0 = v_0| because 0 = (0 . 0).

Axiom codes are assigned as follows.  -- means ignored.

    AC  P1  P2  P3  WHAT
    1   ps  --  --  Detachment rule.  Pops a minor premise (proof of ph), then
                    pops a major premise which is expected to match
                    ( ph -> P1 ).  If the major premise matches, pushes ps,
                    else pushes moot.
    2   x   --  --  Generalization rule.  Pops a theorem of statement ph;
                    proves A. x ph.
    3   ph  ps  ch  Push B1
    4   ph  --  --  Push B2
    5   ph  ps  --  Push B3
    6   x   ph  ps  Push B4
    7   x   y   z   Push B6a if distinctness conds met, else moot
    8   x   y   ph  Push B6b
    9   x   ph  --  Push B6c
    10  x   y   --  Push B7
    11  x   y   z   Push B8a
    12  x   y   z   Push B8b
    13  x   y   z   Push B8c
    14  --  --  --  Push EXT
    15  ph  --  --  Push REP
    16  --  --  --  Push POW
    17  --  --  --  Push UNI
    >17 --  --  --  Push INF

# Use of variables

The main loop runs over all sequences of proof steps, encoded by nextproof.
Each sequence is temporarily in prooflist; the next outermost loop breaks down
prooflist one step at a time, with the parts of the step in axiomcode, param1,
param2, and param3.  prooflist is reset when it reaches zero, which happens
infinitely often because prooflist is reduced by at least 1 in every iteration
where it is not reset.

(topwff . wffstack) represents a single list, the wff-stack.  Between
iterations of the step loop, the wff stack corresponds to the stack of
previously proved statements described above.  Within the step loop, there may
be unproved statements on the wff-stack.

The bulk of the step loop consists of a sequence of clauses, each of which ends
with a call to select().  A clause is _active_ if axiomcode == 1; axiomcode is
decremented after each clause, so the initial value of axiomcode selects which
clause is active.  An inactive clause must not remove proofs from the proof
section of the wffstack or modify the params variables.

Wffs are constructed using a sequence of calls to functions that manipulate the
wff stack, effectively using a reverse-Polish notation.

    v_0()       ( -- v_0 ) Pushes variable 0, or the moot theorem
    v_1()       ( -- v_1 )
    v_2()       ( -- v_2 )
    v_3()       ( -- v_3 )
    par1()      ( -- P1 ) Pushes a scheme parameter
    par2()      ( -- P2 )
    par3()      ( -- P3 )
    wim()       ( ph ps -- ( ph -> ps ) )
    wn()        ( ph -- -. ph )
    wal()       ( x ph -- A. x ph )
    wex()       ( x ph -- E. x ph )
    wa()        ( ph ps -- ( ph /\ ps ) )
    wel()       ( x y -- x e. y )
    weq()       ( x y -- x = y )

No operator is provided for \/ or <->; they must be expanded.

*/

global prooflist;
global nextproof;

global topwff;
global wffstack;

global axiomcode;
global param1;
global param2;
global param3;

global t2;

/* Cantor pair manipulation proctions */
/* zeros in1, in2 */
proc pair(out, in1, in2) {
    builtin_pair(out, in1, in2);
}

/* zeros in */
proc unpair(out1, out2, in) {
    builtin_unpair(out1, out2, in);
}

proc pushwff() { pair(wffstack, topwff, wffstack); }
proc popwff() { unpair(topwff, wffstack, wffstack); }
proc v_0_() { pushwff(); topwff = topwff + 0; }
proc v_1_() { pushwff(); topwff = topwff + 1; }
proc v_2_() { pushwff(); topwff = topwff + 2; }
proc v_3_() { pushwff(); topwff = topwff + 3; }
proc v_4_() { pushwff(); topwff = topwff + 4; }

proc cons() { unpair(t2, wffstack, wffstack); pair(topwff, t2, topwff); }
proc weq() { cons(); v_0_(); cons(); }
proc wel() { cons(); v_1_(); cons(); }
proc wim() { cons(); v_2_(); cons(); }
proc wn()  { v_3_(); cons(); }
proc wal() { cons(); v_4_(); cons(); }

proc wex() { wn(); wal(); wn(); }
proc wa() { wn(); wim(); wn(); }

proc v_0() { v_0_(); noop_7(); }
proc v_1() { v_1_(); noop_7(); }
proc v_2() { v_2_(); noop_7(); }
proc v_3() { v_3_(); noop_7(); }

proc par1() { pushwff(); topwff = param1; noop_7(); }
proc par2() { pushwff(); topwff = param2; noop_7(); }
proc par3() { pushwff(); topwff = param3; noop_7(); }

proc select() {
    builtin_move(t2, topwff); popwff();
    if (axiomcode > 0) {
        axiomcode = axiomcode - 1;
        builtin_move(topwff, t2);
    }
}

proc cparam(p) {
    if (axiomcode == 1) {
        unpair(t2, wffstack, wffstack);
        builtin_move(p, t2);
    }
}


proc main() {
    if (prooflist == 0) {
        prooflist = nextproof;
        nextproof = nextproof + 1;
    }
    prooflist = prooflist - 1;

    unpair(t2, prooflist, prooflist); builtin_move(axiomcode, t2);
    unpair(t2, prooflist, prooflist); builtin_move(param1, t2);
    unpair(t2, prooflist, prooflist); builtin_move(param2, t2);
    unpair(t2, prooflist, prooflist); builtin_move(param3, t2);
    v_0();

    /* DET */
    cparam(param3); /* minor premise ph */
    cparam(param2); /* major premise ( ph -> ps ) */ /* par1 = ps */
    par3(); par1(); wim();
    if (topwff != param2) {
        topwff = 0;
    } else {
        topwff = param1;
    }
    select();

    /* GEN */
    cparam(param3); /* ph */
    par1(); par3(); wal(); select();

    /* B1 */
    par1(); par2(); wim(); par2(); par3(); wim(); par1(); par3(); wim(); wim(); wim(); select();

    /* B2 */
    par1(); wn(); par1(); wim(); par1(); wim(); select();

    /* B3 */
    par1(); par1(); wn(); par2(); wim(); wim(); select();

    /* B4 */
    par1(); par2(); par3(); wim(); wal(); par1(); par2(); wal(); par1(); par3(); wal(); wim(); wim(); select();

    /* B6a */
    par1(); par2(); weq();  par3(); par1(); par2(); weq(); wal();  wim();
    par1(); par2(); wel();  par3(); par1(); par2(); wel(); wal();  wim(); wa();
    if (param1 == param3 || param3 == param2) {
        topwff = 0;
    }
    select();

    /* B6b */
    par1(); par2(); par3(); wal(); wal();  par2(); par1(); par3(); wal(); wal();  wim();  select();

    /* B6c */
    par1(); par1(); par2(); wal(); wex();  par2();  wim();  select();

    /* B7 */
    par1(); par1(); par2(); weq(); wex(); select();

    /* B8a */
    par1(); par2(); weq();  par1(); par3(); weq();  par2(); par3(); weq(); wim(); wim();  select();

    /* B8b */
    par1(); par2(); weq();  par1(); par3(); wel();  par2(); par3(); wel(); wim(); wim();  select();

    /* B8c */
    par1(); par2(); weq();  par3(); par1(); wel();  par3(); par2(); wel(); wim(); wim();  select();

    /* EXT */
    v_2();
    v_2(); v_0(); wel();  v_2(); v_1(); wel(); wim();
    v_2(); v_1(); wel();  v_2(); v_0(); wel(); wim(); wa();
    wal();  v_0(); v_1(); weq(); wim();  select();

    /* REP */
    v_3(); v_1(); v_2();  v_1(); par1(); wal(); v_2(); v_1(); weq(); wim();  wal(); wex(); wal();
    v_1(); v_2();
    v_2(); v_1(); wel();  v_3(); v_3(); v_0(); wel(); v_1(); par1(); wal(); wa(); wex();  wim();
    v_3(); v_3(); v_0(); wel(); v_1(); par1(); wal(); wa(); wex();  v_2(); v_1(); wel();  wim(); wa();
    wal(); wex();
    wim(); select();

    /* POW */
    v_1(); v_2();  v_3(); v_3(); v_2(); wel(); v_3(); v_0(); wel(); wim(); wal();  v_2(); v_1(); wel(); wim();  wal(); wex();  select();

    /* UNI */
    v_1(); v_2();  v_3(); v_2(); v_3(); wel(); v_3(); v_0(); wel(); wa(); wex();  v_2(); v_1(); wel(); wim();  wal(); wex();  select();

    /* INF */
    v_1(); v_0(); v_1(); wel();  v_0(); v_0(); v_1(); wel();  v_2(); v_2(); v_1(); wel();
    v_1();   v_1(); v_2(); wel();  v_1(); v_0(); weq(); wim();
    v_1(); v_0(); weq();  v_1(); v_2(); wel();  wim(); wa(); wal();
    wa(); wex();  wim(); wal();  wa(); wex(); select();

    if (topwff == 1) {
        /* vacuously false wff proved, we're done */
        return;
    }
}