#!/usr/local/bin/aut { ----------------------------- many-sorted first order logic -----------15-- } * prop : TYPE := PRIM * [a:prop] proof : TYPE := PRIM * sort : TYPE := PRIM * [s:sort] elt : TYPE := PRIM * false : prop := PRIM a * [b:prop] imp : prop := PRIM s * [p:[z,elt(s)]prop] for : prop := PRIM s * [x:elt(s)][y:elt(s)] eq : 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,elt(s)]not(p))) p * unique : prop := for([z,elt(s)]imp(p,for([z',elt(s)]imp(p,eq(z,z'))))) p * ex_unique : prop := and(ex,unique) b * [_1:[_,proof(a)]proof(b)] imp_intro : proof(imp(a,b)) := PRIM b * [_1:proof(imp(a,b))][_2:proof(a)] imp_elim : proof(b) := PRIM p * [_1:[z,elt(s)]proof(p)] for_intro : proof(for(p)) := PRIM p * [_1:proof(for(p))][z:elt(s)] for_elim : proof(p) := PRIM a * [_1:proof(not(not(a)))] classical : proof(a) := PRIM x * eq_intro : proof(eq(x,x)) := PRIM y * [_1:proof(eq(x,y))][q:[z,elt(s)]prop][_2:proof(q)] eq_elim : proof(q) := PRIM { ----------------------------- category theory --------------------------8-- } * object_sort : sort := PRIM * arrow_sort : sort := PRIM * object : TYPE := elt(object_sort) * arrow : TYPE := elt(arrow_sort) * [p:[A:object]prop] for_object : prop := for(object_sort,p) ex_object : prop := ex(object_sort,p) * [p:[A:arrow]prop] for_arrow : prop := for(arrow_sort,p) ex_arrow : prop := ex(arrow_sort,p) ex_unique_arrow : prop := ex_unique(arrow_sort,p) * [f:arrow][g:arrow] eq_arrow : prop := eq(arrow_sort,f,g) * [A:object] Id : arrow := PRIM * [f:arrow][A:object][B:object] maps : prop := PRIM f * [g:arrow][h:arrow] comp : prop := PRIM * [f:arrow][A:object][B:object] axiom_1 : proof(imp(maps(f,A,B),and(comp(f,Id(A),f),comp(Id(B),f,f)))) := PRIM f * [g:arrow] axiom_2 : proof(iff(ex_object([A,object]ex_object([B,object]ex_object([C,object] and(maps(f,A,B),maps(g,B,C))))), ex_arrow([h,arrow]comp(g,f,h)))) := PRIM g * [h:arrow][k:arrow][i:arrow][j:arrow] axiom_3 : proof(imp(and(comp(g,f,k),and(comp(h,k,j),comp(h,g,i))), comp(i,f,j))) := PRIM { ----------------------------- terminal object and cartesian products ---9-- } * 1 : object := PRIM * [A:object][B:object] prod_object : object := PRIM g * prod_arrow : arrow := PRIM B * p1 : arrow := PRIM p2 : arrow := PRIM A * axiom_4 : proof(ex_unique_arrow([f,arrow]maps(f,A,1))) := PRIM B * axiom_5 : proof(and(maps(p1(A,B),prod_object(A,B),A),maps(p2(A,B),prod_object(A,B),B))) := PRIM g * [A:object][B:object][T:object] axiom_6 : proof(imp(and(maps(f,T,A),maps(g,T,B)), ex_unique_arrow([u,arrow]and(maps(u,T,prod_object(A,B)), and(comp(p1(A,B),u,f),comp(p2(A,B),u,g)))))) := PRIM B * [C:object][D:object] axiom_7 : proof(imp(and(maps(f,A,B),maps(g,C,D)), and(maps(prod_arrow(f,g),prod_object(A,C),prod_object(B,D)), for_arrow([h,arrow]for_arrow([k,arrow] imp(and(comp(f,p1(A,C),h),comp(g,p2(A,C),k)), and(comp(p1(B,D),prod_arrow(f,g),h), comp(p2(B,D),prod_arrow(f,g),k)))))))) := PRIM { ----------------------------- non-trivial Boolean topos ---------------10-- } * 2 : object := PRIM * i1 : arrow := PRIM i2 : arrow := PRIM * [A:object][B:object] funcs : object := PRIM B * eval : arrow := PRIM f * monic : prop := PRIM # axiom_8 f * [A:object][B:object][T:object] axiom_9 : proof(imp(maps(f,prod_object(T,A),B), ex_unique_arrow([u,arrow]and(maps(u,T,funcs(A,B)), comp(eval(A,B),prod_arrow(u,Id(A)),f))))) := PRIM g * [A:object] axiom_10 : proof(and(not(eq_arrow(i1,i2)),imp(and(maps(f,1,A),maps(g,1,A)), ex_unique_arrow([u,arrow]and(maps(u,1,A), and(comp(u,i1,g),comp(u,i2,g))))))) := PRIM f * axiom_11 : proof(iff(monic(f),for_arrow([g,arrow]for_arrow([h,arrow]for_arrow([k,arrow] imp(and(comp(f,g,k),comp(f,h,k)),eq_arrow(g,h))))))) := PRIM f * [A:object][B:object][u:arrow][h:arrow][k:arrow][j:arrow] axiom_12 : proof(and(imp(and(monic(f),maps(f,A,B)), ex_unique_arrow([u,arrow]and(maps(u,B,2), for_arrow([h,arrow]for_arrow([k,arrow]for_arrow([j,arrow] imp(and(comp(i1,k,j),comp(u,h,j)), ex_unique_arrow([v,arrow]comp(f,v,h))))))))), imp(and(maps(u,B,2),and(comp(i1,k,j),comp(u,h,j))), ex_unique_arrow([v,arrow]comp(f,v,h))))) := PRIM { ----------------------------- natural numbers --------------------------1-- } * axiom_13 : proof(ex_object([N,object]ex_arrow([0,arrow]ex_arrow([s,arrow] and(and(maps(0,1,N),maps(s,N,N)), for_object([A,object]for_arrow([x,arrow]for_arrow([f,arrow] imp(and(maps(x,1,A),maps(f,A,A)), ex_unique_arrow([u,arrow]and(maps(u,N,A), ex_arrow([h,arrow]ex_arrow([k,arrow] and(comp(u,0,x),and(comp(u,s,k),comp(f,u,k)))))))))))))))) := PRIM { ----------------------------- well-pointed topos with choice -----------2-- } g * [A:object][B:object] axiom_14 : proof(imp(and(and(maps(f,A,B),maps(g,A,B)), for_arrow([k,arrow]for_arrow([h,arrow]imp(maps(h,1,A), iff(comp(f,h,k),comp(g,h,k)))))), eq_arrow(f,g))) := PRIM f * [A:object][B:object] axiom_15 : proof(imp(and(maps(f,A,B), for_arrow([h,arrow]imp(maps(h,1,B), ex_arrow([k,arrow]and(maps(k,1,A),comp(f,k,h)))))), ex_arrow([g,arrow]and(maps(g,B,A),comp(f,g,Id(B)))))) := PRIM