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.
** Module lib_logic Imports parameters ** Config Infix /\ left 3 ** Config Infix \/ left 2 cut = ... : {A,B|Prop}A->(A->B)->B trueProp = ... : Prop Id = ... : {T|SET}T->T PropId = ... : {A|Prop}A->A Contrapos = ... : {A,B|Prop}(A->B)->{X|Prop}(B->X)->A->X compose = ... : {T,S,U|SET}(S->U)->(T->S)->T->U permute = ... : {T,S,U|SET}(T->S->U)->S->T->U forall_elim = ... : {C|Prop}{T|SET}{P:T->Prop}({x:T}P x)->{e:T}((P e)->C)->C impl_elim = ... : {A,B,C|Prop}(A->B)->A->(B->C)->C and = ... : Prop->Prop->Prop or = ... : Prop->Prop->Prop or_elim = ... : {A,B,C|Prop}(A \/ B)->(A->C)->(B->C)->C pair = ... : {A,B|Prop}A->B->(A /\ B) inl = ... : {A,B|Prop}A->(A \/ B) inr = ... : {A,B|Prop}B->(A \/ B) fst = ... : {A,B|Prop}(A /\ B)->A snd = ... : {A,B|Prop}(A /\ B)->B iff = ... : Prop->Prop->Prop absurd = ... : Prop absurd_elim = ... : absurd->{N:Prop}N not = ... : Prop->Prop All = ... : {T|SET}(T->Prop)->Prop Ex = ... : {T|SET}(T->Prop)->Prop ExIntro = ... : {T|SET}{wit:T}{P:T->Prop}(P wit)->Ex P ExIn = ... : {T|SET}{wit:T}{P:T->Prop}(P wit)->{B:Prop}({t:T}(P t)->B)->B ExElim = ... : {T|SET}{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,S|SET}(T->S->Prop)->Prop Ex2Intro = ... : {T,S|SET}{P:T->S->Prop}{t|T}{s|S}(P t s)->Ex2 P Ex2Elim = ... : {T,S|SET}{P|T->S->Prop}(Ex2 P)->{N|Prop}({t|T}{s|S}(P t s)->N)->N Ex2In = ... : {T,S|SET}{t:T}{s:S}{P:T->S->Prop}(P t s)->Ex2 P Ex3 = ... : {T,S,U|SET}(T->S->U->Prop)->Prop Ex3In = ... : {T,S,U|SET}{t:T}{s:S}{u:U}{P:T->S->U->Prop}(P t s u)->Ex3 P Ex3Elim = ... : {T,S,U|SET}{P|T->S->U->Prop}(Ex3 P)->{N|Prop} ({t|T}{s|S}{u|U}(P t s u)->N)->N Ex4 = ... : {T,S,U,V|SET}(T->S->U->V->Prop)->Prop Ex4In = ... : {T,S,U,V|SET}{t:T}{s:S}{u:U}{v:V}{P:T->S->U->V->Prop}(P t s u v)-> Ex4 P Ex4Elim = ... : {T,S,U,V|SET}{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,S,U,V,W|SET}(T->S->U->V->W->Prop)->Prop Ex5In = ... : {T,S,U,V,W|SET}{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,S,U,V,W|SET}{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,S,U,V,W,X|SET}(T->S->U->V->W->X->Prop)->Prop Ex6In = ... : {T,S,U,V,W,X|SET}{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,S,U,V,W,X|SET}{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|SET}(T->T->Prop)->Prop sym = ... : {T|SET}(T->T->Prop)->Prop trans = ... : {T|SET}(T->T->Prop)->Prop Equivalence = ... : {T|SET}(T->T->Prop)->Prop respect = ... : {T,S|SET}(T->S)->({X|SET}X->X->Prop)->Prop respect2 = ... : {T,S,U|SET}(T->U->S)->({X|SET}X->X->Prop)->Prop