Create a gist now

Instantly share code, notes, and snippets.

@sorear /zf.lac
Last active May 10, 2016

first-order logic and ZF set theory in Adam Yedidia's Laconic
/* Cantor pair manipulation functions */
/* t0 and t1 clobbered by pairing, also use t0 as blackhole a la MIPS */
int t0;
int t1;
func pair(out, in1, in2) {
t0 = in1 + in2;
out = (t0 * (t0 + 1)) / 2 + in2;
}
func unpair(out1, out2, in) {
t0 = 0;
while (2 * in >= t0 * (t0 + 1)) {
t0 = t0 + 1;
}
t0 = t0 - 1;
t1 = in - (t0 * (t0 + 1)) / 2;
out2 = t1;
out1 = t0 - t1;
}
func push(stack, var) { pair(stack, var, stack); }
func pop(var, stack) { unpair(var, stack, stack); }
/* Wff construction routines */
/* wstack is a cons-list of wffs, proof nodes, or variable names */
/* proof is the current node in the claimed proof */
/* valid is set to zero when the verifier discovers an error */
int wstack;
int proof;
int valid;
int t2;
int t3;
int t4;
int t5;
/* metavariable routines, push a value from the proof node */
func gproof {
push(wstack, proof);
}
func car() {
pop(t2, wstack);
unpair(t2, t0, t2);
push(wstack, t2);
}
func cdr() {
pop(t2, wstack);
unpair(t0, t2, t2);
push(wstack, t2);
}
func cddr() { cdr(); cdr(); }
func cadr() { cdr(); car(); }
/* our axioms need 4 metavariables */
func vA() { gproof(); cadr(); }
func vB() { gproof(); cdr(); cadr(); }
func vC() { gproof(); cddr(); cadr(); }
func vD() { gproof(); cddr(); cdr(); cadr(); }
/* check that two (set!) variables are distinct */
func isne() {
pop(t2, wstack);
pop(t3, wstack);
if (t2 == t3) {
valid = 0;
}
}
/* equality check, use this after verify() to be sure of what was proved */
func isne() {
pop(t2, wstack);
pop(t3, wstack);
if (t2 != t3) {
valid = 0;
}
}
/* wff codes:
(1, (|ph|, |ps|)) = ( ph -> ps )
(2, (|ph, |ph|)) = -. ph
(3, (|ph|, |x|)) = A. x ph
(4, (|x|, |y|)) = x = y
(5, (|x|, |y|)) = x e. y */
func triple() {
pop(t2, wstack); /* 2nd part */
pop(t3, wstack); /* 1st part */
pair(t2, t3, t2);
pair(t2, t4, t2);
push(wstack, t2);
}
func wal() {
t4 = 3;
triple();
}
func wn() {
unpair(t4, t0, wstack);
push(wstack, t4);
t4 = 2;
triple();
}
func wi() {
t4 = 1;
triple();
}
func weq() {
t4 = 4;
triple();
}
func wel() {
t4 = 5;
triple();
}
/* checks that set x does not appear in wff ph.
used only by ax-17 and is not strictly needed, but saves a few axioms(?)
IN (x ph) OUT () */
func var_not_used() {
pop(t3, wstack);
pop(t2, wstack);
unpair(t3, t4, t3);
unpair(t4, t5, t4);
/* t2=x t3=ph.opcode t4=ph.left t5=ph.right */
if ((t2 == t5) && (t3 >= 3)) { valid = 0; }
if ((t2 == t4) && (t3 >= 4)) { valid = 0; }
if (t3 == 1) {
push(wstack, t2);
push(wstack, t4);
push(wstack, t2);
push(wstack, t5);
var_not_used();
var_not_used();
} else if (t3 < 4) {
push(wstack, t2);
push(wstack, t4);
var_not_used();
}
}
/* abbreviations */
int t6;
int t7;
func wex() { /* E. x ph == -. A. x -. ph */
pop(t6,wstack);
wn();
push(wstack,t6);
wal();
wn();
}
func wa() { /* ( ph /\ ps ) == -. ( ph -> -. ps ) */
wn();
wi();
wn();
}
func wb() { /* ( ph <-> ps ) == ( ( ph -> ps ) /\ ( ps -> ph ) ) */
unpair(t6, t7, wstack); /* t6=tos=ps */
unpair(t7, t0, t7); /* t7=ntos=ph */
wi();
pair(wstack, t7, wstack);
pair(wstack, t6, wstack);
wi();
wan();
}
/* verifier */
func verify() {
/* wstack in: proof stack out: wff that was proved, may set valid=0 */
/* get the opcode/axiom number */
pop(proof, wstack);
unpair(t2, t0, proof);
/* axioms from:
http://us.metamath.org/mpegif/mmset.html
http://us.metamath.org/mpegif/mmzfcnd.html
I've omitted Regularity and Choice because they don't affect logical power. */
/* re-added Regularity per metamath-list discussion, until someone gets me an axinf2nd */
/* mostly generated with https://github.com/sorear/smm/blob/master/misc/printparse.js */
if (t2 == 18) {
/* axiom of modus ponens
A: ph
B: ps
C: proof of ( ph -> ps )
D: proof of ph
=> ps
*/
/* doing this in a weird order so that we don't reference "proof" after the recursive call */
vB();
vA(); vB(); wi(); vC();
vA(); vD(); verify(); iseq();
verify(); iseq();
} else if (t2 == 1) {
/* axiom of generalization
A: ph B: x C: proof(ph) => A. x ph */
vA(); vB(); wal();
vA(); vC(); verify(); iseq();
/* from here on are true axioms, which do not use verify() */
/* set variables and wff variables are assigned to metavariables in that order */
} else if (t2 == 19) {
/* ax-1: ( ph -> ( ps -> ph ) ) */
vA(); vB(); vA(); wi(); wi();
} else if (t2 == 20) {
/* ax-2: ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) */
vA(); vB(); vC(); wi(); wi(); vA(); vB(); wi(); vA(); vC(); wi(); wi(); wi();
} else if (t2 == 21) {
/* ax-3: ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) */
vA(); wn(); vB(); wn(); wi(); vB(); vA(); wi(); wi();
} else if (t2 == 2) {
/* ax-5: (A. x (ph -> ps) -> (A. x ph -> A. x ps)) */
vA(); vB(); wi(); vC(); wal(); vA(); vC(); wal(); vB(); vC(); wal(); wi(); wi();
} else if (t2 == 3) {
/* ax-6: (-. A. x ph -> A. x -. A. x ph) */
vA(); vB(); wal(); wn(); vA(); vB(); wal(); wn(); vB(); wal(); wi();
} else if (t2 == 4) {
/* ax-7: (A. x A. y ph -> A. y A. x ph) */
vA(); vB(); wal(); vC(); wal(); vA(); vC(); wal(); vB(); wal(); wi();
} else if (t2 == 5) {
/* ax-8: (x = y -> (x = z -> y = z)) */
vA(); vB(); weq(); vA(); vC(); weq(); vB(); vC(); weq(); wi(); wi();
} else if (t2 == 6) {
/* ax-9: -. A. x -. x = y */
vA(); vB(); weq(); wn(); vA(); wal(); wn();
} else if (t2 == 7) {
/* ax-11: (x = y -> (A. y ph -> A. x (x = y -> ph))) */
vA(); vB(); weq(); vC(); vB(); wal(); vA(); vB(); weq(); vC(); wi(); vA(); wal(); wi(); wi();
} else if (t2 == 8) {
/* ax-12: (-. x = y -> (y = z -> A. x y = z)) */
vA(); vB(); weq(); wn(); vB(); vC(); weq(); vB(); vC(); weq(); vA(); wal(); wi(); wi();
} else if (t2 == 9) {
/* ax-13: (x = y -> (x e. z -> y e. z)) */
vA(); vB(); weq(); vA(); vC(); wel(); vB(); vC(); wel(); wi(); wi();
} else if (t2 == 10) {
/* ax-14: (x = y -> (z e. x -> z e. y )) */
vA(); vB(); weq(); vC(); vA(); wel(); vC(); vB(); wel(); wi(); wi();
} else if (t2 == 11) {
/* ax-17: (ph -> A. x ph) */
vB(); vA(); var_not_used();
vA(); vA(); vB(); wal(); wi();
} else if (t2 == 12) {
/* axextnd: E. x ((x e. y <-> x e. z) -> y = z) */
vA(); vB(); wel(); vA(); vC(); wel(); wb(); vB(); vC(); weq(); wi(); vA(); wex();
} else if (t2 == 13) {
/* axrepnd: E. x (E. y A. z(ph -> z = y ) -> A. z(A. y z e. x <-> E. x (A. z x e. y /\ A. y ph))) */
vA(); vB(); vC(); weq(); wi(); vB(); wal(); vC(); wex(); vB(); vD(); wel(); vC(); wal();
vD(); vC(); wel(); vB(); wal(); vA(); vC(); wal(); wa(); vD(); wex(); wb(); vB(); wal(); wi(); vD(); wex();
} else if (t2 == 14) {
/* axpownd: (-. x = y -> E. x A. y (A. x (E. z x e. y -> A. y x e. z) -> y e. x )) */
vA(); vB(); weq(); wn(); vA(); vB(); wel(); vC(); wex(); vA(); vC(); wel();
vB(); wal(); wi(); vA(); wal(); vB(); vA(); wel(); wi(); vB(); wal(); vA(); wex(); wi();
} else if (t2 == 15) {
/* axunnd: E. x A. y (E. x (y e. x /\ x e. z) -> y e. x ) */
vA(); vB(); wel(); vB(); vC(); wel(); wa(); vB(); wex(); vA(); vB(); wel(); wi(); vA(); wal(); vB(); wex();
} else if (t2 == 22) {
/* axregnd: ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) */
vA(); vB(); wel(); vA(); vB(); wel(); vC(); vA(); wel(); vC(); vB(); wel(); wn(); wi(); vC(); wal(); wa(); vA(); wex(); wi();
} else if (t2 == 16) {
/* axinfnd: E. x (y e. z -> (y e. x /\ A. y (y e. x -> E. z(y e. z /\ z e. x )))) */
vA(); vB(); wel(); vA(); vC(); wel(); vA(); vC(); wel(); vA(); vB(); wel(); vB(); vC(); wel();
wa(); vB(); wex(); wi(); vA(); wal(); wa(); wi(); vC(); wex();
} else if (t2 == 17) {
/* dtru: -. A. x x = y */
vA(); vB(); isne();
vA(); vB(); weq(); vA(); wal(); wn();
} else {
valid = 0;
}
pop(proof, pstack);
}
int nextproof;
valid = 0;
while (valid == 0) {
valid = 1;
wstack = 0;
t2 = 1;
push(wstack, t2);
push(wstack, t2);
weq();
wn();
/* we just pushed -. v0 = v0 , which should not be provable */
push(wstack, nextproof);
verify();
iseq();
nextproof = nextproof + 1;
/* if we're valid here, we found a contradiction in ZF */
}
halt;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment