#!/usr/local/bin/aut { ----------------------------- meta logic -------------------------------8-- } * typ : TYPE := PRIM * [tau:typ] term : TYPE := PRIM tau * [tau':typ] fun : typ := PRIM * prop : typ := PRIM tau' * [t:[x,term(tau)]term(tau')] lambda {Abs} : term(fun(tau,tau')) := PRIM tau' * [t:term(fun(tau,tau'))][t':term(tau)] app {$} : term(tau') := PRIM * [alpha:typ] all : term(fun(fun(alpha,prop),prop)) := PRIM * imp {==>} : term(fun(prop,fun(prop,prop))) := PRIM alpha * [P:term(fun(alpha,prop))] all' : term(prop) := app(fun(alpha,prop),prop,all,P) * [phi:term(prop)][psi:term(prop)] imp' : term(prop) := app(prop,prop,app(prop,fun(prop,prop),imp,phi),psi) { ----------------------------- proof terms ------------------------------5-- } phi * proof : TYPE := PRIM psi * [p:[h,proof(phi)]proof(psi)] imp_intro {AbsP} : proof(imp'(phi,psi)) := PRIM psi * [p:proof(imp'(phi,psi))][q:proof(phi)] imp_elim {%%} : proof(psi) := PRIM tau * [phi:[x,term(tau)]term(prop)][p:[x,term(tau)]proof(phi)] all_intro {Abst} : proof(all'(tau,lambda(tau,prop,phi))) := PRIM phi * [p:proof(all'(tau,lambda(tau,prop,phi)))][t:term(tau)] all_elim {%} : proof(phi) := PRIM { ----------------------------- equality --------------------------------10-- } tau * eq {==} : term(fun(tau,fun(tau,prop))) := PRIM tau * [a:term(tau)][b:term(tau)] eq' : term(prop) := app(tau,prop,app(tau,fun(tau,prop),eq,a),b) * [phi:term(prop)][psi:term(prop)] [_1:proof(imp'(phi,psi))][_2:proof(imp'(psi,phi))] eq_intro : proof(eq'(prop,phi,psi)) := PRIM psi * [_1:proof(eq'(prop,phi,psi))][_2:proof(phi)] eq_elim : proof(psi) := PRIM a * refl : proof(eq'(a,a)) := PRIM b * [_1:proof(eq'(a,b))] sym : proof(eq'(b,a)) := PRIM b * [c:term(tau)][_1:proof(eq'(a,b))][_2:proof(eq'(b,c))] trans : proof(eq'(a,c)) := PRIM tau' * [a:[x,term(tau)]term(tau')][b:term(tau)] beta : proof(eq'(tau',app(lambda(a),b),a)) := PRIM tau' * [f:term(fun(tau,tau'))][g:term(fun(tau,tau'))] [_1:[x:term(tau)]proof(eq'(tau',app(f,x),app(g,x)))] ext : proof(eq'(fun(tau,tau'),f,g)) := PRIM a * [b:[x,term(tau)]term(tau')][_1:[x,term(tau)]proof(eq'(tau',a,b))] abs : proof(eq'(fun(tau,tau'),lambda(a),lambda(b))) := PRIM g * [a:term(tau)][b:term(tau)] [_1:proof(eq'(fun(tau,tau'),f,g))][_2:proof(eq'(a,b))] comb : proof(eq'(tau',app(f,a),app(g,b))) := PRIM