The logic file contains impredicative encodings of ``and'', ``or'' ``exists'', etc. and their introduction and elimination rules, and definitions of some properties of relations (symmetry, reflexivity etc.). It is based on Randy Pollack's logic file. For the convenience of some of our users we have included definitions of ``and'' and ``exists'' which take up to 7 arguments; we omit those with more than 3 arguments from this report.
** Module lib_logic Imports parameters cut = ... : {A,B|Prop}A->(A->B)->B trueProp = ... : Prop Id = ... : {T|Type}T->T PropId = ... : {A|Prop}A->A Contrapos = ... : {A,B|Prop}(A->B)->{X|Prop}(B->X)->A->X compose = ... : {T|Type}{S|Type}{U|Type}(S->U)->(T->S)->T->U permute = ... : {T|Type}{S|Type}{U|Type}(T->S->U)->S->T->U and = ... : Prop->Prop->Prop or = ... : Prop->Prop->Prop or_elim = ... : {A,B,C|Prop}(or A B)->(A->C)->(B->C)->C pair = ... : {A,B|Prop}A->B->and A B inl = ... : {A,B|Prop}A->or A B inr = ... : {A,B|Prop}B->or A B fst = ... : {A,B|Prop}(and A B)->A snd = ... : {A,B|Prop}(and A B)->B iff = ... : Prop->Prop->Prop absurd = ... : Prop absurd_elim = ... : absurd->{N:Prop}N not = ... : Prop->Prop All = ... : {T|Type}(T->Prop)->Prop Ex = ... : {T|Type}(T->Prop)->Prop ExIntro = ... : {T|Type}{wit:T}{P:T->Prop}(P wit)->Ex P ExIn = ... : {T|Type}{wit:T}{P:T->Prop}(P wit)->{B:Prop}({t:T}(P t)->B)->B ExElim = ... : {T|Type}{P|T->Prop}(Ex P)->{N|Prop}({t:T}(P t)->N)->N ex = ... : {A|Prop}(A->Prop)->Prop ex_intro = ... : {A|Prop}{P:A->Prop}{wit|A}(P wit)->ex P witness = ... : {A|Prop}{P|A->Prop}(ex P)->A Ex2 = ... : {T|Type}{S|Type}(T->S->Prop)->Prop Ex2Intro = ... : {T|Type}{S|Type}{P:T->S->Prop}{t|T}{s|S}(P t s)->Ex2 P Ex2Elim = ... : {T|Type}{S|Type}{P|T->S->Prop}(Ex2 P)->{N|Prop} ({t|T}{s|S}(P t s)->N)->N Ex2In = ... : {T|Type}{S|Type}{t:T}{s:S}{P:T->S->Prop}(P t s)->Ex2 P Ex3 = ... : {T|Type}{S|Type}{U|Type}(T->S->U->Prop)->Prop Ex3In = ... : {T|Type}{S|Type}{U|Type}{t:T}{s:S}{u:U}{P:T->S->U->Prop}(P t s u)-> Ex3 P Ex3Elim = ... : {T|Type}{S|Type}{U|Type}{P|T->S->U->Prop}(Ex3 P)->{N|Prop} ({t|T}{s|S}{u|U}(P t s u)->N)->N Ex4 = ... : {T|Type}{S|Type}{U|Type}{V|Type}(T->S->U->V->Prop)->Prop Ex4In = ... : {T|Type}{S|Type}{U|Type}{V|Type}{t:T}{s:S}{u:U}{v:V} {P:T->S->U->V->Prop}(P t s u v)->Ex4 P Ex4Elim = ... : {T|Type}{S|Type}{U|Type}{V|Type}{P|T->S->U->V->Prop}(Ex4 P)-> {N|Prop}({t|T}{s|S}{u|U}{v|V}(P t s u v)->N)->N Ex5 = ... : {T|Type}{S|Type}{U|Type}{V|Type}{W|Type}(T->S->U->V->W->Prop)->Prop Ex5In = ... : {T|Type}{S|Type}{U|Type}{V|Type}{W|Type}{t:T}{s:S}{u:U}{v:V}{w:W} {P:T->S->U->V->W->Prop}(P t s u v w)->Ex5 P Ex5Elim = ... : {T|Type}{S|Type}{U|Type}{V|Type}{W|Type}{P|T->S->U->V->W->Prop} (Ex5 P)->{N|Prop}({t|T}{s|S}{u|U}{v|V}{w|W}(P t s u v w)->N)->N Ex6 = ... : {T|Type}{S|Type}{U|Type}{V|Type}{W|Type}{X|Type} (T->S->U->V->W->X->Prop)->Prop Ex6In = ... : {T|Type}{S|Type}{U|Type}{V|Type}{W|Type}{X|Type}{t:T}{s:S}{u:U}{v:V} {w:W}{x:X}{P:T->S->U->V->W->X->Prop}(P t s u v w x)->Ex6 P Ex6Elim = ... : {T|Type}{S|Type}{U|Type}{V|Type}{W|Type}{X|Type} {P|T->S->U->V->W->X->Prop}(Ex6 P)->{N|Prop} ({t|T}{s|S}{u|U}{v|V}{w|W}{x|X}(P t s u v w x)->N)->N and3 = ... : Prop->Prop->Prop->Prop pair3 = ... : {A,B,C|Prop}A->B->C->and3 A B C and3_out1 = ... : {A,B,C|Prop}(and3 A B C)->A and3_out2 = ... : {A,B,C|Prop}(and3 A B C)->B and3_out3 = ... : {A,B,C|Prop}(and3 A B C)->C and4 = ... : Prop->Prop->Prop->Prop->Prop pair4 = ... : {A,B,C,D|Prop}A->B->C->D->and4 A B C D and4_out1 = ... : {A,B,C,D|Prop}(and4 A B C D)->A and4_out2 = ... : {A,B,C,D|Prop}(and4 A B C D)->B and4_out3 = ... : {A,B,C,D|Prop}(and4 A B C D)->C and4_out4 = ... : {A,B,C,D|Prop}(and4 A B C D)->D and5 = ... : Prop->Prop->Prop->Prop->Prop->Prop pair5 = ... : {A,B,C,D,E|Prop}A->B->C->D->E->and5 A B C D E and5_out1 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->A and5_out2 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->B and5_out3 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->C and5_out4 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->D and5_out5 = ... : {A,B,C,D,E|Prop}(and5 A B C D E)->E and6 = ... : Prop->Prop->Prop->Prop->Prop->Prop->Prop pair6 = ... : {A,B,C,D,E,F|Prop}A->B->C->D->E->F->and6 A B C D E F and6_out1 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->A and6_out2 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->B and6_out3 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->C and6_out4 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->D and6_out5 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->E and6_out6 = ... : {A,B,C,D,E,F|Prop}(and6 A B C D E F)->F and7 = ... : Prop->Prop->Prop->Prop->Prop->Prop->Prop->Prop pair7 = ... : {A,B,C,D,E,F,G|Prop}A->B->C->D->E->F->G->and7 A B C D E F G and7_out1 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->A and7_out2 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->B and7_out3 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->C and7_out4 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->D and7_out5 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->E and7_out6 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->F and7_out7 = ... : {A,B,C,D,E,F,G|Prop}(and7 A B C D E F G)->G iff3 = ... : Prop->Prop->Prop->Prop or3 = ... : Prop->Prop->Prop->Prop or3_in1 = ... : {A,B,C|Prop}A->or3 A B C or3_in2 = ... : {A,B,C|Prop}B->or3 A B C or3_in3 = ... : {A,B,C|Prop}C->or3 A B C or3_elim = ... : {A,B,C,X|Prop}(or3 A B C)->(A->X)->(B->X)->(C->X)->X refl = ... : {T|Type}(T->T->Prop)->Prop sym = ... : {T|Type}(T->T->Prop)->Prop trans = ... : {T|Type}(T->T->Prop)->Prop Equivalence = ... : {T|Type}(T->T->Prop)->Prop respect = ... : {T|Type}{S|Type}(T->S)->({X|Type}X->X->Prop)->Prop respect2 = ... : {T|Type}{S|Type}{U|Type}(T->U->S)->({X|Type}X->X->Prop)->Prop