:: Sequent calculus, derivability, provability. Goedel's completeness theorem
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2019 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, XCMPLX_0, NAT_1, RELAT_1, NUMBERS, REAL_1, FUNCT_1,
INT_1, FINSEQ_1, XREAL_0, FUNCT_2, FINSEQ_2, SUBSET_1, RELSET_1,
PARTFUN1, EQREL_1, FINSEQ_6, PRE_POLY, CARD_1, XBOOLE_0, XXREAL_0,
ZFMISC_1, SETFAM_1, MARGREL1, MATROID0, SIMPLEX0, FINSET_1, RAMSEY_1,
YELLOW12, FUNCOP_1, CARD_3, COHSP_1, 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;