#!/usr/local/bin/aut { ----------------------------- first order logic -----------------------15-- } * prop : TYPE := PRIM * [a:prop] proof : TYPE := PRIM * set : TYPE := PRIM * false : prop := PRIM a * [b:prop] imp : prop := PRIM * [p:[z,set]prop] for : prop := PRIM * [x:set][y:set] eq : prop := PRIM y * in : prop := PRIM a * not : prop := imp(a,false) b * and : prop := not(imp(a,not(b))) b * iff : prop := and(imp(a,b),imp(b,a)) p * ex : prop := not(for([z,set]not(p))) b * [_:[_1,proof(a)]proof(b)] imp_intro : proof(imp(a,b)) := PRIM b * [_:proof(imp(a,b))][_1:proof(a)] imp_elim : proof(b) := PRIM p * [_:[z,set]proof(p)] for_intro : proof(for(p)) := PRIM p * [_:proof(for(p))][z:set] for_elim : proof(p) := PRIM a * [_:proof(not(not(a)))] classical : proof(a) := PRIM x * eq_intro : proof(eq(x,x)) := PRIM y * [_:proof(eq(x,y))][q:[z,set]prop][_1:proof(q)] eq_elim : proof(q) := PRIM { ----------------------------- stratification levels --------------------3-- } * nat : TYPE := PRIM * 0 : nat := PRIM * [n:nat] S : nat := PRIM { ----------------------------- stratified formulas ---------------------14-- } * prop' : TYPE := PRIM n * set' : TYPE := PRIM * false' : prop' := PRIM * [a':prop'][b':prop'] imp' : prop' := PRIM n * [p':[z',set'(n)]prop'] for' : prop' := PRIM n * [x':set'(n)][y':set'(n)] eq' : prop' := PRIM n * [x':set'(n)][y':set'(S(n))] in' : prop' := PRIM a * [a':prop'] same_prop : TYPE := PRIM n * [x:set][x':set'(n)] same_set : TYPE := PRIM * same_false : same_prop(false,false') := PRIM a' * [_1:same_prop(a,a')][b:prop][b':prop'][_2:same_prop(b,b')] same_imp : same_prop(imp(a,b),imp'(a',b')) := PRIM n * [p:[z,set]prop][p':[z',set'(n)]prop'] [_1:[z,set][z',set'(n)][_:same_set(n,z,z')]same_prop(p,p')] same_for : same_prop(for(p),for'(n,p')) := PRIM n * [x:set][x':set'(n)][_1:same_set(n,x,x')][y:set] [y':set'(n)][_2:same_set(n,y,y')] same_eq : same_prop(eq(x,y),eq'(n,x',y')) := PRIM y * [y':set'(S(n))][_2:same_set(S(n),y,y')] same_in : same_prop(in(x,y),in'(n,x',y')) := PRIM { ----------------------------- new foundations --------------------------5-- } * [y:set][z:set] axiom_1 : proof(imp(for([x,set]iff(in(x,y),in(x,z))),eq(y,z))) := PRIM # n * [phi:[x,set]prop][phi':[x',set'(n)]prop'] # [_1:[x,set][x',set'(n)][_,same_set(n,x,x')]same_prop(phi,phi')] # axiom_2 : proof(ex([A,set]for([x,set]iff(in(x,A),phi)))) := PRIM a * axiom_scheme : TYPE := PRIM * [phi:[x,set]prop] axiom_base : axiom_scheme(ex([A,set]for([x,set]iff(in(x,A),phi)))) := PRIM * [p:[z,set]prop][_1:[z,set]axiom_scheme(p)] axiom_for : axiom_scheme(for(p)) := PRIM a' * [_1:axiom_scheme(a)][_2:same_prop(a,a')] axiom_2 : proof(a) := PRIM