#!/usr/local/bin/aut { ----------------------------- the types --------------------------------3-- } * prop : TYPE := PRIM * [a:prop] proof : TYPE := PRIM * set : TYPE := PRIM { ----------------------------- first order logic ------------------------5-- } * 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 * or : prop := imp(not(a),b) b * iff : prop := and(imp(a,b),imp(b,a)) p * ex : prop := not(for([z,set]not(p))) p * unique : prop := for([z,set]imp(p,for([z',set]imp(p,eq(z,z'))))) p * ex_unique : prop := and(ex,unique) { ----------------------------- natural deduction ------------------------7-- } # a * [_:proof(a)][_':proof(a)][h:[_,proof(a)]prop][_1:proof(<_>h)] # irrelevance : proof(<_'>h) := PRIM 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 { ----------------------------- definition by cases ----------------------2-- } y * [c:prop] cases : set := PRIM c * cases_axiom : proof(and(imp(c,eq(cases(x,y,c),x)),imp(not(c),eq(cases(x,y,c),y)))) := PRIM { ----------------------------- set theory -------------------------------6-- } * empty : set := PRIM y * double : set := PRIM # {x,y} x * unions : set := PRIM x * powerset : set := PRIM x * [f:[z,set]set] replace : set := PRIM * omega : set := PRIM x * single : set := double(x,x) x * [q:[z,set]prop] restrict : set := unions(replace(x,[z,set]cases(single(z),empty,q))) y * inter : set := restrict(x,[z,set]in(z,y)) y * union : set := unions(double(x,y)) x * succ : set := union(x,single(x)) y * subset : prop := for([z,set]imp(in(z,x),in(z,y))) y * disjoint : prop := eq(inter(x,y),empty) x * omega_closed : prop := and(in(empty,x),for([n,set]imp(in(n,x),in(succ(n),x)))) { ----------------------------- the axioms -------------------------------8-- } y * extensionality : proof(iff(eq(x,y),for([z,set]iff(in(z,x),in(z,y))))) := PRIM x * foundation : proof(imp(not(eq(x,empty)),ex([z,set]and(in(z,x),disjoint(z,x))))) := PRIM * empty_axiom : proof(for([z,set]not(in(z,empty)))) := PRIM y * double_axiom : proof(for([z,set]iff(in(z,double(x,y)),or(eq(z,x),eq(z,y))))) := PRIM x * unions_axiom : proof(for([z,set]iff(in(z,unions(x)),ex([y,set]and(in(z,y),in(y,x)))))) := PRIM x * powerset_axiom : proof(for([z,set]iff(in(z,powerset(x)),subset(z,x)))) := PRIM f * replace_axiom : proof(for([z,set]iff(in(z,replace(x,f)),ex([y,set]and(in(y,x),eq(z,f)))))) := PRIM * omega_axiom : proof(and(omega_closed(omega), for([o,set]imp(omega_closed(o),subset(omega,o))))) := PRIM { ----------------------------- choice -----------------------------------1-- } * AC : proof(for([x,set]imp( and(for([y,set]imp(in(y,x),not(eq(y,empty)))), for([y1,set]imp(in(y1,x),for([y2,set]imp(in(y2,x), or(eq(y1,y2),disjoint(y1,y2))))))), ex([x',set]for([y,set]imp(in(y,x),ex_unique([y',set] and(in(y',x'),in(y',y))))))))) := PRIM