:: Intuitionistic Propositional Calculus in the Extended Framework with Modal :: Operator, Part I :: by Takao Inou\'e :: :: Received April 3, 2003 :: Copyright (c) 2003-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, QC_LANG2, XBOOLEAN, INTPRO_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1; constructors NAT_1, FINSEQ_1, NUMBERS; registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1, NAT_1, XCMPLX_0; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI; expansions TARSKI; theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1; schemes XBOOLE_0; begin :: Intuitionistic propositional calculus IPC in the extended :: language with modal operator definition let E be set; attr E is with_FALSUM means :Def1: <*0*>in E; end; definition let E be set; attr E is with_int_implication means :Def2: for p, q being FinSequence st p in E & q in E holds <*1*>^p^q in E; end; definition let E be set; attr E is with_int_conjunction means :Def3: for p, q being FinSequence st p in E & q in E holds <*2*>^p^q in E; end; definition let E be set; attr E is with_int_disjunction means :Def4: for p, q being FinSequence st p in E & q in E holds <*3*>^p^q in E; end; definition let E be set; attr E is with_int_propositional_variables means :Def5: for n being Element of NAT holds <* 5+2*n *> in E; end; definition let E be set; attr E is with_modal_operator means :Def6: for p being FinSequence st p in E holds <*6*>^p in E; end; :: We reserve <*4*> for verum for a possible formulation. :: So do we <* 5+2*n+1 *> for every n >= 1 for introduction of a number of :: other logical connectives (e.g. for polymodal logics, :: hybrid logics, recent computer-oriented logics and so on). definition let E be set; attr E is MC-closed means :Def7: E c= NAT* & E is with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator; end; Lm1: for E be set st E is MC-closed holds E is non empty proof let E be set; assume E is MC-closed; then E is with_FALSUM; hence thesis; end; registration cluster MC-closed -> with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator non empty for set; coherence by Lm1; cluster with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator -> MC-closed for Subset of NAT*; coherence; end; definition func MC-wff -> set means :Def8: it is MC-closed & for E being set st E is MC-closed holds it c= E; existence proof A1: <*0*> in NAT* by FINSEQ_1:def 11; defpred P[object] means for E being set st E is MC-closed holds \$1 in E; consider E0 being set such that A2: for x being object holds x in E0 iff x in NAT* & P[x] from XBOOLE_0: sch 1; A3: for E being set st E is MC-closed holds <*0*> in E by Def1; then reconsider E0 as non empty set by A2,A1; take E0; A4: E0 c= NAT* by A2; for p being FinSequence st p in E0 holds <*6*>^p in E0 proof let p be FinSequence such that A5: p in E0; p in NAT* by A2,A5; then reconsider p9=p as FinSequence of NAT by FINSEQ_1:def 11; A6: for E being set st E is MC-closed holds <*6*>^p in E proof let E be set; assume A7: E is MC-closed; then p in E by A2,A5; hence thesis by A7,Def6; end; <*6*>^p9 in NAT* by FINSEQ_1:def 11; hence thesis by A2,A6; end; then A8: E0 is with_modal_operator; for n being Element of NAT holds <* 5+2*n *> in E0 proof let n be Element of NAT; set p = 5+2*n; reconsider h = <*p*> as FinSequence of NAT; A9: h in NAT* by FINSEQ_1:def 11; for E being set st E is MC-closed holds <*p*> in E by Def5; hence thesis by A2,A9; end; then A10: E0 is with_int_propositional_variables; for p, q being FinSequence st p in E0 & q in E0 holds <*3*>^p^q in E0 proof let p, q be FinSequence such that A11: p in E0 and A12: q in E0; A13: q in NAT* by A2,A12; A14: for E being set st E is MC-closed holds <*3*>^p^q in E proof let E be set; assume A15: E is MC-closed; then A16: q in E by A2,A12; p in E by A2,A11,A15; hence thesis by A15,A16,Def4; end; p in NAT* by A2,A11; then reconsider p9=p, q9=q as FinSequence of NAT by A13,FINSEQ_1:def 11; <*3*>^p9^q9 in NAT* by FINSEQ_1:def 11; hence thesis by A2,A14; end; then A17: E0 is with_int_disjunction; for p, q being FinSequence st p in E0 & q in E0 holds <*2*>^p^q in E0 proof let p, q be FinSequence such that A18: p in E0 and A19: q in E0; A20: q in NAT* by A2,A19; A21: for E being set st E is MC-closed holds <*2*>^p^q in E proof let E be set; assume A22: E is MC-closed; then A23: q in E by A2,A19; p in E by A2,A18,A22; hence thesis by A22,A23,Def3; end; p in NAT* by A2,A18; then reconsider p9=p, q9=q as FinSequence of NAT by A20,FINSEQ_1:def 11; <*2*>^p9^q9 in NAT* by FINSEQ_1:def 11; hence thesis by A2,A21; end; then A24: E0 is with_int_conjunction; for p, q being FinSequence st p in E0 & q in E0 holds <*1*>^p^q in E0 proof let p, q be FinSequence such that A25: p in E0 and A26: q in E0; A27: q in NAT* by A2,A26; A28: for E being set st E is MC-closed holds <*1*>^p^q in E proof let E be set; assume A29: E is MC-closed; then A30: q in E by A2,A26; p in E by A2,A25,A29; hence thesis by A29,A30,Def2; end; p in NAT* by A2,A25; then reconsider p9=p, q9=q as FinSequence of NAT by A27,FINSEQ_1:def 11; <*1*>^p9^q9 in NAT* by FINSEQ_1:def 11; hence thesis by A2,A28; end; then A31: E0 is with_int_implication; <*0*> in E0 by A2,A1,A3; then E0 is with_FALSUM; hence E0 is MC-closed by A4,A10,A31,A24,A17,A8; let E be set such that A32: E is MC-closed; let x be object; assume x in E0; hence thesis by A2,A32; end; uniqueness proof let E1, E2 be set such that A33: E1 is MC-closed and A34: for E being set st E is MC-closed holds E1 c= E and A35: E2 is MC-closed and A36: for E being set st E is MC-closed holds E2 c= E; A37: E2 c= E1 by A33,A36; E1 c= E2 by A34,A35; hence thesis by A37,XBOOLE_0:def 10; end; end; registration cluster MC-wff -> MC-closed; coherence by Def8; end; registration cluster MC-closed non empty for set; existence proof take MC-wff; thus thesis; end; end; registration cluster MC-wff -> functional; coherence proof MC-wff c= NAT* by Def7; hence thesis; end; end; registration cluster -> FinSequence-like for Element of MC-wff; coherence proof let p be Element of MC-wff; MC-wff c= NAT* by Def7; hence thesis; end; end; definition mode MC-formula is Element of MC-wff; end; definition func FALSUM -> MC-formula equals <*0*>; correctness by Def1; let p, q be Element of MC-wff; func p => q -> MC-formula equals <*1*>^p^q; correctness by Def2; func p '&' q -> MC-formula equals <*2*>^p^q; correctness by Def3; func p 'or' q -> MC-formula equals <*3*>^p^q; correctness by Def4; end; definition let p be Element of MC-wff; func Nes p -> MC-formula equals <*6*>^p; correctness by Def6; end; reserve T, X, Y for Subset of MC-wff; reserve p, q, r, s for Element of MC-wff; definition let T be Subset of MC-wff; attr T is IPC_theory means :Def14: for p, q, r being Element of MC-wff holds p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & (p in T & p => q in T implies q in T); correctness; end; definition let X; func CnIPC X -> Subset of MC-wff means :Def15: r in it iff for T st T is IPC_theory & X c= T holds r in T; existence proof defpred P[object] means for T st T is IPC_theory & X c= T holds \$1 in T; consider Y being set such that A1: for a being object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0: sch 1; Y c= MC-wff by A1; then reconsider Z = Y as Subset of MC-wff; take Z; thus thesis by A1; end; uniqueness proof let Y,Z be Subset of MC-wff such that A2: r in Y iff for T st T is IPC_theory & X c= T holds r in T and A3: r in Z iff for T st T is IPC_theory & X c= T holds r in T; for a being object holds a in Y iff a in Z proof let a be object; hereby assume A4: a in Y; then reconsider t=a as Element of MC-wff; for T st T is IPC_theory & X c= T holds t in T by A2,A4; hence a in Z by A3; end; assume A5: a in Z; then reconsider t=a as Element of MC-wff; for T st T is IPC_theory & X c= T holds t in T by A3,A5; hence thesis by A2; end; hence thesis by TARSKI:2; end; end; definition func IPC-Taut -> Subset of MC-wff equals CnIPC({}(MC-wff)); correctness; end; definition let p be Element of MC-wff; func neg p -> MC-formula equals (p => FALSUM); correctness; end; definition func IVERUM -> MC-formula equals (FALSUM => FALSUM); correctness; end; theorem Th1: p => (q => p) in CnIPC (X) proof T is IPC_theory & X c= T implies p => (q => p) in T; hence thesis by Def15; end; theorem Th2: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) proof T is IPC_theory & X c= T implies (p => (q => r)) => ((p => q) => (p => r )) in T; hence thesis by Def15; end; theorem Th3: p '&' q => p in CnIPC(X) proof T is IPC_theory & X c= T implies p '&' q => p in T; hence thesis by Def15; end; theorem Th4: p '&' q => q in CnIPC(X) proof T is IPC_theory & X c= T implies p '&' q => q in T; hence thesis by Def15; end; theorem Th5: p => (q => (p '&' q)) in CnIPC (X) proof T is IPC_theory & X c= T implies p => (q => (p '&' q)) in T; hence thesis by Def15; end; theorem Th6: p => (p 'or' q) in CnIPC (X) proof T is IPC_theory & X c= T implies p => (p 'or' q) in T; hence thesis by Def15; end; theorem Th7: q => (p 'or' q) in CnIPC (X) proof T is IPC_theory & X c= T implies q => (p 'or' q) in T; hence thesis by Def15; end; theorem Th8: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) proof T is IPC_theory & X c= T implies (p => r) => ((q => r) => ((p 'or' q) => r)) in T; hence thesis by Def15; end; theorem Th9: FALSUM => p in CnIPC (X) proof T is IPC_theory & X c= T implies FALSUM => p in T; hence thesis by Def15; end; theorem Th10: p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X) proof assume that A1: p in CnIPC(X) and A2: p => q in CnIPC(X); T is IPC_theory & X c= T implies q in T proof assume that A3: T is IPC_theory and A4: X c= T; A5: p => q in T by A2,A3,A4,Def15; p in T by A1,A3,A4,Def15; hence thesis by A3,A5; end; hence thesis by Def15; end; theorem Th11: T is IPC_theory & X c= T implies CnIPC(X) c= T by Def15; theorem Th12: X c= CnIPC(X) proof let a be object; assume A1: a in X; then reconsider t = a as Element of MC-wff; for T st T is IPC_theory & X c= T holds t in T by A1; hence thesis by Def15; end; theorem Th13: X c= Y implies CnIPC(X) c= CnIPC(Y) proof assume A1: X c= Y; thus CnIPC(X) c= CnIPC(Y) proof let a be object; assume A2: a in CnIPC(X); then reconsider t = a as Element of MC-wff; for T st T is IPC_theory & Y c= T holds t in T proof let T such that A3: T is IPC_theory and A4: Y c= T; X c= T by A1,A4; hence thesis by A2,A3,Def15; end; hence thesis by Def15; end; end; Lm2: CnIPC(CnIPC(X)) c= CnIPC(X) proof let a be object; assume A1: a in CnIPC(CnIPC(X)); then reconsider t = a as Element of MC-wff; for T st T is IPC_theory & X c= T holds t in T proof let T; assume that A2: T is IPC_theory and A3: X c= T; CnIPC(X) c= T by A2,A3,Th11; hence thesis by A1,A2,Def15; end; hence thesis by Def15; end; theorem CnIPC(CnIPC(X)) = CnIPC(X) proof A1: CnIPC(X) c= CnIPC(CnIPC(X)) by Th12; CnIPC(CnIPC(X)) c= CnIPC(X) by Lm2; hence thesis by A1,XBOOLE_0:def 10; end; Lm3: CnIPC(X) is IPC_theory by Th1,Th2,Th3,Th4,Th5,Th6,Th7,Th8,Th9,Th10; registration let X be Subset of MC-wff; cluster CnIPC(X) -> IPC_theory; coherence by Lm3; end; theorem Th15: T is IPC_theory iff CnIPC(T) = T proof hereby assume A1: T is IPC_theory; A2: CnIPC(T) c= T by A1,Def15; T c= CnIPC(T) by Th12; hence CnIPC(T) = T by A2,XBOOLE_0:def 10; end; thus thesis; end; theorem T is IPC_theory implies IPC-Taut c= T proof assume A1: T is IPC_theory; IPC-Taut c= CnIPC(T) by Th13,XBOOLE_1:2; hence thesis by A1,Th15; end; registration cluster IPC-Taut -> IPC_theory; coherence; end; begin :: Formulas provable in IPC : implication theorem Th17: p => p in IPC-Taut proof A1: p => (p => p) in IPC-Taut by Def14; A2: p => ((p => p) => p) in IPC-Taut by Def14; (p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) in IPC-Taut by Def14; then (p => (p => p)) => (p => p) in IPC-Taut by A2,Def14; hence thesis by A1,Def14; end; theorem Th18: q in IPC-Taut implies p => q in IPC-Taut proof q => (p => q) in IPC-Taut by Def14; hence thesis by Def14; end; theorem IVERUM in IPC-Taut by Def14; theorem (p => q) => (p => p) in IPC-Taut by Th17,Th18; theorem (q => p) => (p => p) in IPC-Taut by Th17,Th18; theorem Th22: (q => r) => ((p => q) => (p => r)) in IPC-Taut proof A1: ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14; A2: ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) => (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r)))) in IPC-Taut by Def14; ((p => (q => r)) => ((p => q) => (p => r))) => ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut by Def14; then ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut by A1,Def14; then A3: ((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r))) in IPC-Taut by A2,Def14; (q => r) => (p => (q => r)) in IPC-Taut by Def14; hence thesis by A3,Def14; end; theorem Th23: p => (q => r) in IPC-Taut implies q => (p => r) in IPC-Taut proof assume A1: p => (q => r) in IPC-Taut; A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in IPC-Taut by Th22; (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14; then ((p => q) => (p => r)) in IPC-Taut by A1,Def14; then A3: ((q => (p => q)) => (q => (p => r))) in IPC-Taut by A2,Def14; q => (p => q) in IPC-Taut by Def14; hence thesis by A3,Def14; end; theorem Th24: :: Hypothetical syllogism (p => q) => ((q => r) => (p => r)) in IPC-Taut proof (q => r) => ((p => q) => (p => r)) in IPC-Taut by Th22; hence thesis by Th23; end; theorem Th25: p => q in IPC-Taut implies (q => r) => (p => r) in IPC-Taut proof assume A1: p => q in IPC-Taut; (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24; hence thesis by A1,Def14; end; theorem Th26: p => q in IPC-Taut & q => r in IPC-Taut implies p => r in IPC-Taut proof assume that A1: p => q in IPC-Taut and A2: q => r in IPC-Taut; (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24; then (q => r) => (p => r) in IPC-Taut by A1,Def14; hence thesis by A2,Def14; end; Lm4: (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut proof (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24; hence thesis by Th25; end; theorem Th27: (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut proof A1: (((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in IPC-Taut by Lm4; ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in IPC-Taut by Lm4; hence thesis by A1,Def14; end; theorem ((p => q) => r) => (q => r) in IPC-Taut proof A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in IPC-Taut by Th24; q => (p => q) in IPC-Taut by Def14; hence thesis by A1,Def14; end; theorem Th29: :: Contraposition (p => (q => r)) => (q => (p => r)) in IPC-Taut proof A1: q => (p => q) in IPC-Taut by Def14; (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14; then A2: (p => q) => ((p => (q => r)) => (p => r)) in IPC-Taut by Th23; ((p => q) => ((p => (q => r)) => (p => r))) => ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in IPC-Taut by Th22; then (q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A2,Def14; then (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A1,Def14; hence thesis by Th23; end; theorem Th30: :: A Hilbert axiom (p => (p => q)) => (p => q) in IPC-Taut proof (p => (p => q)) => ((p => p) => (p => q)) in IPC-Taut by Def14; then A1: (p => p) => ((p => (p => q)) => (p => q)) in IPC-Taut by Th23; p => p in IPC-Taut by Th17; hence thesis by A1,Def14; end; theorem :: Modus ponendo ponens q => ((q => p) => p) in IPC-Taut proof A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in IPC-Taut by Th29; (q => p) => (q => p) in IPC-Taut by Th17; hence thesis by A1,Def14; end; theorem Th32: s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut proof assume that A1: s => (q => p) in IPC-Taut and A2: q in IPC-Taut; (s => (q => p)) => (q => (s => p)) in IPC-Taut by Th29; then q => (s => p) in IPC-Taut by A1,Def14; hence thesis by A2,Def14; end; begin :: Formulas provable in IPC : conjunction theorem Th33: p => (p '&' p) in IPC-Taut proof A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in IPC-Taut by Th30; p => (p => (p '&' p)) in IPC-Taut by Def14; hence thesis by A1,Def14; end; theorem Th34: (p '&' q) in IPC-Taut iff p in IPC-Taut & q in IPC-Taut proof hereby A1: (p '&' q) => q in IPC-Taut by Def14; assume A2: p '&' q in IPC-Taut; (p '&' q) => p in IPC-Taut by Def14; hence p in IPC-Taut & q in IPC-Taut by A2,A1,Def14; end; assume that A3: p in IPC-Taut and A4: q in IPC-Taut; p => (q => (p '&' q)) in IPC-Taut by Def14; then q => (p '&' q) in IPC-Taut by A3,Def14; hence thesis by A4,Def14; end; theorem (p '&' q) in IPC-Taut iff (q '&' p) in IPC-Taut proof hereby assume A1: p '&' q in IPC-Taut; then A2: q in IPC-Taut by Th34; p in IPC-Taut by A1,Th34; hence q '&' p in IPC-Taut by A2,Th34; end; assume A3: q '&' p in IPC-Taut; then A4: p in IPC-Taut by Th34; q in IPC-Taut by A3,Th34; hence thesis by A4,Th34; end; theorem Th36: (( p '&' q ) => r ) => ( p => ( q => r )) in IPC-Taut proof set qp = ( q => ( p '&' q )); set pr = (( p '&' q ) => r) => ( q => r ); A1: ( p => ( qp => pr )) => ( ( p => qp ) => ( p => pr )) in IPC-Taut by Def14; A2: p => ( q => ( p '&' q )) in IPC-Taut by Def14; p => (( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r ))) in IPC-Taut by Th18,Th24; then ( ( p => qp ) => ( p => pr )) in IPC-Taut by A1,Def14; then A3: p => ((( p '&' q ) => r ) => ( q => r )) in IPC-Taut by A2,Def14; (p => ((( p '&' q ) => r ) => ( q => r ))) => ((( p '&' q ) => r ) => ( p => ( q => r ))) in IPC-Taut by Th29; hence thesis by A3,Def14; end; theorem Th37: ( p => ( q => r )) => (( p '&' q ) => r ) in IPC-Taut proof A1: (( p '&' q ) => q) => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut by Th24; ( p '&' q ) => q in IPC-Taut by Def14; then ( q => r ) => (( p '&' q ) => r ) in IPC-Taut by A1,Def14; then A2: p => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut by Th18; A3: ( p => (( p '&' q ) => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by Th29; p => (( q => r ) => (( p '&' q ) => r )) => ((p => ( q => r )) => ( p => (( p '&' q ) => r ))) in IPC-Taut by Def14; then (p => ( q => r )) => ( p => (( p '&' q ) => r )) in IPC-Taut by A2,Def14 ; then A4: (p => ( q => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by A3,Th26; A5: ( p '&' q ) => p in IPC-Taut by Def14; ((p '&' q ) => ( p => r )) => ((( p '&' q ) => p ) => (( p '&' q ) => r )) in IPC-Taut by Def14; then ((p '&' q ) => ( p => r )) => (( p '&' q ) => r ) in IPC-Taut by A5,Th32 ; hence thesis by A4,Th26; end; theorem Th38: ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in IPC-Taut proof A1: ( r => ( q => ( p '&' q ))) => (( r => q ) => ( r => ( p '&' q ))) in IPC-Taut by Def14; p => ( q => ( p '&' q )) in IPC-Taut by Def14; then A2: r => ( p => ( q => ( p '&' q ))) in IPC-Taut by Th18; (r => ( p => ( q => ( p '&' q )))) => (( r => p ) => ( r => ( q => ( p '&' q )))) in IPC-Taut by Def14; then ( r => p ) => ( r => ( q => ( p '&' q ))) in IPC-Taut by A2,Def14; hence thesis by A1,Th26; end; theorem Th39: ( (p => q) '&' p ) => q in IPC-Taut proof set P = p => q; A1: P => P in IPC-Taut by Th17; ( P => P ) => (( P '&' p ) => q ) in IPC-Taut by Th37; hence thesis by A1,Def14; end; theorem (( (p => q) '&' p ) '&' s ) => q in IPC-Taut proof set P = (p => q) '&' p; A1: P => q in IPC-Taut by Th39; (P '&' s) => P in IPC-Taut by Def14; hence thesis by A1,Th26; end; theorem (q => s) => (( p '&' q ) => s) in IPC-Taut proof set P = p '&' q; A1: P => q in IPC-Taut by Def14; (P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24; hence thesis by A1,Def14; end; theorem Th42: (q => s) => (( q '&' p ) => s) in IPC-Taut proof set P = q '&' p; A1: P => q in IPC-Taut by Def14; (P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24; hence thesis by A1,Def14; end; theorem Th43: ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut proof set P = p '&' s; A1: ( P => q ) => (( P => s ) => ( P => ( q '&' s ))) in IPC-Taut by Th38; P => s in IPC-Taut by Def14; hence thesis by A1,Th32; end; theorem Th44: ( p => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut proof A1: ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th43; (p => q) => (( p '&' s ) => q) in IPC-Taut by Th42; hence thesis by A1,Th26; end; theorem Th45: (( p => q ) '&' ( p '&' s )) => ( q '&' s ) in IPC-Taut proof set P = p => q, Q = p '&' s, S = q '&' s; A1: P => (Q => S) in IPC-Taut by Th44; ( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37; hence thesis by A1,Def14; end; theorem Th46: ( p '&' q ) => ( q '&' p ) in IPC-Taut proof set P = p '&' q; A1: P => q in IPC-Taut by Def14; A2: P => p in IPC-Taut by Def14; ( P => q ) => (( P => p ) => ( P => ( q '&' p ))) in IPC-Taut by Th38; then ( P => p ) => ( P => ( q '&' p )) in IPC-Taut by A1,Def14; hence thesis by A2,Def14; end; theorem Th47: ( p => q ) '&' ( p '&' s ) => ( s '&' q ) in IPC-Taut proof A1: ( q '&' s ) => ( s '&' q ) in IPC-Taut by Th46; ( p => q ) '&' ( p '&' s ) => ( q '&' s ) in IPC-Taut by Th45; hence thesis by A1,Th26; end; theorem Th48: ( p => q ) => (( p '&' s ) => ( s '&' q )) in IPC-Taut proof set P = p => q, Q = p '&' s, S = s '&' q; A1: P '&' Q => S in IPC-Taut by Th47; (( P '&' Q ) => S ) => ( P => ( Q => S )) in IPC-Taut by Th36; hence thesis by A1,Def14; end; theorem Th49: ( p => q ) => (( s '&' p ) => ( s '&' q )) in IPC-Taut proof set P = p => q, Q = p '&' s, S = s '&' q, T = s '&' p; A1: P => (Q => S) in IPC-Taut by Th48; A2: T => Q in IPC-Taut by Th46; (P => (Q => S)) => ((T => Q) => (P => (T => S))) in IPC-Taut by Th27; then (T => Q) => (P => (T => S)) in IPC-Taut by A1,Def14; hence thesis by A2,Def14; end; theorem ( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in IPC-Taut proof set P = s '&' q, Q = q '&' s; A1: P => Q in IPC-Taut by Th46; ( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49; hence thesis by A1,Def14; end; theorem ( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in IPC-Taut proof set P = p => q, Q = p => s, S = p => (q '&' s); A1: P => (Q => S) in IPC-Taut by Th38; ( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37; hence thesis by A1,Def14; end; Lm5: ( (p '&' q) '&' s ) => q in IPC-Taut proof A1: (p '&' q) => q in IPC-Taut by Def14; ((p '&' q) '&' s) => (p '&' q) in IPC-Taut by Def14; hence thesis by A1,Th26; end; Lm6: ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q in IPC-Taut proof set P = (p '&' q) '&' s; A1: P => q in IPC-Taut by Lm5; ( P => q ) => (( P '&' P ) => ( P '&' q )) in IPC-Taut by Th49; hence thesis by A1,Def14; end; Lm7: (p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut proof A1: ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q in IPC-Taut by Lm6; ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) in IPC-Taut by Th33; hence thesis by A1,Th26; end; Lm8: (p '&' q) '&' s => (p '&' s) in IPC-Taut proof set P = p '&' q; A1: P => p in IPC-Taut by Def14; ( P => p ) => ((P '&' s) => (p '&' s)) in IPC-Taut by Th44; hence thesis by A1,Def14; end; Lm9: (p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut proof set P = p '&' q '&' s, Q = p '&' s; A1: P => Q in IPC-Taut by Lm8; ( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44; hence thesis by A1,Def14; end; Lm10: (p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut proof A1: (p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut by Lm9; (p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut by Lm7; hence thesis by A1,Th26; end; Lm11: (p '&' s) '&' q => (s '&' p) '&' q in IPC-Taut proof set P = p '&' s, Q = s '&' p; A1: P => Q in IPC-Taut by Th46; ( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44; hence thesis by A1,Def14; end; Lm12: (p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut proof A1: (p '&' s) '&' q => (s '&' p) '&' q in IPC-Taut by Lm11; (p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut by Lm10; hence thesis by A1,Th26; end; Lm13: (p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut proof A1: (s '&' p) '&' q => (s '&' q) '&' p in IPC-Taut by Lm10; (p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut by Lm12; hence thesis by A1,Th26; end; Lm14: (p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut proof A1: (s '&' q) '&' p => p '&' (s '&' q) in IPC-Taut by Th46; (p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut by Lm13; hence thesis by A1,Th26; end; Lm15: p '&' (s '&' q) => p '&' (q '&' s) in IPC-Taut proof set P = s '&' q, Q = q '&' s; A1: s '&' q => q '&' s in IPC-Taut by Th46; ( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49; hence thesis by A1,Def14; end; theorem (p '&' q) '&' s => p '&' (q '&' s) in IPC-Taut proof A1: p '&' (s '&' q) => p '&' (q '&' s) in IPC-Taut by Lm15; (p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut by Lm14; hence thesis by A1,Th26; end; Lm16: p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut proof A1: p '&' (s '&' q) => (s '&' q) '&' p in IPC-Taut by Th46; p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm15; hence thesis by A1,Th26; end; Lm17: (s '&' q) '&' p => (q '&' s) '&' p in IPC-Taut proof set P = s '&' q, Q = q '&' s; A1: s '&' q => q '&' s in IPC-Taut by Th46; ( P => Q ) => ((P '&' p) => (Q '&' p)) in IPC-Taut by Th44; hence thesis by A1,Def14; end; Lm18: p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut proof A1: (s '&' q) '&' p => (q '&' s) '&' p in IPC-Taut by Lm17; p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut by Lm16; hence thesis by A1,Th26; end; Lm19: p '&' (q '&' s) => (p '&' s) '&' q in IPC-Taut proof A1: (q '&' s) '&' p => (p '&' s) '&' q in IPC-Taut by Lm13; p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut by Lm18; hence thesis by A1,Th26; end; Lm20: p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut proof set P = q '&' s, Q = s '&' q; A1: q '&' s => s '&' q in IPC-Taut by Th46; ( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49; hence thesis by A1,Def14; end; theorem p '&' (q '&' s) => (p '&' q) '&' s in IPC-Taut proof A1: p '&' (s '&' q) => (p '&' q) '&' s in IPC-Taut by Lm19; p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm20; hence thesis by A1,Th26; end; begin :: Formulas provable in IPC: disjunction theorem Th54: (p 'or' p) => p in IPC-Taut proof A1: p => p in IPC-Taut by Th17; (p => p) => ((p => p) => ((p 'or' p) => p)) in IPC-Taut by Def14; then (p => p) => ((p 'or' p) => p) in IPC-Taut by A1,Def14; hence thesis by A1,Def14; end; theorem p in IPC-Taut or q in IPC-Taut implies (p 'or' q) in IPC-Taut proof assume A1: p in IPC-Taut or q in IPC-Taut; now per cases by A1; case A2: p in IPC-Taut; p => (p 'or' q) in IPC-Taut by Def14; hence thesis by A2,Def14; end; case A3: q in IPC-Taut; q => (p 'or' q) in IPC-Taut by Def14; hence thesis by A3,Def14; end; end; hence thesis; end; theorem Th56: (p 'or' q) => (q 'or' p) in IPC-Taut proof A1: p => (q 'or' p) in IPC-Taut by Def14; A2: q => (q 'or' p) in IPC-Taut by Def14; (p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p))) in IPC-Taut by Def14; then ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p))) in IPC-Taut by A1 ,Def14; hence thesis by A2,Def14; end; theorem (p 'or' q) in IPC-Taut iff (q 'or' p) in IPC-Taut proof hereby assume A1: p 'or' q in IPC-Taut; (p 'or' q) => (q 'or' p) in IPC-Taut by Th56; hence q 'or' p in IPC-Taut by A1,Def14; end; assume A2: q 'or' p in IPC-Taut; (q 'or' p) => (p 'or' q) in IPC-Taut by Th56; hence thesis by A2,Def14; end; theorem Th58: (p => q) => (p => (q 'or' s)) in IPC-Taut proof A1: (q => (q 'or' s)) => ((p => q) => (p => (q 'or' s))) in IPC-Taut by Th22; q => (q 'or' s) in IPC-Taut by Def14; hence thesis by A1,Def14; end; theorem Th59: (p => q) => (p => (s 'or' q)) in IPC-Taut proof A1: (q => (s 'or' q)) => ((p => q) => (p => (s 'or' q))) in IPC-Taut by Th22; q => (s 'or' q) in IPC-Taut by Def14; hence thesis by A1,Def14; end; theorem Th60: ( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut proof set P = p 'or' s, Q = q 'or' s; A1: (p => q) => (p => Q) in IPC-Taut by Th58; (p => Q) => ((s => Q) => (P => Q)) in IPC-Taut by Def14; then A2: (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Th23; s => Q in IPC-Taut by Def14; then (p => Q) => (P => Q) in IPC-Taut by A2,Def14; hence thesis by A1,Th26; end; theorem Th61: p => q in IPC-Taut implies (p 'or' s) => (q 'or' s) in IPC-Taut proof assume A1: p => q in IPC-Taut; ( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by Th60; hence thesis by A1,Def14; end; theorem Th62: ( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut proof set P = s 'or' p, Q = s 'or' q; A1: s => Q in IPC-Taut by Def14; A2: (p => q) => (p => Q) in IPC-Taut by Th59; (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Def14; then (p => Q) => (P => Q) in IPC-Taut by A1,Def14; hence thesis by A2,Th26; end; theorem Th63: p => q in IPC-Taut implies ( s 'or' p ) => ( s 'or' q ) in IPC-Taut proof assume A1: p => q in IPC-Taut; ( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut by Th62; hence thesis by A1,Def14; end; theorem Th64: ( p 'or' (q 'or' s) ) => ( q 'or' (p 'or' s) ) in IPC-Taut proof set P = p 'or' s, Q = q 'or' s; A1: P => (q 'or' P) in IPC-Taut by Def14; p => P in IPC-Taut by Def14; then p => (q 'or' P) in IPC-Taut by A1,Th26; then A2: ((q 'or' P) 'or' p) => ((q 'or' P) 'or' (q 'or' P)) in IPC-Taut by Th63; ((q 'or' P) 'or' (q 'or' P)) => (q 'or' P) in IPC-Taut by Th54; then A3: ((q 'or' P) 'or' p) => (q 'or' P) in IPC-Taut by A2,Th26; s => P in IPC-Taut by Def14; then (q 'or' s) => (q 'or' P) in IPC-Taut by Th63; then A4: (p 'or' Q) => (p 'or' (q 'or' P)) in IPC-Taut by Th63; (p 'or' (q 'or' P)) => ((q 'or' P) 'or' p) in IPC-Taut by Th56; then (p 'or' Q) => ((q 'or' P) 'or' p) in IPC-Taut by A4,Th26; hence thesis by A3,Th26; end; theorem ( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut proof A1: (s 'or' (p 'or' q)) => ((p 'or' q) 'or' s) in IPC-Taut by Th56; (q 'or' s) => (s 'or' q) in IPC-Taut by Th56; then A2: (p 'or' (q 'or' s)) => (p 'or' (s 'or' q)) in IPC-Taut by Th63; (p 'or' (s 'or' q)) => (s 'or' (p 'or' q)) in IPC-Taut by Th64; then (p 'or' (q 'or' s)) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26; hence thesis by A1,Th26; end; theorem ( (p 'or' q) 'or' s ) => ( p 'or' (q 'or' s) ) in IPC-Taut proof (p 'or' q) => (q 'or' p) in IPC-Taut by Th56; then A1: ((p 'or' q) 'or' s) => ((q 'or' p) 'or' s) in IPC-Taut by Th61; (q 'or' p) => (p 'or' q) in IPC-Taut by Th56; then A2: (s 'or' (q 'or' p)) => (s 'or' (p 'or' q)) in IPC-Taut by Th63; ((q 'or' p) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by Th56; then ((p 'or' q) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by A1,Th26; then A3: ((p 'or' q) 'or' s) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26; (s 'or' q) => (q 'or' s) in IPC-Taut by Th56; then A4: (p 'or' (s 'or' q)) => (p 'or' (q 'or' s)) in IPC-Taut by Th63; (s 'or' (p 'or' q)) => (p 'or' (s 'or' q)) in IPC-Taut by Th64; then ((p 'or' q) 'or' s) => (p 'or' (s 'or' q)) in IPC-Taut by A3,Th26; hence thesis by A4,Th26; end; begin :: Classical propositional calculus CPC reserve T, X, Y for Subset of MC-wff; reserve p, q, r for Element of MC-wff; definition let T be Subset of MC-wff; attr T is CPC_theory means for p, q, r being Element of MC-wff holds p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (p in T & p => q in T implies q in T); correctness; end; theorem T is CPC_theory implies T is IPC_theory; definition let X; func CnCPC X -> Subset of MC-wff means :Def20: r in it iff for T st T is CPC_theory & X c= T holds r in T; existence proof defpred P[object] means for T st T is CPC_theory & X c= T holds \$1 in T; consider Y being set such that A1: for a being object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0: sch 1; Y c= MC-wff by A1; then reconsider Z = Y as Subset of MC-wff; take Z; thus thesis by A1; end; uniqueness proof let Y,Z be Subset of MC-wff such that A2: r in Y iff for T st T is CPC_theory & X c= T holds r in T and A3: r in Z iff for T st T is CPC_theory & X c= T holds r in T; for a being object holds a in Y iff a in Z proof let a be object; hereby assume A4: a in Y; then reconsider t=a as Element of MC-wff; for T st T is CPC_theory & X c= T holds t in T by A2,A4; hence a in Z by A3; end; assume A5: a in Z; then reconsider t=a as Element of MC-wff; for T st T is CPC_theory & X c= T holds t in T by A3,A5; hence thesis by A2; end; hence thesis by TARSKI:2; end; end; definition func CPC-Taut -> Subset of MC-wff equals CnCPC({}(MC-wff)); correctness; end; theorem Th68: CnIPC (X) c= CnCPC (X) proof let a be object; assume A1: a in CnIPC (X); then reconsider r = a as Element of MC-wff; for T st T is CPC_theory & X c= T holds r in T proof let T such that A2: T is CPC_theory and A3: X c= T; T is IPC_theory by A2; hence thesis by A1,A3,Def15; end; hence thesis by Def20; end; theorem Th69: p => (q => p) in CnCPC (X) & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X) & p '&' q => p in CnCPC (X) & p '&' q => q in CnCPC (X) & p => (q => (p '&' q)) in CnCPC (X) & p => (p 'or' q) in CnCPC (X) & q => (p 'or' q) in CnCPC (X) & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X) & FALSUM => p in CnCPC (X) & p 'or' (p => FALSUM) in CnCPC (X) proof A1: CnIPC(X) c= CnCPC(X) by Th68; p => (q => p) in CnIPC (X) by Th1; hence p => (q => p) in CnCPC (X) by A1; A2: CnIPC(X) c= CnCPC(X) by Th68; (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2; hence (p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X) by A2; A3: CnIPC(X) c= CnCPC(X) by Th68; p '&' q => p in CnIPC (X) by Th3; hence p '&' q => p in CnCPC (X) by A3; A4: CnIPC(X) c= CnCPC(X) by Th68; p '&' q => q in CnIPC (X) by Th4; hence p '&' q => q in CnCPC (X) by A4; A5: CnIPC(X) c= CnCPC(X) by Th68; p => (q => (p '&' q)) in CnIPC (X) by Th5; hence p => (q => (p '&' q)) in CnCPC (X) by A5; A6: CnIPC(X) c= CnCPC(X) by Th68; p => (p 'or' q) in CnIPC (X) by Th6; hence p => (p 'or' q) in CnCPC (X) by A6; A7: CnIPC(X) c= CnCPC(X) by Th68; q => (p 'or' q) in CnIPC (X) by Th7; hence q => (p 'or' q) in CnCPC (X) by A7; A8: CnIPC(X) c= CnCPC(X) by Th68; (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8; hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X) by A8; A9: CnIPC(X) c= CnCPC(X) by Th68; FALSUM => p in CnIPC (X) by Th9; hence FALSUM => p in CnCPC (X) by A9; T is CPC_theory & X c= T implies p 'or' (p => FALSUM) in T; hence p 'or' (p => FALSUM) in CnCPC (X) by Def20; end; theorem Th70: p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X) proof assume that A1: p in CnCPC(X) and A2: p => q in CnCPC(X); T is CPC_theory & X c= T implies q in T proof assume that A3: T is CPC_theory and A4: X c= T; A5: p => q in T by A2,A3,A4,Def20; p in T by A1,A3,A4,Def20; hence thesis by A3,A5; end; hence thesis by Def20; end; theorem Th71: T is CPC_theory & X c= T implies CnCPC(X) c= T by Def20; theorem Th72: X c= CnCPC(X) proof let a be object; assume A1: a in X; then reconsider t = a as Element of MC-wff; for T st T is CPC_theory & X c= T holds t in T by A1; hence thesis by Def20; end; theorem Th73: X c= Y implies CnCPC(X) c= CnCPC(Y) proof assume A1: X c= Y; thus CnCPC(X) c= CnCPC(Y) proof let a be object; assume A2: a in CnCPC(X); then reconsider t = a as Element of MC-wff; for T st T is CPC_theory & Y c= T holds t in T proof let T such that A3: T is CPC_theory and A4: Y c= T; X c= T by A1,A4; hence thesis by A2,A3,Def20; end; hence thesis by Def20; end; end; Lm21: CnCPC(CnCPC(X)) c= CnCPC(X) proof let a be object; assume A1: a in CnCPC(CnCPC(X)); then reconsider t = a as Element of MC-wff; for T st T is CPC_theory & X c= T holds t in T proof let T; assume that A2: T is CPC_theory and A3: X c= T; CnCPC(X) c= T by A2,A3,Th71; hence thesis by A1,A2,Def20; end; hence thesis by Def20; end; theorem CnCPC(CnCPC(X)) = CnCPC(X) proof A1: CnCPC(X) c= CnCPC(CnCPC(X)) by Th72; CnCPC(CnCPC(X)) c= CnCPC(X) by Lm21; hence thesis by A1,XBOOLE_0:def 10; end; Lm22: CnCPC(X) is CPC_theory by Th69,Th70; registration let X be Subset of MC-wff; cluster CnCPC(X) -> CPC_theory; coherence by Lm22; end; theorem Th75: T is CPC_theory iff CnCPC(T) = T proof hereby assume A1: T is CPC_theory; A2: CnCPC(T) c= T by A1,Def20; T c= CnCPC(T) by Th72; hence CnCPC(T) = T by A2,XBOOLE_0:def 10; end; thus thesis; end; theorem T is CPC_theory implies CPC-Taut c= T proof assume A1: T is CPC_theory; CPC-Taut c= CnCPC(T) by Th73,XBOOLE_1:2; hence thesis by A1,Th75; end; registration cluster CPC-Taut -> CPC_theory; coherence; end; theorem IPC-Taut c= CPC-Taut by Th68; begin :: Modal calculus S4 reserve T, X, Y for Subset of MC-wff; reserve p, q, r for Element of MC-wff; definition let T be Subset of MC-wff; attr T is S4_theory means for p, q, r being Element of MC-wff holds p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (Nes (p => q)) => ((Nes p) => (Nes q)) in T & (Nes p) => p in T & (Nes p) => Nes (Nes p) in T & (p in T & p => q in T implies q in T) & (p in T implies Nes p in T); correctness; end; theorem T is S4_theory implies T is CPC_theory; theorem T is S4_theory implies T is IPC_theory; definition let X; func CnS4 X -> Subset of MC-wff means :Def23: r in it iff for T st T is S4_theory & X c= T holds r in T; existence proof defpred P[object] means for T st T is S4_theory & X c= T holds \$1 in T; consider Y being set such that A1: for a being object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0: sch 1; Y c= MC-wff by A1; then reconsider Z = Y as Subset of MC-wff; take Z; thus thesis by A1; end; uniqueness proof let Y,Z be Subset of MC-wff such that A2: r in Y iff for T st T is S4_theory & X c= T holds r in T and A3: r in Z iff for T st T is S4_theory & X c= T holds r in T; for a being object holds a in Y iff a in Z proof let a be object; hereby assume A4: a in Y; then reconsider t=a as Element of MC-wff; for T st T is S4_theory & X c= T holds t in T by A2,A4; hence a in Z by A3; end; assume A5: a in Z; then reconsider t=a as Element of MC-wff; for T st T is S4_theory & X c= T holds t in T by A3,A5; hence thesis by A2; end; hence thesis by TARSKI:2; end; end; definition func S4-Taut -> Subset of MC-wff equals CnS4({}(MC-wff)); correctness; end; theorem Th80: CnCPC (X) c= CnS4 (X) proof let a be object; assume A1: a in CnCPC (X); then reconsider r = a as Element of MC-wff; for T st T is S4_theory & X c= T holds r in T proof let T such that A2: T is S4_theory and A3: X c= T; T is CPC_theory by A2; hence thesis by A1,A3,Def20; end; hence thesis by Def23; end; theorem Th81: CnIPC (X) c= CnS4 (X) proof A1: CnCPC (X) c= CnS4 (X) by Th80; CnIPC (X) c= CnCPC (X) by Th68; hence thesis by A1; end; theorem Th82: p => (q => p) in CnS4 (X) & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X) & p '&' q => p in CnS4 (X) & p '&' q => q in CnS4 (X) & p => (q => (p '&' q)) in CnS4 (X) & p => (p 'or' q) in CnS4 (X) & q => (p 'or' q) in CnS4 (X) & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X) & FALSUM => p in CnS4 (X) & p 'or' (p => FALSUM) in CnS4 (X) proof A1: CnIPC (X) c= CnS4 (X) by Th81; p => (q => p) in CnIPC (X) by Th1; hence p => (q => p) in CnS4 (X) by A1; A2: CnIPC (X) c= CnS4 (X) by Th81; (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2; hence (p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X) by A2; A3: CnIPC (X) c= CnS4 (X) by Th81; p '&' q => p in CnIPC (X) by Th3; hence p '&' q => p in CnS4 (X) by A3; A4: CnIPC (X) c= CnS4 (X) by Th81; p '&' q => q in CnIPC (X) by Th4; hence p '&' q => q in CnS4 (X) by A4; A5: CnIPC (X) c= CnS4 (X) by Th81; p => (q => (p '&' q)) in CnIPC (X) by Th5; hence p => (q => (p '&' q)) in CnS4 (X) by A5; A6: CnIPC (X) c= CnS4 (X) by Th81; p => (p 'or' q) in CnIPC (X) by Th6; hence p => (p 'or' q) in CnS4 (X) by A6; A7: CnIPC (X) c= CnS4 (X) by Th81; q => (p 'or' q) in CnIPC (X) by Th7; hence q => (p 'or' q) in CnS4 (X) by A7; A8: CnIPC (X) c= CnS4 (X) by Th81; (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8; hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X) by A8; A9: CnIPC (X) c= CnS4 (X) by Th81; FALSUM => p in CnIPC (X) by Th9; hence FALSUM => p in CnS4 (X) by A9; T is S4_theory & X c= T implies p 'or' (p => FALSUM) in T; hence p 'or' (p => FALSUM) in CnS4 (X) by Def23; end; theorem Th83: p in CnS4 (X) & p => q in CnS4 (X) implies q in CnS4 (X) proof assume that A1: p in CnS4 (X) and A2: p => q in CnS4 (X); T is S4_theory & X c= T implies q in T proof assume that A3: T is S4_theory and A4: X c= T; A5: p => q in T by A2,A3,A4,Def23; p in T by A1,A3,A4,Def23; hence thesis by A3,A5; end; hence thesis by Def23; end; theorem Th84: (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 (X) proof T is S4_theory & X c= T implies (Nes (p => q)) => ((Nes p) => (Nes q)) in T; hence thesis by Def23; end; theorem Th85: (Nes p) => p in CnS4 (X) proof T is S4_theory & X c= T implies (Nes p) => p in T; hence thesis by Def23; end; theorem Th86: (Nes p) => Nes (Nes p) in CnS4 (X) proof T is S4_theory & X c= T implies (Nes p) => Nes (Nes p) in T; hence thesis by Def23; end; theorem Th87: p in CnS4 (X) implies Nes p in CnS4 (X) proof assume A1: p in CnS4 (X); T is S4_theory & X c= T implies Nes p in T proof assume that A2: T is S4_theory and A3: X c= T; p in T by A1,A2,A3,Def23; hence thesis by A2; end; hence thesis by Def23; end; theorem Th88: T is S4_theory & X c= T implies CnS4(X) c= T by Def23; theorem Th89: X c= CnS4(X) proof let a be object; assume A1: a in X; then reconsider t = a as Element of MC-wff; for T st T is S4_theory & X c= T holds t in T by A1; hence thesis by Def23; end; theorem Th90: X c= Y implies CnS4(X) c= CnS4(Y) proof assume A1: X c= Y; thus CnS4(X) c= CnS4(Y) proof let a be object; assume A2: a in CnS4(X); then reconsider t = a as Element of MC-wff; for T st T is S4_theory & Y c= T holds t in T proof let T such that A3: T is S4_theory and A4: Y c= T; X c= T by A1,A4; hence thesis by A2,A3,Def23; end; hence thesis by Def23; end; end; Lm23: CnS4(CnS4(X)) c= CnS4(X) proof let a be object; assume A1: a in CnS4(CnS4(X)); then reconsider t = a as Element of MC-wff; for T st T is S4_theory & X c= T holds t in T proof let T; assume that A2: T is S4_theory and A3: X c= T; CnS4(X) c= T by A2,A3,Th88; hence thesis by A1,A2,Def23; end; hence thesis by Def23; end; theorem CnS4(CnS4(X)) = CnS4(X) proof A1: CnS4(X) c= CnS4(CnS4(X)) by Th89; CnS4(CnS4(X)) c= CnS4(X) by Lm23; hence thesis by A1,XBOOLE_0:def 10; end; Lm24: CnS4(X) is S4_theory by Th82,Th84,Th85,Th86,Th83,Th87; registration let X be Subset of MC-wff; cluster CnS4(X) -> S4_theory; coherence by Lm24; end; theorem Th92: T is S4_theory iff CnS4(T) = T proof hereby assume A1: T is S4_theory; A2: CnS4(T) c= T by A1,Def23; T c= CnS4(T) by Th89; hence CnS4(T) = T by A2,XBOOLE_0:def 10; end; thus thesis; end; theorem T is S4_theory implies S4-Taut c= T proof assume A1: T is S4_theory; S4-Taut c= CnS4(T) by Th90,XBOOLE_1:2; hence thesis by A1,Th92; end; registration cluster S4-Taut -> S4_theory; coherence; end; theorem CPC-Taut c= S4-Taut by Th80; theorem IPC-Taut c= S4-Taut by Th81;