:: Sequent calculus, derivability, provability. Goedel's completeness theorem :: by Marco B. Caminati :: :: Received December 29, 2010 :: Copyright (c) 2010-2021 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 TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1, RELAT_2, FINSEQ_1, FUNCT_1, ARYTM_3, XCMPLX_0, CARD_1, ARYTM_1, FUNCT_2, XXREAL_0, ORDINAL4, FUNCT_7, FINSEQ_2, EQREL_1, COMPLEX1, MCART_1, PARTFUN1, MARGREL1, XBOOLEAN, FINSET_1, FUNCT_3, SETFAM_1, FUNCT_4, FUNCOP_1, CARD_3, COHSP_1, FOMODEL0, FOMODEL1, FOMODEL2, FOMODEL3, FOMODEL4; notations COHSP_1, TARSKI, MARGREL1, XBOOLE_0, ZFMISC_1, SETFAM_1, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, MCART_1, NAT_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_2, XXREAL_0, FUNCT_7, FINSEQ_1, LANG1, FINSEQ_2, EQREL_1, INT_2, FINSET_1, FUNCT_4, FUNCOP_1, CARD_3, ORDERS_4, LEXBFS, XTUPLE_0, XFAMILY, FOMODEL0, FOMODEL1, FOMODEL2, FOMODEL3; constructors NAT_1, CARD_1, ZFMISC_1, NUMBERS, INT_1, FINSEQ_1, XCMPLX_0, MONOID_0, XXREAL_0, FUNCT_7, FINSEQ_2, ENUMSET1, EQREL_1, RELSET_1, MCART_1, MARGREL1, FINSET_1, PARTFUN1, FINSEQOP, MATRIX_1, FUNCT_3, RFUNCT_3, SETFAM_1, LANG1, PRE_POLY, FUNCT_1, FUNCT_4, FUNCOP_1, CARD_3, ORDERS_4, LEXBFS, MATROID0, COHSP_1, XTUPLE_0, FOMODEL0, FOMODEL1, FOMODEL2, FOMODEL3, XFAMILY; registrations ORDINAL1, NAT_1, RELAT_1, FUNCT_1, INT_1, FINSEQ_1, XREAL_0, FUNCT_2, FINSEQ_2, SUBSET_1, RELSET_1, PARTFUN1, EQREL_1, CARD_1, XBOOLE_0, XXREAL_0, ZFMISC_1, MARGREL1, FINSET_1, RAMSEY_1, YELLOW12, FUNCOP_1, CARD_3, FUNCT_7, FOMODEL0, FOMODEL1, FOMODEL2, FOMODEL3, XTUPLE_0; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin ::#General framework for sequent calculus reserve k,m,n for Nat, kk,mm,nn for Element of NAT, U,U1,U2 for non empty set, A,B,X,Y,Z, x,x1,x2,y,z for set, S for Language, s, s1, s2 for Element of S, f,g for Function, w for string of S, tt,tt1,tt2 for Element of AllTermsOf S, psi,psi1,psi2,phi,phi1,phi2 for wff string of S, u,u1,u2 for Element of U, Phi,Phi1,Phi2 for Subset of AllFormulasOf S, t,t1,t2,t3 for termal string of S, r for relational Element of S, a for ofAtomicFormula Element of S, l, l1, l2 for literal Element of S, p for FinSequence, m1, n1 for non zero Nat, S1, S2 for Language; ::##################################################################### ::#Definitions and auxiliary lemmas definition let S be Language; func S-sequents -> set equals :: FOMODEL4:def 1 {[premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S: premises is finite}; end; registration let S be Language; cluster S-sequents -> non empty; end; registration let S; cluster S-sequents -> Relation-like; end; definition ::#def2 6 let S be Language; let x be object; attr x is S-sequent-like means :: FOMODEL4:def 2 x in S-sequents; end; definition ::#def3 6 let S,X; attr X is S-sequents-like means :: FOMODEL4:def 3 X c= S-sequents; end; registration let S; cluster -> S-sequents-like for Subset of S-sequents; cluster -> S-sequent-like for Element of S-sequents; end; registration let S be Language; cluster S-sequent-like for Element of S-sequents; cluster S-sequents-like for Subset of S-sequents; end; registration let S; cluster S-sequent-like for object; cluster S-sequents-like for set; end; definition let S be Language; mode Rule of S is Element of Funcs(bool (S-sequents), bool (S-sequents)); end; definition let S be Language; mode RuleSet of S is Subset of Funcs(bool (S-sequents), bool (S-sequents)); end; reserve D,D1,D2,D3 for RuleSet of S, R for Rule of S, Seqts,Seqts1,Seqts2 for Subset of S-sequents, seqt,seqt1,seqt2 for Element of S-sequents, SQ,SQ1,SQ2 for S-sequents-like set, Sq,Sq1,Sq2 for S-sequent-like object; registration let S, Sq; cluster {Sq} -> S-sequents-like; end; registration let S,SQ1,SQ2; cluster SQ1\/SQ2 -> S-sequents-like; end; registration let S; let x,y be S-sequent-like object; cluster {x,y} -> S-sequents-like; end; registration let S,phi; let Phi1,Phi2 be finite Subset of (AllFormulasOf S); cluster [Phi1 \/ Phi2, phi] -> S-sequent-like; end; registration let S; cluster {} /\ S -> S-sequents-like; end; registration let S; cluster {} null S -> S-sequents-like; end; registration let S,Y; let X be S-sequents-like set; cluster X/\Y -> S-sequents-like; end; registration let S; let premises be finite Subset of (AllFormulasOf S); let phi be wff string of S; cluster [premises,phi] -> S-sequent-like; end; registration let S; let phi1,phi2 be wff string of S; cluster [{phi1},phi2] -> S-sequent-like; let phi3 be wff string of S; cluster [{phi1,phi2},phi3] -> S-sequent-like; end; registration let S, phi1, phi2; let Phi be finite Subset of AllFormulasOf S; cluster [Phi\/{phi1}, phi2] -> S-sequent-like; end; definition let S,X,D; redefine func D null X -> RuleSet of S; end; definition let S,x; attr x is S-premises-like means :: FOMODEL4:def 4 x c= AllFormulasOf S & x is finite; end; registration let S; cluster S-premises-like -> finite for set; end; registration let S,phi; cluster {phi} -> S-premises-like; end; registration let S; let e be empty set; cluster e null S -> S-premises-like; end; registration let X,S; cluster S-premises-like for Subset of X; end; registration let S; cluster S-premises-like for set; end; registration let S; let X be S-premises-like set; cluster -> S-premises-like for Subset of X; end; reserve H,H1,H2,H3 for S-premises-like set; definition let S, H2, H1; redefine func H1 null H2 -> Subset of (AllFormulasOf S); end; registration let S,H,x; cluster H null x -> S-premises-like; end; registration let S, H1, H2; cluster H1\/H2 -> S-premises-like; end; registration let S,H,phi; cluster [H,phi] -> S-sequent-like; end; definition let S,D; func OneStep(D) -> Rule of S means :: FOMODEL4:def 5 for Seqs being Element of bool (S-sequents) holds it.Seqs = union ((union D) .: {Seqs}); end; definition let S,D,m; func (m,D)-derivables -> Rule of S equals :: FOMODEL4:def 6 iter(OneStep D,m); end; definition let S be Language; let D be RuleSet of S; let Seqs1 be object, Seqs2 be set; attr Seqs2 is (Seqs1,D)-derivable means :: FOMODEL4:def 7 Seqs2 c= union (((OneStep D) [*]) .: {Seqs1}); end; definition let m,S,D; let Seqts be set, seqt be object; attr seqt is (m,Seqts,D)-derivable means :: FOMODEL4:def 8 seqt in (m,D)-derivables.Seqts; end; definition let S,D; func D-iterators -> Subset-Family of [:bool (S-sequents), bool (S-sequents):] equals :: FOMODEL4:def 9 the set of all iter(OneStep D,mm); end; definition let S,R; attr R is isotone means :: FOMODEL4:def 10 Seqts1 c= Seqts2 implies R.Seqts1 c= R.Seqts2; end; registration let S; cluster isotone for Rule of S; end; definition let S,D; attr D is isotone means :: FOMODEL4:def 11 for Seqts1,Seqts2,f st Seqts1 c= Seqts2 & f in D ex g st (g in D & f.Seqts1 c= g.Seqts2); end; registration let S; let M be isotone Rule of S; cluster {M} -> isotone for RuleSet of S; end; registration let S; cluster isotone for RuleSet of S; end; reserve M,K,K1,K2 for isotone RuleSet of S; definition let S be Language; let D be RuleSet of S; let Seqts be set; attr Seqts is D-derivable means :: FOMODEL4:def 12 Seqts is ({},D)-derivable; end; registration let S,D; cluster D-derivable -> ({},D)-derivable for set; cluster ({},D)-derivable -> D-derivable for set; end; registration let S,D; let Seqts be empty set; cluster (Seqts,D)-derivable -> D-derivable for set; end; definition let S,D,X; let phi be object; attr phi is (X,D)-provable means :: FOMODEL4:def 13 ::#Def12 6 {[X,phi]} is D-derivable or ex seqt being object st (seqt`1 c= X & seqt`2 = phi & {seqt} is D-derivable); end; definition let S,D,X,x; redefine attr x is (X,D)-provable means :: FOMODEL4:def 14 ex seqt being object st seqt`1 c= X & seqt`2 = x & {seqt} is D-derivable; end; definition ::#def64 6 let S,D,X; attr X is D-inconsistent means :: FOMODEL4:def 15 ex phi1,phi2 st phi1 is (X,D)-provable & <*TheNorSymbOf S*>^phi1^phi2 is (X,D)-provable; end; registration let S,D; let Phi1, Phi2 be set; cluster (Phi1\Phi2,D)-provable -> (Phi1,D)-provable for set; end; registration let S,D; let Phi1, Phi2 be set; cluster (Phi1\Phi2,D)-provable -> (Phi1\/Phi2,D)-provable for set; end; registration let S,D; let Phi1,Phi2 be set; cluster (Phi1/\Phi2,D)-provable -> (Phi1,D)-provable for set; end; registration let S,D; let X be set, x be Subset of X; cluster (x,D)-provable -> (X,D)-provable for set; end; definition let S,D; let Phi be set; func (Phi,D)-termEq -> set equals :: FOMODEL4:def 16 { [t1, t2] where t1,t2 is termal string of S: <* TheEqSymbOf S *> ^ t1 ^ t2 is (Phi,D)-provable}; end; definition let S,D; let Phi be set; attr Phi is D-expanded means :: FOMODEL4:def 17 ::#Deductively closed (cfr. Hedman) x is (Phi,D)-provable implies {x} c= Phi; end; definition let S,D,X; redefine attr X is D-expanded means :: FOMODEL4:def 18 ::#def63 4 x is (X,D)-provable implies x in X; end; definition let S,x; attr x is S-null means :: FOMODEL4:def 19 not contradiction; end; registration let S; cluster S-sequent-like -> S-null for set; end; ::#Type Tuning definition let S,D; let Phi be set; redefine func (Phi,D)-termEq -> Relation of (AllTermsOf S); end; definition let S; let x be empty set; let phi be wff string of S; redefine func [ x, phi ] -> Element of S-sequents; end; registration let S; cluster S-null for set; end; registration let S; cluster S-sequent-like -> S-null for set; end; registration let S; cluster -> S-null for Element of S-sequents; end; registration let m,S,D,X; cluster (m,D)-derivables.X -> S-sequents-like; end; registration let S,D,m,X; cluster (m,X,D)-derivable -> S-sequent-like for object; end; registration let S,D; cluster D-expanded for Subset of AllFormulasOf S; end; registration let S,D; cluster D-expanded for set; end; registration let S,D,X; cluster (X,D)-derivable -> S-sequents-like for set; end; definition ::#def18 6 let S,D,X,x; redefine attr x is (X,D)-provable means :: FOMODEL4:def 20 ex H being set, m st H c= X & [H,x] is (m,{},D)-derivable; end; theorem :: FOMODEL4:1 {y} is (SQ,D)-derivable implies ex mm st y is (mm,SQ,D)-derivable; theorem :: FOMODEL4:2 D1 c= D2 & (D2 is isotone or D1 is isotone) & x is (m,X,D1)-derivable implies x is (m,X,D2)-derivable; begin ::#An example of complete set of inference rules ::############################################################################ ::# Encoding of modified Gentzen rules definition let Seqts be set; let S be Language; let seqt be S-null set; pred seqt Rule0 Seqts means :: FOMODEL4:def 21 seqt`2 in seqt`1; ::# assumption rule; could be weakened to seqt`1={seqt`2}, since the ::# stronger form overlaps with Rule1 pred seqt Rule1 Seqts means :: FOMODEL4:def 22 ex y being set st y in Seqts & y`1 c= seqt`1 & seqt`2 = y`2; pred seqt Rule2 Seqts means :: FOMODEL4:def 23 seqt`1 is empty & ex t being termal string of S st seqt`2 = <* TheEqSymbOf S *> ^ t ^ t; pred seqt Rule3a Seqts means :: FOMODEL4:def 24 ex t1,t2,t3 being termal string of S st (seqt=[{<*TheEqSymbOf S*>^t1^t2,<*TheEqSymbOf S*>^t2^t3}, <*TheEqSymbOf S*>^t1^t3]); pred seqt Rule3b Seqts means :: FOMODEL4:def 25 ex t1,t2 being termal string of S st seqt`1 = {<*TheEqSymbOf S*>^t1^t2} & seqt`2 = <*TheEqSymbOf S*>^t2^t1; pred seqt Rule3d Seqts means :: FOMODEL4:def 26 ex s being low-compounding Element of S, T,U being (|.ar s.|)-element Element of (AllTermsOf S)* st (s is operational & seqt`1= {<*TheEqSymbOf S*>^(TT.j)^(UU.j) where j is Element of Seg |.ar s.|, TT,UU is Function of Seg |.ar s.|, (AllSymbolsOf S)*\{{}} : TT=T & UU=U} & seqt`2=<*TheEqSymbOf S*>^(s-compound(T))^(s-compound(U))); pred seqt Rule3e Seqts means :: FOMODEL4:def 27 ex s being relational Element of S, T,U being (|.ar s.|)-element Element of (AllTermsOf S)* st (seqt`1={s-compound(T)} \/ {<*TheEqSymbOf S*>^(TT.j)^(UU.j) where j is Element of Seg |.ar s.|, TT,UU is Function of Seg |.ar s.|, (AllSymbolsOf S)*\{{}} : TT=T & UU=U} & seqt`2=s-compound(U)); pred seqt Rule4 Seqts means :: FOMODEL4:def 28 ex l being literal Element of S, phi being wff string of S, t being termal string of S st seqt`1={(l,t) SubstIn phi} & seqt`2=<*l*>^phi; pred seqt Rule5 Seqts means :: FOMODEL4:def 29 ex v1,v2 being literal Element of S, x,p st seqt`1=x \/ {<*v1*>^p} & v2 is (x\/{p}\/{seqt`2})-absent & [x\/{(v1 SubstWith v2).p},seqt`2] in Seqts; pred seqt Rule6 Seqts means :: FOMODEL4:def 30 ex y1,y2 being set,phi1, phi2 being wff string of S st y1 in Seqts & y2 in Seqts & y1`1 = y2`1 & y2`1=seqt`1 & y1`2= <*TheNorSymbOf S*> ^ phi1 ^ phi1 & y2`2= <*TheNorSymbOf S*> ^ phi2 ^ phi2 & seqt`2 = <*TheNorSymbOf S*> ^ phi1 ^ phi2; pred seqt Rule7 Seqts means :: FOMODEL4:def 31 ex y being set, phi1, phi2 being wff string of S st y in Seqts & y`1 = seqt`1 & y`2 =<* TheNorSymbOf S*> ^ phi1 ^ phi2 & seqt`2 = <* TheNorSymbOf S*> ^ phi2 ^ phi1; pred seqt Rule8 Seqts means :: FOMODEL4:def 32 ex y1,y2 being set, phi,phi1,phi2 being wff string of S st y1 in Seqts & y2 in Seqts & y1`1=y2`1 & y1`2=phi1 & y2`2 = <* TheNorSymbOf S *> ^ phi1 ^ phi2 & {phi}\/seqt`1=y1`1 & seqt`2= <* TheNorSymbOf S *> ^ phi ^ phi; pred seqt Rule9 Seqts means :: FOMODEL4:def 33 ex y being set, phi being wff string of S st y in Seqts & seqt`2=phi & y`1=seqt`1 & y`2=xnot (xnot phi); end; definition let S be Language; func P#0(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 34 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule0 Seqts; func P#1(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 35 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule1 Seqts; func P#2(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 36 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule2 Seqts; func P#3a(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 37 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule3a Seqts; func P#3b(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 38 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule3b Seqts; func P#3d(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 39 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule3d Seqts; func P#3e(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 40 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule3e Seqts; func P#4(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 41 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule4 Seqts; func P#5(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 42 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule5 Seqts; func P#6(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 43 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule6 Seqts; func P#7(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 44 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule7 Seqts; func P#8(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 45 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule8 Seqts; func P#9(S) -> Relation of bool (S-sequents), S-sequents means :: FOMODEL4:def 46 for Seqts being Element of bool (S-sequents), seqt being Element of (S-sequents) holds [ Seqts, seqt ] in it iff seqt Rule9 Seqts; end; definition let S; let R be Relation of bool (S-sequents), S-sequents; func FuncRule(R) -> Rule of S means :: FOMODEL4:def 47 for inseqs being set st inseqs in bool (S-sequents) holds it.inseqs = { x where x is Element of S-sequents : [inseqs, x] in R}; end; theorem :: FOMODEL4:3 for R being Relation of bool (S-sequents), S-sequents st [SQ, Sq] in R holds Sq in (FuncRule(R)).SQ; definition let S; func R#0(S) -> Rule of S equals :: FOMODEL4:def 48 FuncRule(P#0(S)); func R#1(S) -> Rule of S equals :: FOMODEL4:def 49 FuncRule(P#1(S)); func R#2(S) -> Rule of S equals :: FOMODEL4:def 50 FuncRule(P#2(S)); func R#3a(S) -> Rule of S equals :: FOMODEL4:def 51 FuncRule(P#3a(S)); func R#3b(S) -> Rule of S equals :: FOMODEL4:def 52 FuncRule(P#3b(S)); func R#3d(S) -> Rule of S equals :: FOMODEL4:def 53 FuncRule(P#3d(S)); func R#3e(S) -> Rule of S equals :: FOMODEL4:def 54 FuncRule(P#3e(S)); func R#4(S) -> Rule of S equals :: FOMODEL4:def 55 FuncRule(P#4(S)); func R#5(S) -> Rule of S equals :: FOMODEL4:def 56 FuncRule(P#5(S)); func R#6(S) -> Rule of S equals :: FOMODEL4:def 57 FuncRule(P#6(S)); func R#7(S) -> Rule of S equals :: FOMODEL4:def 58 FuncRule(P#7(S)); func R#8(S) -> Rule of S equals :: FOMODEL4:def 59 FuncRule(P#8(S)); func R#9(S) -> Rule of S equals :: FOMODEL4:def 60 FuncRule(P#9(S)); end; registration let S; let t be termal string of S; cluster {[{},<*TheEqSymbOf S*>^t^t]} -> {R#2(S)}-derivable for set; end; registration let S; cluster R#1(S) -> isotone for Rule of S; end; registration let S; cluster R#2(S) -> isotone for Rule of S; end; registration let S; cluster R#3b(S) -> isotone for Rule of S; end; registration let S; let phi be wff string of S, Phi be finite Subset of AllFormulasOf S; cluster [Phi \/ {phi}, phi] -> (1,{},{R#0(S)})-derivable for object; end; registration let S; let phi1,phi2 be wff string of S; cluster [{phi1,phi2},phi1] -> (1,{},{R#0(S)})-derivable for object; end; registration let S,phi; cluster [{phi},phi] -> (1,{},{R#0(S)})-derivable for object; end; registration let S; let phi be wff string of S; cluster {[{phi}, phi]} -> ({},{R#0(S)})-derivable for set; end; registration let S; cluster R#0(S) -> isotone for Rule of S; cluster R#3a(S) -> isotone for Rule of S; cluster R#3d(S) -> isotone for Rule of S; cluster R#3e(S) -> isotone for Rule of S; let K1,K2; cluster K1\/K2 -> isotone for RuleSet of S; end; registration let S; cluster R#6(S) -> isotone for Rule of S; end; registration let S; cluster R#8(S) -> isotone for Rule of S; end; registration let S; cluster R#7(S) -> isotone for Rule of S; end; registration let S,t1,t2,t3; cluster [{<*TheEqSymbOf S*>^t1^t2, <*TheEqSymbOf S*>^t2^t3}, <*TheEqSymbOf S*>^t1^t3] -> (1,{},{R#3a(S)})-derivable for object; end; registration let S, H1, H2, phi; cluster [H1\/H2, phi] -> (1,{[H1,phi]},{R#1(S)})-derivable for object; end; registration let S,H,phi; cluster [H\/{phi}, phi] -> (1,{},{R#0(S)})-derivable for object; end; registration let S, H, phi1, phi2; cluster [H, <*TheNorSymbOf S*>^phi2^phi1] -> (1, {[H,<*TheNorSymbOf S*>^phi1^phi2]},{R#7(S)})-derivable for object; end; registration let S,Sq; cluster Sq`1 -> S-premises-like for set; end; registration let S,phi1,phi2,l1,H; let l2 be (H\/{phi1}\/{phi2})-absent literal Element of S; cluster [(H\/{<*l1*>^phi1}) null l2, phi2] -> (1,{[H\/{(l1,l2)-SymbolSubstIn phi1}, phi2]},{R#5(S)})-derivable for object; end; registration let m1, S, H1, H2, phi; cluster [(H1\/H2) null m1, phi] -> (m1,{[H1,phi]}, {R#1(S)})-derivable for object; end; registration let S; cluster non empty for isotone RuleSet of S; end; registration let S; cluster R#5(S) -> isotone for Rule of S; end; registration let S,l,t,phi; cluster [{(l,t) SubstIn phi}, <*l*>^phi] -> (1,{},{R#4(S)})-derivable for object; end; registration let S, H, phi, phi1, phi2; cluster [H null (phi1^phi2),xnot phi] -> (1, {[H\/{phi},phi1],[H\/{phi},<*TheNorSymbOf S*>^phi1^phi2]}, {R#8(S)})-derivable for object; end; registration let S; cluster R#4(S) -> isotone for Rule of S; end; begin definition let S; let m be non zero Nat; let T,U be m-element (Element of ((AllTermsOf S)*)); func PairWiseEq (T,U) -> set equals :: FOMODEL4:def 61 {<*TheEqSymbOf S*>^(TT.j)^(UU.j) where j is Element of Seg m, TT,UU is Function of Seg m, (AllSymbolsOf S)*\{{}} : TT=T & UU=U}; end; definition let S; let m be non zero Nat, T1,T2 be m-element Element of ((AllTermsOf S)*); redefine func PairWiseEq (T1,T2) -> Subset of AllFormulasOf S; end; registration let S; let m be non zero Nat; let T,U be m-element (Element of ((AllTermsOf S)*)); cluster PairWiseEq(T,U) -> finite; end; registration let S; let s be relational Element of S; let T1,T2 be |.ar s.|-element Element of (AllTermsOf S)*; cluster {[PairWiseEq(T1,T2)\/{s-compound(T1)},s-compound(T2)]} -> ({},{R#3e(S)})-derivable; end; definition let m,S,D; attr D is m-ranked means :: FOMODEL4:def 62 R#0(S) in D & R#2(S) in D & R#3a(S) in D & R#3b(S) in D if m=0, R#0(S) in D & R#2(S) in D & R#3a(S) in D & R#3b(S) in D & R#3d(S) in D & R#3e(S) in D if m=1, R#0(S) in D & R#1(S) in D & R#2(S) in D & R#3a(S) in D & R#3b(S) in D & R#3d(S) in D & R#3e(S) in D & R#4(S) in D & R#5(S) in D & R#6(S) in D & R#7(S) in D & R#8(S) in D if m=2 otherwise D={}; end; registration let S; cluster 1-ranked -> 0-ranked for RuleSet of S; cluster 2-ranked -> 1-ranked for RuleSet of S; end; definition let S; func S-rules -> RuleSet of S equals :: FOMODEL4:def 63 {R#0(S), R#1(S), R#2(S), R#3a(S), R#3b(S), R#3d(S), R#3e(S), R#4(S)} \/ {R#5(S), R#6(S), R#7(S), R#8(S)}; end; registration let S; cluster S-rules -> 2-ranked for RuleSet of S; end; registration let S; cluster 2-ranked for RuleSet of S; end; registration let S; cluster 1-ranked for RuleSet of S; end; registration let S; cluster 0-ranked for RuleSet of S; end; registration let S; let D be 1-ranked RuleSet of S; let X be D-expanded set; let a; cluster X-freeInterpreter(a) -> ((X,D)-termEq)-respecting for Interpreter of a, AllTermsOf S; end; registration let S; let D be 0-ranked RuleSet of S; let X be D-expanded set; cluster ((X,D)-termEq) -> total symmetric transitive for Relation of (AllTermsOf S); end; registration let S; cluster 1-ranked for 0-ranked RuleSet of S; end; theorem :: FOMODEL4:4 D1 c= D2 & (D2 is isotone or D1 is isotone) & Y is (X,D1)-derivable implies Y is (X,D2)-derivable; registration let S, H, phi1, phi2; cluster [H null phi2,xnot phi1] -> (2, {[H,<*TheNorSymbOf S*>^phi1^phi2]},{R#0(S)}\/{R#1(S)}\/{R#8(S)})-derivable; end; registration let S, H, phi1, phi2; cluster [H null phi1, xnot phi2] -> (3,{[H,<*TheNorSymbOf S*>^phi1^phi2]},{R#0(S)}\/{R#1(S)}\/{R#8(S)}\/{R#7(S)}) -derivable for object; end; registration let S, phi1, phi2; cluster [{xnot phi1, xnot phi2},<*TheNorSymbOf S*>^phi1^phi2] -> (1, {[{xnot phi1,xnot phi2}, xnot phi1], [{xnot phi1, xnot phi2}, xnot phi2]}, {R#6(S)})-derivable for object; end; registration let S,phi1,phi2; cluster [{phi1,phi2},phi2] -> (1,{},{R#0(S)})-derivable for object; end; theorem :: FOMODEL4:5 x in R.X implies x is (1,X,{R})-derivable; theorem :: FOMODEL4:6 phi in X implies phi is (X,{R#0(S)})-provable; theorem :: FOMODEL4:7 (D1\/D2 is isotone & D1\/D2\/D3 is isotone & x is (m,SQ1,D1)-derivable & y is (m,SQ2,D2)-derivable & z is (n,{x,y},D3)-derivable) implies z is (m+n,SQ1\/SQ2,D1\/D2\/D3)-derivable; ::#generalizing Lm28 theorem :: FOMODEL4:8 (D1 is isotone & D1\/D2 is isotone & y is (m,X,D1)-derivable & z is (n,{y},D2)-derivable) implies z is (m+n,X,D1\/D2)-derivable; theorem :: FOMODEL4:9 x is (m,X,D)-derivable implies {x} is (X,D)-derivable; theorem :: FOMODEL4:10 (D1 c= D2 & (D1 is isotone or D2 is isotone) & x is (X,D1)-provable) implies x is (X,D2)-provable; theorem :: FOMODEL4:11 X c= Y & x is (X,D)-provable implies x is (Y,D)-provable; theorem :: FOMODEL4:12 x is (X,D)-provable implies x is wff string of S; reserve D,E,F for (RuleSet of S), D1 for 1-ranked 0-ranked RuleSet of S; registration let S, D1; let X be D1-expanded set; cluster (S,X)-freeInterpreter -> ((X,D1)-termEq)-respecting for (S,AllTermsOf S)-interpreter-like Function; end; definition let S; let D be 0-ranked RuleSet of S; let X be D-expanded set; func D Henkin X -> Function equals :: FOMODEL4:def 64 (S,X)-freeInterpreter quotient ((X,D)-termEq); end; registration let S; let D be 0-ranked RuleSet of S; let X be D-expanded set; cluster D Henkin X -> (OwnSymbolsOf S)-defined; end; registration let S, D1; let X be D1-expanded set; cluster D1 Henkin X -> (S,Class (X,D1)-termEq)-interpreter-like for Function; end; definition let S, D1; let X be D1-expanded set; redefine func D1 Henkin X -> Element of (Class (X,D1)-termEq)-InterpretersOf S; end; registration let S, phi1, phi2; cluster <*TheNorSymbOf S*>^phi1^phi2 -> ({xnot phi1, xnot phi2},{R#0(S)}\/{R#6(S)})-provable for set; end; registration let S; cluster -> non empty for 0-ranked RuleSet of S; end; definition let S,X; attr X is S-witnessed means :: FOMODEL4:def 65 for l1, phi1 st <*l1*>^phi1 in X ex l2 st ( (l1,l2)-SymbolSubstIn phi1 in X & not l2 in rng phi1); end; notation let S,D,X; antonym X is D-consistent for X is D-inconsistent; end; theorem :: FOMODEL4:13 for X being Subset of Y st X is D-inconsistent holds Y is D-inconsistent; definition let S,D; let X be functional set; let phi be Element of ExFormulasOf S; func (D,phi) AddAsWitnessTo X -> set equals :: FOMODEL4:def 66 X\/{ (S-firstChar.phi, the Element of ( LettersOf S \ SymbolsOf (((AllSymbolsOf S)*\{{}})/\(X\/{head phi})) ))-SymbolSubstIn (head phi) } if X\/{phi} is D-consistent & LettersOf S \ SymbolsOf (((AllSymbolsOf S)*\{{}})/\(X\/{head phi}))<>{} otherwise X; end; registration let S,D; let X be functional set; let phi be Element of ExFormulasOf S; cluster X \ ((D,phi) AddAsWitnessTo X) -> empty for set; end; registration let S,D; let X be functional set; let phi be Element of ExFormulasOf S; cluster ((D,phi) AddAsWitnessTo X)\X -> trivial for set; end; definition let S,D; let X be functional set; let phi be Element of ExFormulasOf S; redefine func (D,phi) AddAsWitnessTo X -> Subset of (X\/AllFormulasOf S); end; definition let S,D; attr D is Correct means :: FOMODEL4:def 67 for phi, X st phi is (X,D)-provable holds for U for I being Element of U-InterpretersOf S st X is I-satisfied holds I-TruthEval phi=1; end; registration let S, t1, t2; cluster SubTerms (<*TheEqSymbOf S*>^t1^t2) \+\ <*t1, t2*> -> empty for set; end; definition let S; let R be Rule of S; attr R is Correct means :: FOMODEL4:def 68 X is S-correct implies R.X is S-correct; end; registration let S; cluster R#0(S) -> Correct for Rule of S; end; registration let S; cluster Correct for Rule of S; end; registration let S; cluster R#1(S) -> Correct for Rule of S; end; registration let S; cluster R#2(S) -> Correct for Rule of S; end; registration let S; cluster R#3a(S) -> Correct for Rule of S; end; registration let S; cluster R#3b(S) -> Correct for Rule of S; end; registration let S; cluster R#3d(S) -> Correct for Rule of S; end; registration let S; cluster R#3e(S) -> Correct for Rule of S; end; registration let S; cluster R#4(S) -> Correct for Rule of S; end; registration let S; cluster R#5(S) -> Correct for Rule of S; end; registration let S; cluster R#6(S) -> Correct for Rule of S; end; registration let S; cluster R#7(S) -> Correct for Rule of S; end; registration let S; cluster R#8(S) -> Correct for Rule of S; end; theorem :: FOMODEL4:14 (for R being Rule of S st R in D holds R is Correct) implies D is Correct; registration let S; let R be Correct Rule of S; cluster {R} -> Correct for RuleSet of S; end; registration let S; cluster S-rules -> Correct for RuleSet of S; end; registration let S; cluster R#9(S) -> isotone for Rule of S; end; registration let S,H,phi; cluster [H,phi] null 1 -> (1,{[H,xnot(xnot phi)]},{R#9(S)})-derivable for set; end; registration let X, S; cluster X-implied for 0-wff string of S; end; registration let X, S; cluster X-implied for wff string of S; end; registration let S, X; let phi be X-implied wff string of S; cluster xnot xnot phi -> X-implied for wff string of S; end; definition let X, S, phi; attr phi is X-provable means :: FOMODEL4:def 69 phi is (X,{R#9(S)}\/S-rules)-provable; end; registration let S; let r1, r2 be isotone Rule of S; cluster {r1,r2} -> isotone for RuleSet of S; end; registration let S; let r1, r2, r3 ,r4 be isotone Rule of S; cluster {r1,r2,r3,r4} -> isotone for RuleSet of S; end; registration let S; cluster S-rules -> isotone for RuleSet of S; end; registration let S; cluster Correct for isotone RuleSet of S; end; registration let S; cluster 2-ranked for Correct isotone RuleSet of S; end; theorem :: FOMODEL4:15 for X being D1-expanded set, phi being 0wff string of S holds ((D1 Henkin X)-AtomicEval phi = 1 iff phi in X); theorem :: FOMODEL4:16 for X being D1-expanded set st ::# Henkin's theorem R#1(S) in D1 & R#4(S) in D1 & R#6(S) in D1 & R#7(S) in D1 & R#8(S) in D1 & X is S-mincover & X is S-witnessed holds (D1 Henkin X)-TruthEval psi = 1 iff psi in X; definition let S,D,X; attr X is D-inconsistentStrong means :: FOMODEL4:def 70 phi is (X,D)-provable; end; notation let S,D,X; antonym X is D-consistentWeak for X is D-inconsistentStrong; end; begin ::# constructions for countable languages-witness adjoining definition let X be functional set; let S,D; let num be sequence of ExFormulasOf S; func (D,num) AddWitnessesTo X -> sequence of bool (X\/AllFormulasOf S) means :: FOMODEL4:def 71 it.0=X & for mm holds it.(mm+1)=(D, num.mm) AddAsWitnessTo (it.mm); end; notation let X be functional set; let S,D; let num be sequence of ExFormulasOf S; synonym (D,num) addw X for (D,num) AddWitnessesTo X; end; theorem :: FOMODEL4:17 for X being functional set, num being sequence of ExFormulasOf S st D is isotone & R#1(S) in D & R#8(S) in D & R#2(S) in D & R#5(S) in D & LettersOf S\SymbolsOf (X/\((AllSymbolsOf S)*\{{}})) is infinite & X is D-consistent holds ((D,num) addw X).k c= ((D,num) addw X).(k+m) & LettersOf S\SymbolsOf (((D,num) addw X).m/\((AllSymbolsOf S)*\{{}})) is infinite & ((D,num) addw X).m is D-consistent; definition let X be functional set; let S,D; let num be sequence of ExFormulasOf S; func X WithWitnessesFrom (D,num) -> Subset of (X\/AllFormulasOf S) equals :: FOMODEL4:def 72 union rng (D,num) AddWitnessesTo X; end; notation let X be functional set; let S,D; let num be sequence of ExFormulasOf S; synonym X addw (D,num) for X WithWitnessesFrom (D,num); end; registration let X be functional set; let S,D; let num be sequence of ExFormulasOf S; cluster X\ (X addw (D,num)) -> empty for set; end; theorem :: FOMODEL4:18 for X being functional set, num being sequence of ExFormulasOf S st D is isotone & R#1(S) in D & R#8(S) in D & R#2(S) in D & R#5(S) in D & LettersOf S\SymbolsOf (X/\((AllSymbolsOf S)*\{{}})) is infinite & X addw (D,num) c= Z & Z is D-consistent & rng num = ExFormulasOf S holds Z is S-witnessed; begin ::# constructions for countable languages ::# Consistently maximizing a set of formulas (Lindenbaum's lemma) ::# of a countable language definition let X,S,D; let phi be Element of AllFormulasOf S; func (D,phi) AddFormulaTo X equals :: FOMODEL4:def 73 X\/{phi} if not xnot phi is (X,D)-provable otherwise X \/ {xnot phi}; end; definition let X,S,D; let phi be Element of AllFormulasOf S; redefine func (D,phi) AddFormulaTo X -> Subset of (X\/AllFormulasOf S); end; registration let X,S,D; let phi be Element of AllFormulasOf S; cluster X \ ((D,phi) AddFormulaTo X) -> empty for set; end; definition let X,S,D; let num be sequence of AllFormulasOf S; func (D,num) AddFormulasTo X -> sequence of bool (X\/AllFormulasOf S) means :: FOMODEL4:def 74 it.0=X & for m holds it.(m+1)=(D,num.m) AddFormulaTo (it.m); end; definition let X,S,D; let num be sequence of AllFormulasOf S; func (D,num) CompletionOf X -> Subset of (X\/AllFormulasOf S) equals :: FOMODEL4:def 75 union rng ((D,num) AddFormulasTo X); end; registration let X,S,D; let num be sequence of AllFormulasOf S; cluster X\((D,num) CompletionOf X) -> empty for set; end; definition let S; func S-diagFormula -> Function equals :: FOMODEL4:def 76 the set of all [tt,<*TheEqSymbOf S*>^tt^tt]; end; definition let S; redefine func S-diagFormula -> Function of AllTermsOf S, AtomicFormulasOf S; end; registration let S; cluster S-diagFormula -> one-to-one for Function; end; begin ::#Satisfiability, completeness and Lowenheim-Skolem theorems reserve D2 for 2-ranked RuleSet of S; theorem :: FOMODEL4:19 for S being countable Language, D being RuleSet of S st D is 2-ranked & D is isotone & D is Correct & Z is D-consistent & Z c= AllFormulasOf S ex U being non empty countable set, I being Element of U-InterpretersOf S st Z is I-satisfied; reserve C for countable Language, phi for wff string of C; theorem :: FOMODEL4:20 ::#Goedel's completeness theorem (X c= AllFormulasOf C & phi is X-implied) implies phi is X-provable; ::# countable downward Lowenheim-Skolem theorem ("weak version", Skolem 1922) ::# cfr. Ebbinghaus-Flum-Thomas, theorem VI.1.1 theorem :: FOMODEL4:21 for X2 being countable Subset of AllFormulasOf S2, I2 being Element of U-InterpretersOf S2 st X2 is I2-satisfied ex U1 being countable non empty set, I1 being Element of U1-InterpretersOf S2 st X2 is I1-satisfied;