:: Sequent calculus, derivability, provability. Goedel's completeness theorem.
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users

begin

Lm7: for X, A, B being set st X is Subset of (Funcs (A,B)) holds
X is Subset-Family of [:A,B:]

proof end;

Lm10: for S being Language
for t1, t2 being termal string of S holds (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S

proof end;

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 } ;
coherence
{ [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite } is set ;

end;

:: deftheorem defines -sequents FOMODEL4:def 1 :
for S being Language holds S -sequents = { [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite } ;

registration

let S be Language;
cluster S -sequents -> non empty ;
coherence
not S -sequents is empty

proof end;

end;

registration

let S be Language;
cluster S -sequents -> Relation-like ;
coherence
S -sequents is Relation-like

proof end;

end;

definition

let S be Language;
let x be set ;
attr x is S -sequent-like means :DefSeqtLike: :: FOMODEL4:def 2
x in S -sequents ;

end;

:: deftheorem DefSeqtLike defines -sequent-like FOMODEL4:def 2 :
for S being Language
for x being set holds
( x is S -sequent-like iff x in S -sequents );

definition

let S be Language;
let X be set ;
attr X is S -sequents-like means :DefSeqtLike2: :: FOMODEL4:def 3
X c= S -sequents ;

end;

:: deftheorem DefSeqtLike2 defines -sequents-like FOMODEL4:def 3 :
for S being Language
for X being set holds
( X is S -sequents-like iff X c= S -sequents );

registration

let S be Language;
cluster -> S -sequents-like Element of bool (S -sequents);
coherence
for b₁ being Subset of (S -sequents) holds b₁ is S -sequents-like by DefSeqtLike2;
cluster -> S -sequent-like Element of S -sequents ;
coherence
for b₁ being Element of S -sequents holds b₁ is S -sequent-like by DefSeqtLike;

end;

registration

let S be Language;
cluster S -sequent-like Element of S -sequents ;
existence
ex b₁ being Element of S -sequents st b₁ is S -sequent-like

proof end;

cluster Relation-like S -sequents-like Element of bool (S -sequents);
existence
ex b₁ being Subset of (S -sequents) st b₁ is S -sequents-like

proof end;

end;

registration

let S be Language;
cluster S -sequent-like set ;
existence
ex b₁ being set st b₁ is S -sequent-like

proof end;

cluster S -sequents-like set ;
existence
ex b₁ being set st b₁ is S -sequents-like

proof end;

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;

registration

let A, B be set ;
let X be Subset of (Funcs (A,B));
cluster union X -> Relation-like ;
coherence
union X is Relation-like ;

end;

registration

let S be Language;
let D be RuleSet of S;
cluster union D -> Relation-like ;
coherence
union D is Relation-like ;

end;

definition

let S be Language;
let D be RuleSet of S;
func OneStep D -> Rule of S means :Def1Step: :: FOMODEL4:def 4
for Seqs being Element of bool (S -sequents) holds it . Seqs = union ((union D) .: {Seqs});
existence
ex b₁ being Rule of S st
for Seqs being Element of bool (S -sequents) holds b₁ . Seqs = union ((union D) .: {Seqs})

proof end;

uniqueness
for b₁, b₂ being Rule of S st ( for Seqs being Element of bool (S -sequents) holds b₁ . Seqs = union ((union D) .: {Seqs}) ) & ( for Seqs being Element of bool (S -sequents) holds b₂ . Seqs = union ((union D) .: {Seqs}) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1Step defines OneStep FOMODEL4:def 4 :
for S being Language
for D being RuleSet of S
for b₃ being Rule of S holds
( b₃ = OneStep D iff for Seqs being Element of bool (S -sequents) holds b₃ . Seqs = union ((union D) .: {Seqs}) );

Lm4: for m being Nat
for S being Language
for D being RuleSet of S
for R being Rule of S
for Seqts being Subset of (S -sequents)
for SQ being b₂ -sequents-like set holds
( dom (OneStep D) = bool (S -sequents) & rng (OneStep D) c= dom (OneStep D) & iter ((OneStep D),m) is Function of (bool (S -sequents)),(bool (S -sequents)) & dom (iter ((OneStep D),m)) = bool (S -sequents) & (dom (OneStep D)) \/ (rng (OneStep D)) = bool (S -sequents) & Seqts in dom R & SQ in dom (iter (R,m)) )

proof end;

definition

let S be Language;
let D be RuleSet of S;
let m be Nat;
func (m,D) -derivables -> Rule of S equals :: FOMODEL4:def 5
iter ((OneStep D),m);
coherence
iter ((OneStep D),m) is Rule of S

proof end;

end;

:: deftheorem defines -derivables FOMODEL4:def 5 :
for S being Language
for D being RuleSet of S
for m being Nat holds (m,D) -derivables = iter ((OneStep D),m);

definition

let S be Language;
let D be RuleSet of S;
let Seqs1, Seqs2 be set ;
attr Seqs2 is Seqs1,D -derivable means :DefDerivable: :: FOMODEL4:def 6
Seqs2 c= union (((OneStep D) [*]) .: {Seqs1});

end;

:: deftheorem DefDerivable defines -derivable FOMODEL4:def 6 :
for S being Language
for D being RuleSet of S
for Seqs1, Seqs2 being set holds
( Seqs2 is Seqs1,D -derivable iff Seqs2 c= union (((OneStep D) [*]) .: {Seqs1}) );

definition

let m be Nat;
let S be Language;
let D be RuleSet of S;
let Seqts, seqt be set ;
attr seqt is m,Seqts,D -derivable means :DefDerivable3: :: FOMODEL4:def 7
seqt in ((m,D) -derivables) . Seqts;

end;

:: deftheorem DefDerivable3 defines -derivable FOMODEL4:def 7 :
for m being Nat
for S being Language
for D being RuleSet of S
for Seqts, seqt being set holds
( seqt is m,Seqts,D -derivable iff seqt in ((m,D) -derivables) . Seqts );

definition

let S be Language;
let D be RuleSet of S;
func D -iterators -> Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):] equals :: FOMODEL4:def 8
{ (iter ((OneStep D),mm)) where mm is Element of NAT : verum } ;
coherence
{ (iter ((OneStep D),mm)) where mm is Element of NAT : verum } is Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):]

proof end;

end;

:: deftheorem defines -iterators FOMODEL4:def 8 :
for S being Language
for D being RuleSet of S holds D -iterators = { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } ;

definition

let S be Language;
let R be Rule of S;
attr R is isotone means :DefMonotonic1: :: FOMODEL4:def 9
for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 holds
R . Seqts1 c= R . Seqts2;

end;

:: deftheorem DefMonotonic1 defines isotone FOMODEL4:def 9 :
for S being Language
for R being Rule of S holds
( R is isotone iff for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 holds
R . Seqts1 c= R . Seqts2 );

Lm16: for S being Language
for R being Rule of S holds
( id (bool (S -sequents)) is Rule of S & ( R = id (bool (S -sequents)) implies R is isotone ) )

proof end;

registration

let S be Language;
cluster Relation-like bool (S -sequents) -defined bool (S -sequents) -valued Function-like total quasi_total isotone Element of Funcs ((bool (S -sequents)),(bool (S -sequents)));
existence
ex b₁ being Rule of S st b₁ is isotone

proof end;

end;

definition

let S be Language;
let D be RuleSet of S;
attr D is isotone means :DefMonotonic2: :: FOMODEL4:def 10
for Seqts1, Seqts2 being Subset of (S -sequents)
for f being Function st Seqts1 c= Seqts2 & f in D holds
ex g being Function st
( g in D & f . Seqts1 c= g . Seqts2 );

end;

:: deftheorem DefMonotonic2 defines isotone FOMODEL4:def 10 :
for S being Language
for D being RuleSet of S holds
( D is isotone iff for Seqts1, Seqts2 being Subset of (S -sequents)
for f being Function st Seqts1 c= Seqts2 & f in D holds
ex g being Function st
( g in D & f . Seqts1 c= g . Seqts2 ) );

registration

let S be Language;
let M be isotone Rule of S;
cluster {M} -> isotone RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = {M} holds
b₁ is isotone

proof end;

end;

registration

let S be Language;
cluster functional isotone Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
ex b₁ being RuleSet of S st b₁ is isotone

proof end;

end;

definition

let S be Language;
let D be RuleSet of S;
let Seqts be set ;
attr Seqts is D -derivable means :DefDerivable2: :: FOMODEL4:def 11
Seqts is {} ,D -derivable ;

end;

:: deftheorem DefDerivable2 defines -derivable FOMODEL4:def 11 :
for S being Language
for D being RuleSet of S
for Seqts being set holds
( Seqts is D -derivable iff Seqts is {} ,D -derivable );

registration

let S be Language;
let D be RuleSet of S;
cluster D -derivable -> {} ,D -derivable set ;
coherence
for b₁ being set st b₁ is D -derivable holds
b₁ is {} ,D -derivable by DefDerivable2;
cluster {} ,D -derivable -> D -derivable set ;
coherence
for b₁ being set st b₁ is {} ,D -derivable holds
b₁ is D -derivable by DefDerivable2;

end;

registration

let S be Language;
let D be RuleSet of S;
let Seqts be empty set ;
cluster Seqts,D -derivable -> D -derivable set ;
coherence
for b₁ being set st b₁ is Seqts,D -derivable holds
b₁ is D -derivable ;

end;

definition

let S be Language;
let D be RuleSet of S;
let X, phi be set ;
attr phi is X,D -provable means :DefProvable: :: FOMODEL4:def 12
( {[X,phi]} is D -derivable or ex seqt being set st
( seqt `1 c= X & seqt `2 = phi & {seqt} is D -derivable ) );

end;

:: deftheorem DefProvable defines -provable FOMODEL4:def 12 :
for S being Language
for D being RuleSet of S
for X, phi being set holds
( phi is X,D -provable iff ( {[X,phi]} is D -derivable or ex seqt being set st
( seqt `1 c= X & seqt `2 = phi & {seqt} is D -derivable ) ) );

definition

let S be Language;
let D be RuleSet of S;
let X, x be set ;
redefine attr x is X,D -provable means :DefProvable2: :: FOMODEL4:def 13
ex seqt being set st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable );
compatibility
( x is X,D -provable iff ex seqt being set st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) )

proof end;

end;

:: deftheorem DefProvable2 defines -provable FOMODEL4:def 13 :
for S being Language
for D being RuleSet of S
for X, x being set holds
( x is X,D -provable iff ex seqt being set st
( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) );

definition

let S be Language;
let D be RuleSet of S;
let R be Rule of S;
attr R is D -macro means :: FOMODEL4:def 14
for Seqs being Subset of (S -sequents) holds R . Seqs is Seqs,D -derivable ;

end;

:: deftheorem defines -macro FOMODEL4:def 14 :
for S being Language
for D being RuleSet of S
for R being Rule of S holds
( R is D -macro iff for Seqs being Subset of (S -sequents) holds R . Seqs is Seqs,D -derivable );

definition

let S be Language;
let D be RuleSet of S;
let Phi be set ;
func (Phi,D) -termEq -> set equals :: FOMODEL4:def 15
{ [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } ;
coherence
{ [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } is set ;

end;

:: deftheorem defines -termEq FOMODEL4:def 15 :
for S being Language
for D being RuleSet of S
for Phi being set holds (Phi,D) -termEq = { [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } ;

definition

let S be Language;
let D be RuleSet of S;
let Phi be set ;
attr Phi is D -expanded means :DefExpanded: :: FOMODEL4:def 16
for x being set st x is Phi,D -provable holds
{x} c= Phi;

end;

:: deftheorem DefExpanded defines -expanded FOMODEL4:def 16 :
for S being Language
for D being RuleSet of S
for Phi being set holds
( Phi is D -expanded iff for x being set st x is Phi,D -provable holds
{x} c= Phi );

definition

let S be Language;
let x be set ;
attr x is S -null means :DefNull: :: FOMODEL4:def 17
verum;

end;

:: deftheorem DefNull defines -null FOMODEL4:def 17 :
for S being Language
for x being set holds
( x is S -null iff verum );

Lm31: for X, Y, x being set
for S being Language
for D being RuleSet of S st X c= Y & x is X,D -provable holds
x is Y,D -provable

proof end;

definition

let S be Language;
let D be RuleSet of S;
let Phi be set ;
:: original: -termEq
redefine func (Phi,D) -termEq -> Relation of (AllTermsOf S);
coherence
(Phi,D) -termEq is Relation of (AllTermsOf S)

proof end;

end;

registration

let S be Language;
let phi be wff string of S;
let Phi1, Phi2 be finite Subset of (AllFormulasOf S);
cluster [(Phi1 \/ Phi2),phi] -> S -sequent-like ;
coherence
[(Phi1 \/ Phi2),phi] is S -sequent-like

proof end;

end;

definition

let S be Language;
let x be empty set ;
let phi be wff string of S;
:: original: [
redefine func [x,phi] -> Element of S -sequents ;
coherence
[x,phi] is Element of S -sequents

proof end;

end;

registration

let S be Language;
cluster {} /\ S -> S -sequents-like set ;
coherence
for b₁ being set st b₁ = {} /\ S holds
b₁ is S -sequents-like

proof end;

end;

registration

let S be Language;
cluster S -null set ;
existence
ex b₁ being set st b₁ is S -null by DefNull;

end;

registration

let S be Language;
cluster S -sequent-like -> S -null set ;
coherence
for b₁ being set st b₁ is S -sequent-like holds
b₁ is S -null by DefNull;

end;

registration

let S be Language;
cluster -> S -null Element of S -sequents ;
coherence
for b₁ being Element of S -sequents holds b₁ is S -null ;

end;

registration

let m be Nat;
let S be Language;
let D be RuleSet of S;
let X be set ;
cluster ((m,D) -derivables) . X -> S -sequents-like ;
coherence
((m,D) -derivables) . X is S -sequents-like

proof end;

end;

registration

let S be Language;
let Y be set ;
let X be S -sequents-like set ;
cluster X /\ Y -> S -sequents-like set ;
coherence
for b₁ being set st b₁ = X /\ Y holds
b₁ is S -sequents-like

proof end;

end;

registration

let S be Language;
let D be RuleSet of S;
let m be Nat;
let X be set ;
cluster m,X,D -derivable -> S -sequent-like set ;
coherence
for b₁ being set st b₁ is m,X,D -derivable holds
b₁ is S -sequent-like

proof end;

end;

registration

let S be Language;
let D be RuleSet of S;
let Phi1, Phi2 be set ;
cluster Phi1 \ Phi2,D -provable -> Phi1,D -provable set ;
coherence
for b₁ being set st b₁ is Phi1 \ Phi2,D -provable holds
b₁ is Phi1,D -provable by Lm31;

end;

registration

let S be Language;
let D be RuleSet of S;
let Phi1, Phi2 be set ;
cluster Phi1 \ Phi2,D -provable -> Phi1 \/ Phi2,D -provable set ;
coherence
for b₁ being set st b₁ is Phi1 \ Phi2,D -provable holds
b₁ is Phi1 \/ Phi2,D -provable by XBOOLE_1:7, Lm31;

end;

registration

let S be Language;
let D be RuleSet of S;
let Phi1, Phi2 be set ;
cluster Phi1 /\ Phi2,D -provable -> Phi1,D -provable set ;
coherence
for b₁ being set st b₁ is Phi1 /\ Phi2,D -provable holds
b₁ is Phi1,D -provable by Lm31;

end;

registration

let S be Language;
let D be RuleSet of S;
let X be set ;
let x be Subset of X;
cluster x,D -provable -> X,D -provable set ;
coherence
for b₁ being set st b₁ is x,D -provable holds
b₁ is X,D -provable

proof end;

end;

registration

let S be Language;
let premises be finite Subset of (AllFormulasOf S);
let phi be wff string of S;
cluster [premises,phi] -> S -sequent-like set ;
coherence
for b₁ being set st b₁ = [premises,phi] holds
b₁ is S -sequent-like

proof end;

end;

registration

let S be Language;
let phi1, phi2 be wff string of S;
cluster [{phi1},phi2] -> S -sequent-like set ;
coherence
for b₁ being set st b₁ = [{phi1},phi2] holds
b₁ is S -sequent-like

proof end;

let phi3 be wff string of S;
cluster [{phi1,phi2},phi3] -> S -sequent-like set ;
coherence
for b₁ being set st b₁ = [{phi1,phi2},phi3] holds
b₁ is S -sequent-like

proof end;

end;

registration

let S be Language;
let phi1, phi2 be wff string of S;
let Phi be finite Subset of (AllFormulasOf S);
cluster [(Phi \/ {phi1}),phi2] -> S -sequent-like set ;
coherence
for b₁ being set st b₁ = [(Phi \/ {phi1}),phi2] holds
b₁ is S -sequent-like

proof end;

end;

Lm13: for X being set
for S being Language
for D being RuleSet of S st X c= S -sequents holds
(OneStep D) . X = union (union { (R .: {X}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } )

proof end;

Lm8: for S being Language
for R being Rule of S holds R = OneStep {R}

proof end;

Lm3: for y being set
for S being Language
for D being RuleSet of S
for Seqts being Subset of (S -sequents) st {y} is Seqts,D -derivable holds
ex mm being Element of NAT st y is mm,Seqts,D -derivable

proof end;

Lm5: for m being Nat
for X being set
for S being Language
for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})

proof end;

Lm18: for X being set
for S being Language
for D being RuleSet of S holds union (((OneStep D) [*]) .: {X}) = union { (((mm,D) -derivables) . X) where mm is Element of NAT : verum }

proof end;

Lm18b: for m being Nat
for X being set
for S being Language
for D being RuleSet of S holds ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})

proof end;

Lm29: for m being Nat
for x, X being set
for S being Language
for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable

proof end;

Lm14: for S being Language
for D1, D2 being RuleSet of S
for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
(OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2

proof end;

Lm15: for m being Nat
for S being Language
for D1, D2 being RuleSet of S
for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2

proof end;

Lm15b: for m being Nat
for S being Language
for D1, D2 being RuleSet of S
for SQ1, SQ2 being b₂ -sequents-like set st SQ1 c= SQ2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2

proof end;

Lm17: for m being Nat
for X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . X c= ((m,D2) -derivables) . X

proof end;

Lm19: for X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
union (((OneStep D1) [*]) .: {X}) c= union (((OneStep D2) [*]) .: {X})

proof end;

Lm20: for Y, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) & Y is X,D1 -derivable holds
Y is X,D2 -derivable

proof end;

Lm9: for Y being set
for S being Language
for R being Rule of S
for Seqts being Subset of (S -sequents) st Y c= R . Seqts holds
Y is Seqts,{R} -derivable

proof end;

Lm27: for m, n being Nat
for Z being set
for S being Language
for D1, D2 being RuleSet of S
for SQ2, SQ1 being b₄ -sequents-like set st D1 is isotone & D1 \/ D2 is isotone & SQ2 c= (iter ((OneStep D1),m)) . SQ1 & Z c= (iter ((OneStep D2),n)) . SQ2 holds
Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1

proof end;

Lm28: for m, n being Nat
for y, X, z being set
for S being Language
for D1, D2 being RuleSet of S st D1 is isotone & D1 \/ D2 is isotone & y is m,X,D1 -derivable & z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable

proof end;

Lm23: for X being set
for S being Language
for t1, t2 being termal string of S
for D being RuleSet of S holds
( [t1,t2] in (X,D) -termEq iff (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable )

proof end;

Lm32: for S being Language
for Sq being b₁ -sequent-like set holds Sq `2 is wff string of S

proof end;

Lm33: for x, X being set
for S being Language
for D being RuleSet of S st x is X,D -provable holds
x is wff string of S

proof end;

Lm34: for S being Language
for D being RuleSet of S holds AllFormulasOf S is D -expanded

proof end;

registration

let S be Language;
let D be RuleSet of S;
cluster functional FinSequence-membered with_non-empty_elements D -expanded Element of bool (AllFormulasOf S);
existence
ex b₁ being Subset of (AllFormulasOf S) st b₁ is D -expanded

proof end;

end;

registration

let S be Language;
let D be RuleSet of S;
cluster D -expanded set ;
existence
ex b₁ being set st b₁ is D -expanded

proof end;

end;

definition

let Seqts be set ;
let S be Language;
let seqt be S -null set ;
pred seqt Rule0 Seqts means :Def0: :: FOMODEL4:def 18
seqt `2 in seqt `1 ;
pred seqt Rule1 Seqts means :Def1: :: FOMODEL4:def 19
ex y being set st
( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 );
pred seqt Rule2 Seqts means :Def2: :: FOMODEL4:def 20
( seqt `1 is empty & ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t );
pred seqt Rule3a Seqts means :Def3a: :: FOMODEL4:def 21
ex t, t1, t2 being termal string of S ex x being set st
( x in Seqts & seqt `1 = (x `1) \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & x `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t1 & seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2 );
pred seqt Rule3b Seqts means :Def3b: :: FOMODEL4:def 22
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 :Def3d: :: FOMODEL4:def 23
ex s being low-compounding Element of S ex T, U being abs (ar b₁) -element Element of (AllTermsOf S) * st
( s is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) );
pred seqt Rule3e Seqts means :Def3e: :: FOMODEL4:def 24
ex s being relational Element of S ex T, U being abs (ar b₁) -element Element of (AllTermsOf S) * st
( seqt `1 = {(s -compound T)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = s -compound U );
pred seqt Rule4 Seqts means :Def4: :: FOMODEL4:def 25
ex l being literal Element of S ex phi being wff string of S ex t being termal string of S st
( seqt `1 = {((l,t) SubstIn phi)} & seqt `2 = <*l*> ^ phi );
pred seqt Rule5 Seqts means :Def5: :: FOMODEL4:def 26
ex v1, v2 being literal Element of S ex x being set ex p being FinSequence st
( seqt `1 = x \/ {(<*v1*> ^ p)} & not v2 is (x \/ {p}) \/ {(seqt `2)} -occurring & [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts );
pred seqt Rule6 Seqts means :Def6: :: FOMODEL4:def 27
ex y1, y2 being set ex 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 :Def7: :: FOMODEL4:def 28
ex y being set ex 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 :Def8: :: FOMODEL4:def 29
ex y1, y2 being set ex 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 :Def9: :: FOMODEL4:def 30
ex y being set ex phi being wff string of S st
( y in Seqts & seqt `2 = phi & y `1 = seqt `1 & y `2 = xnot (xnot phi) );

end;

:: deftheorem Def0 defines Rule0 FOMODEL4:def 18 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule0 Seqts iff seqt `2 in seqt `1 );

:: deftheorem Def1 defines Rule1 FOMODEL4:def 19 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule1 Seqts iff ex y being set st
( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 ) );

:: deftheorem Def2 defines Rule2 FOMODEL4:def 20 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule2 Seqts iff ( seqt `1 is empty & ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t ) );

:: deftheorem Def3a defines Rule3a FOMODEL4:def 21 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3a Seqts iff ex t, t1, t2 being termal string of S ex x being set st
( x in Seqts & seqt `1 = (x `1) \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & x `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t1 & seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2 ) );

:: deftheorem Def3b defines Rule3b FOMODEL4:def 22 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3b Seqts iff ex t1, t2 being termal string of S st
( seqt `1 = {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & seqt `2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 ) );

:: deftheorem Def3d defines Rule3d FOMODEL4:def 23 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3d Seqts iff ex s being low-compounding Element of S ex T, U being abs (ar b₄) -element Element of (AllTermsOf S) * st
( s is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) ) );

:: deftheorem Def3e defines Rule3e FOMODEL4:def 24 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3e Seqts iff ex s being relational Element of S ex T, U being abs (ar b₄) -element Element of (AllTermsOf S) * st
( seqt `1 = {(s -compound T)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = s -compound U ) );

:: deftheorem Def4 defines Rule4 FOMODEL4:def 25 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule4 Seqts iff ex l being literal Element of S ex phi being wff string of S ex t being termal string of S st
( seqt `1 = {((l,t) SubstIn phi)} & seqt `2 = <*l*> ^ phi ) );

:: deftheorem Def5 defines Rule5 FOMODEL4:def 26 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule5 Seqts iff ex v1, v2 being literal Element of S ex x being set ex p being FinSequence st
( seqt `1 = x \/ {(<*v1*> ^ p)} & not v2 is (x \/ {p}) \/ {(seqt `2)} -occurring & [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts ) );

:: deftheorem Def6 defines Rule6 FOMODEL4:def 27 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule6 Seqts iff ex y1, y2 being set ex 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 ) );

:: deftheorem Def7 defines Rule7 FOMODEL4:def 28 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule7 Seqts iff ex y being set ex 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 ) );

:: deftheorem Def8 defines Rule8 FOMODEL4:def 29 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule8 Seqts iff ex y1, y2 being set ex 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 ) );

:: deftheorem Def9 defines Rule9 FOMODEL4:def 30 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule9 Seqts iff ex y being set ex phi being wff string of S st
( y in Seqts & seqt `2 = phi & y `1 = seqt `1 & y `2 = xnot (xnot phi) ) );

definition

let S be Language;
func P0 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP0: :: FOMODEL4:def 31
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule0 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule0 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule0 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule0 Seqts ) ) holds
b₁ = b₂

proof end;

func P1 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP1: :: FOMODEL4:def 32
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule1 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule1 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule1 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule1 Seqts ) ) holds
b₁ = b₂

proof end;

func P2 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP2: :: FOMODEL4:def 33
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule2 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule2 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule2 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule2 Seqts ) ) holds
b₁ = b₂

proof end;

func P3a S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP3a: :: FOMODEL4:def 34
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3a Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3a Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3a Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3a Seqts ) ) holds
b₁ = b₂

proof end;

func P3b S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP3b: :: FOMODEL4:def 35
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3b Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3b Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3b Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3b Seqts ) ) holds
b₁ = b₂

proof end;

func P3d S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP3d: :: FOMODEL4:def 36
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3d Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3d Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3d Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3d Seqts ) ) holds
b₁ = b₂

proof end;

func P3e S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP3e: :: FOMODEL4:def 37
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule3e Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3e Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule3e Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3e Seqts ) ) holds
b₁ = b₂

proof end;

func P4 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP4: :: FOMODEL4:def 38
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule4 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule4 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule4 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule4 Seqts ) ) holds
b₁ = b₂

proof end;

func P5 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP5: :: FOMODEL4:def 39
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule5 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule5 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule5 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule5 Seqts ) ) holds
b₁ = b₂

proof end;

func P6 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP6: :: FOMODEL4:def 40
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule6 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule6 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule6 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule6 Seqts ) ) holds
b₁ = b₂

proof end;

func P7 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP7: :: FOMODEL4:def 41
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule7 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule7 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule7 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule7 Seqts ) ) holds
b₁ = b₂

proof end;

func P8 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP8: :: FOMODEL4:def 42
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule8 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule8 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule8 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule8 Seqts ) ) holds
b₁ = b₂

proof end;

func P9 S -> Relation of (bool (S -sequents)),(S -sequents) means :DefP9: :: FOMODEL4:def 43
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in it iff seqt Rule9 Seqts );
existence
ex b₁ being Relation of (bool (S -sequents)),(S -sequents) st
for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule9 Seqts )

proof end;

uniqueness
for b₁, b₂ being Relation of (bool (S -sequents)),(S -sequents) st ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₁ iff seqt Rule9 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule9 Seqts ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefP0 defines P0 FOMODEL4:def 31 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P0 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule0 Seqts ) );

:: deftheorem DefP1 defines P1 FOMODEL4:def 32 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P1 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule1 Seqts ) );

:: deftheorem DefP2 defines P2 FOMODEL4:def 33 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P2 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule2 Seqts ) );

:: deftheorem DefP3a defines P3a FOMODEL4:def 34 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P3a S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3a Seqts ) );

:: deftheorem DefP3b defines P3b FOMODEL4:def 35 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P3b S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3b Seqts ) );

:: deftheorem DefP3d defines P3d FOMODEL4:def 36 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P3d S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3d Seqts ) );

:: deftheorem DefP3e defines P3e FOMODEL4:def 37 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P3e S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule3e Seqts ) );

:: deftheorem DefP4 defines P4 FOMODEL4:def 38 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P4 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule4 Seqts ) );

:: deftheorem DefP5 defines P5 FOMODEL4:def 39 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P5 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule5 Seqts ) );

:: deftheorem DefP6 defines P6 FOMODEL4:def 40 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P6 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule6 Seqts ) );

:: deftheorem DefP7 defines P7 FOMODEL4:def 41 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P7 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule7 Seqts ) );

:: deftheorem DefP8 defines P8 FOMODEL4:def 42 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P8 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule8 Seqts ) );

:: deftheorem DefP9 defines P9 FOMODEL4:def 43 :
for S being Language
for b₂ being Relation of (bool (S -sequents)),(S -sequents) holds
( b₂ = P9 S iff for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in b₂ iff seqt Rule9 Seqts ) );

definition

let S be Language;
let R be Relation of (bool (S -sequents)),(S -sequents);
func FuncRule R -> Rule of S means :DefFr: :: FOMODEL4:def 44
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 } ;
existence
ex b₁ being Rule of S st
for inseqs being set st inseqs in bool (S -sequents) holds
b₁ . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R }

proof end;

uniqueness
for b₁, b₂ being Rule of S st ( for inseqs being set st inseqs in bool (S -sequents) holds
b₁ . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) & ( for inseqs being set st inseqs in bool (S -sequents) holds
b₂ . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefFr defines FuncRule FOMODEL4:def 44 :
for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents)
for b₃ being Rule of S holds
( b₃ = FuncRule R iff for inseqs being set st inseqs in bool (S -sequents) holds
b₃ . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } );

Lm1: for S being Language
for Seqts being Subset of (S -sequents)
for seqt being Element of S -sequents
for R being Relation of (bool (S -sequents)),(S -sequents) st [Seqts,seqt] in R holds
seqt in (FuncRule R) . Seqts

proof end;

Lm1b: for S being Language
for SQ being b₁ -sequents-like set
for Sq being b₁ -sequent-like set
for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq is 1,SQ,{(FuncRule R)} -derivable

proof end;

Lm1d: for y being set
for S being Language
for SQ being b₂ -sequents-like set
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . SQ iff ( y in S -sequents & [SQ,y] in R ) )

proof end;

Lm1e: for y, X being set
for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) )

proof end;

definition

let S be Language;
func R0 S -> Rule of S equals :: FOMODEL4:def 45
FuncRule (P0 S);
coherence
FuncRule (P0 S) is Rule of S ;
func R1 S -> Rule of S equals :: FOMODEL4:def 46
FuncRule (P1 S);
coherence
FuncRule (P1 S) is Rule of S ;
func R2 S -> Rule of S equals :: FOMODEL4:def 47
FuncRule (P2 S);
coherence
FuncRule (P2 S) is Rule of S ;
func R3a S -> Rule of S equals :: FOMODEL4:def 48
FuncRule (P3a S);
coherence
FuncRule (P3a S) is Rule of S ;
func R3b S -> Rule of S equals :: FOMODEL4:def 49
FuncRule (P3b S);
coherence
FuncRule (P3b S) is Rule of S ;
func R3d S -> Rule of S equals :: FOMODEL4:def 50
FuncRule (P3d S);
coherence
FuncRule (P3d S) is Rule of S ;
func R3e S -> Rule of S equals :: FOMODEL4:def 51
FuncRule (P3e S);
coherence
FuncRule (P3e S) is Rule of S ;
func R4 S -> Rule of S equals :: FOMODEL4:def 52
FuncRule (P4 S);
coherence
FuncRule (P4 S) is Rule of S ;
func R5 S -> Rule of S equals :: FOMODEL4:def 53
FuncRule (P5 S);
coherence
FuncRule (P5 S) is Rule of S ;
func R6 S -> Rule of S equals :: FOMODEL4:def 54
FuncRule (P6 S);
coherence
FuncRule (P6 S) is Rule of S ;
func R7 S -> Rule of S equals :: FOMODEL4:def 55
FuncRule (P7 S);
coherence
FuncRule (P7 S) is Rule of S ;
func R8 S -> Rule of S equals :: FOMODEL4:def 56
FuncRule (P8 S);
coherence
FuncRule (P8 S) is Rule of S ;
func R9 S -> Rule of S equals :: FOMODEL4:def 57
FuncRule (P9 S);
coherence
FuncRule (P9 S) is Rule of S ;

end;

:: deftheorem defines R0 FOMODEL4:def 45 :
for S being Language holds R0 S = FuncRule (P0 S);

:: deftheorem defines R1 FOMODEL4:def 46 :
for S being Language holds R1 S = FuncRule (P1 S);

:: deftheorem defines R2 FOMODEL4:def 47 :
for S being Language holds R2 S = FuncRule (P2 S);

:: deftheorem defines R3a FOMODEL4:def 48 :
for S being Language holds R3a S = FuncRule (P3a S);

:: deftheorem defines R3b FOMODEL4:def 49 :
for S being Language holds R3b S = FuncRule (P3b S);

:: deftheorem defines R3d FOMODEL4:def 50 :
for S being Language holds R3d S = FuncRule (P3d S);

:: deftheorem defines R3e FOMODEL4:def 51 :
for S being Language holds R3e S = FuncRule (P3e S);

:: deftheorem defines R4 FOMODEL4:def 52 :
for S being Language holds R4 S = FuncRule (P4 S);

:: deftheorem defines R5 FOMODEL4:def 53 :
for S being Language holds R5 S = FuncRule (P5 S);

:: deftheorem defines R6 FOMODEL4:def 54 :
for S being Language holds R6 S = FuncRule (P6 S);

:: deftheorem defines R7 FOMODEL4:def 55 :
for S being Language holds R7 S = FuncRule (P7 S);

:: deftheorem defines R8 FOMODEL4:def 56 :
for S being Language holds R8 S = FuncRule (P8 S);

:: deftheorem defines R9 FOMODEL4:def 57 :
for S being Language holds R9 S = FuncRule (P9 S);

registration

let S be Language;
let t be termal string of S;
cluster {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} -> {(R2 S)} -derivable set ;
coherence
for b₁ being set st b₁ = {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} holds
b₁ is {(R2 S)} -derivable

proof end;

end;

registration

let S be Language;
cluster R2 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R2 S holds
b₁ is isotone

proof end;

end;

Lm24: for X being set
for S being Language
for D being RuleSet of S st {(R2 S)} c= D holds
(X,D) -termEq is total

proof end;

registration

let S be Language;
cluster R3b S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3b S holds
b₁ is isotone

proof end;

end;

Lm25: for X being set
for S being Language
for D being RuleSet of S st {(R3b S)} c= D & X is D -expanded holds
(X,D) -termEq is symmetric

proof end;

registration

let S be Language;
let t, t1, t2 be termal string of S;
let premises be finite Subset of (AllFormulasOf S);
cluster [(premises \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)}),((<*(TheEqSymbOf S)*> ^ t) ^ t2)] -> 1,{[premises,((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R3a S)} -derivable set ;
coherence
for b₁ being set st b₁ = [(premises \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)}),((<*(TheEqSymbOf S)*> ^ t) ^ t2)] holds
b₁ is 1,{[premises,((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R3a S)} -derivable

proof end;

end;

registration

let S be Language;
let t, t1, t2 be termal string of S;
let phi be wff string of S;
cluster [{phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t2)},((<*(TheEqSymbOf S)*> ^ t) ^ t2)] -> 1,{[{phi},((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R3a S)} -derivable set ;
coherence
for b₁ being set st b₁ = [{phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t2)},((<*(TheEqSymbOf S)*> ^ t) ^ t2)] holds
b₁ is 1,{[{phi},((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R3a S)} -derivable

proof end;

end;

registration

let S be Language;
let phi be wff string of S;
let Phi be finite Subset of (AllFormulasOf S);
cluster [(Phi \/ {phi}),phi] -> 1, {} ,{(R0 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [(Phi \/ {phi}),phi] holds
b₁ is 1, {} ,{(R0 S)} -derivable

proof end;

end;

registration

let S be Language;
let phi1, phi2 be wff string of S;
cluster [{phi1,phi2},phi1] -> 1, {} ,{(R0 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [{phi1,phi2},phi1] holds
b₁ is 1, {} ,{(R0 S)} -derivable

proof end;

end;

registration

let S be Language;
let phi be wff string of S;
cluster [{phi},phi] -> 1, {} ,{(R0 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [{phi},phi] holds
b₁ is 1, {} ,{(R0 S)} -derivable

proof end;

end;

registration

let S be Language;
let phi be wff string of S;
cluster {[{phi},phi]} -> {} ,{(R0 S)} -derivable set ;
coherence
for b₁ being set st b₁ = {[{phi},phi]} holds
b₁ is {} ,{(R0 S)} -derivable by Lm29;

end;

registration

let S be Language;
cluster R0 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R0 S holds
b₁ is isotone

proof end;

cluster R3a S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3a S holds
b₁ is isotone

proof end;

cluster R3d S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3d S holds
b₁ is isotone

proof end;

cluster R3e S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3e S holds
b₁ is isotone

proof end;

let K1, K2 be isotone RuleSet of S;
cluster K1 \/ K2 -> isotone RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = K1 \/ K2 holds
b₁ is isotone

proof end;

end;

Lm26: for X being set
for S being Language
for D being RuleSet of S st {(R0 S)} \/ {(R3a S)} c= D & X is D -expanded holds
(X,D) -termEq is transitive

proof end;

Lm11: for X being set
for S being Language
for D being RuleSet of S st {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded holds
(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)

proof end;

registration

let S be Language;
let t1, t2 be termal string of S;
cluster (<*(TheEqSymbOf S)*> ^ t1) ^ t2 -> 0 -wff string of S;
coherence
for b₁ being string of S st b₁ = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 holds
b₁ is 0 -wff by Lm10;

end;

definition

let S be Language;
let m be non zero Nat;
let T, U be m -element Element of (AllTermsOf S) * ;
func PairWiseEq (T,U) -> set equals :: FOMODEL4:def 58
{ ((<*(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 ) } ;
coherence
{ ((<*(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 ) } is set ;

end;

:: deftheorem defines PairWiseEq FOMODEL4:def 58 :
for S being Language
for m being non zero Nat
for T, U being b₂ -element Element of (AllTermsOf S) * holds PairWiseEq (T,U) = { ((<*(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 ) } ;

definition

let S be Language;
let m be non zero Nat;
let T1, T2 be m -element Element of (AllTermsOf S) * ;
:: original: PairWiseEq
redefine func PairWiseEq (T1,T2) -> Subset of (AllFormulasOf S);
coherence
PairWiseEq (T1,T2) is Subset of (AllFormulasOf S)

proof end;

end;

registration

let S be Language;
let m be non zero Nat;
let T, U be m -element Element of (AllTermsOf S) * ;
cluster PairWiseEq (T,U) -> finite ;
coherence
PairWiseEq (T,U) is finite

proof end;

end;

Lm41: for S being Language
for s being low-compounding Element of S
for T, U being abs (ar b₂) -element Element of (AllTermsOf S) * st s is termal holds
{[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R3d S)} -derivable

proof end;

Lm44: for S being Language
for s being relational Element of S
for T1, T2 being abs (ar b₂) -element Element of (AllTermsOf S) * holds {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R3e S)} -derivable

proof end;

registration

let S be Language;
let s be relational Element of S;
let T1, T2 be abs (ar s) -element Element of (AllTermsOf S) * ;
cluster {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} -> {} ,{(R3e S)} -derivable ;
coherence
{[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R3e S)} -derivable by Lm44;

end;

Lm42: for X, x1, x2 being set
for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st X is D -expanded & [x1,x2] in (abs (ar s)) -placesOf ((X,D) -termEq) holds
ex T, U being abs (ar b₆) -element Element of (AllTermsOf S) * st
( T = x1 & U = x2 & PairWiseEq (T,U) c= X )

proof end;

Lm48: for X being set
for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st {(R3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting

proof end;

Lm45: for X, x1, x2 being set
for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R3e S)} c= D & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) & (r -compound) . x1 in X holds
(r -compound) . x2 in X

proof end;

Lm46: for X, x1, x2 being set
for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded & [x1,x2] in (abs (ar r)) -placesOf ((X,D) -termEq) holds
( (r -compound) . x1 in X iff (r -compound) . x2 in X )

proof end;

Lm47: for U being non empty set
for Y being set
for x, y being Element of U holds
not ( ( x in Y implies y in Y ) & ( y in Y implies x in Y ) & not [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN )

proof end;

Lm51: for X being set
for S being Language
for r being relational Element of S
for D being RuleSet of S st {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded holds
X -freeInterpreter r is (X,D) -termEq -respecting

proof end;

Lm49: for U being non empty set
for X, x being set
for R being total reflexive Relation of U
for f being Function of X,U st x in X holds
f is {[x,x]},R -respecting

proof end;

Lm50: for U being non empty set
for S being Language
for l being literal Element of S
for E being total reflexive Relation of U
for f being Interpreter of l,U holds f is E -respecting

proof end;

Lm52: for X being set
for S being Language
for l being literal Element of S
for D being RuleSet of S st {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting

proof end;

Lm53: for X being set
for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st {(R0 S),(R3a S)} c= D & D /\ {(R3d S)} = {(R3d S)} & {(R2 S)} /\ D = {(R2 S)} & {(R3b S)} /\ D = {(R3b S)} & D /\ {(R3e S)} = {(R3e S)} & X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting

proof end;

definition

let m be Nat;
let S be Language;
let D be RuleSet of S;
attr D is m -ranked means :DefRank: :: FOMODEL4:def 59
( R0 S in D & R2 S in D & R3a S in D & R3b S in D ) if m = 0
( R0 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D ) if m = 1
( R0 S in D & R1 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D & R4 S in D & R5 S in D & R6 S in D & R7 S in D & R8 S in D ) if m = 2
otherwise D = {} ;
consistency
( ( m = 0 & m = 1 implies ( R0 S in D & R2 S in D & R3a S in D & R3b S in D iff ( R0 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D ) ) ) & ( m = 0 & m = 2 implies ( R0 S in D & R2 S in D & R3a S in D & R3b S in D iff ( R0 S in D & R1 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D & R4 S in D & R5 S in D & R6 S in D & R7 S in D & R8 S in D ) ) ) & ( m = 1 & m = 2 implies ( R0 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D iff ( R0 S in D & R1 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D & R4 S in D & R5 S in D & R6 S in D & R7 S in D & R8 S in D ) ) ) ) ;

end;

:: deftheorem DefRank defines -ranked FOMODEL4:def 59 :
for m being Nat
for S being Language
for D being RuleSet of S holds
( ( m = 0 implies ( D is m -ranked iff ( R0 S in D & R2 S in D & R3a S in D & R3b S in D ) ) ) & ( m = 1 implies ( D is m -ranked iff ( R0 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D ) ) ) & ( m = 2 implies ( D is m -ranked iff ( R0 S in D & R1 S in D & R2 S in D & R3a S in D & R3b S in D & R3d S in D & R3e S in D & R4 S in D & R5 S in D & R6 S in D & R7 S in D & R8 S in D ) ) ) & ( not m = 0 & not m = 1 & not m = 2 implies ( D is m -ranked iff D = {} ) ) );

registration

let S be Language;
cluster 1 -ranked -> 0 -ranked Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
coherence
for b₁ being RuleSet of S st b₁ is 1 -ranked holds
b₁ is 0 -ranked

proof end;

cluster 2 -ranked -> 1 -ranked Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
coherence
for b₁ being RuleSet of S st b₁ is 2 -ranked holds
b₁ is 1 -ranked

proof end;

end;

definition

let S be Language;
func S -rules -> RuleSet of S equals :: FOMODEL4:def 60
{(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)};
coherence
{(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)} is RuleSet of S ;

end;

:: deftheorem defines -rules FOMODEL4:def 60 :
for S being Language holds S -rules = {(R0 S),(R1 S),(R2 S),(R3a S),(R3b S),(R3d S),(R3e S),(R4 S)} \/ {(R5 S),(R6 S),(R7 S),(R8 S)};

registration

let S be Language;
cluster S -rules -> 2 -ranked RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is 2 -ranked

proof end;

end;

registration

let S be Language;
cluster functional 2 -ranked Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
ex b₁ being RuleSet of S st b₁ is 2 -ranked

proof end;

end;

registration

let S be Language;
cluster functional 1 -ranked Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
ex b₁ being RuleSet of S st b₁ is 1 -ranked

proof end;

end;

registration

let S be Language;
cluster functional 0 -ranked Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
ex b₁ being RuleSet of S st b₁ is 0 -ranked

proof end;

end;

Lm53a: for X being set
for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st D is 1 -ranked & X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting

proof end;

registration

let S be Language;
let D be 1 -ranked RuleSet of S;
let X be D -expanded set ;
let a be ofAtomicFormula Element of S;
cluster X -freeInterpreter a -> (X,D) -termEq -respecting Interpreter of a, AllTermsOf S;
coherence
for b₁ being Interpreter of a, AllTermsOf S st b₁ = X -freeInterpreter a holds
b₁ is (X,D) -termEq -respecting by Lm53a;

end;

Lm11a: for X being set
for S being Language
for D being RuleSet of S st D is 0 -ranked & X is D -expanded holds
(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)

proof end;

registration

let S be Language;
let D be 0 -ranked RuleSet of S;
let X be D -expanded set ;
cluster (X,D) -termEq -> total symmetric transitive Relation of (AllTermsOf S);
coherence
for b₁ being Relation of (AllTermsOf S) st b₁ = (X,D) -termEq holds
( b₁ is total & b₁ is symmetric & b₁ is transitive ) by Lm11a;

end;

registration

let S be Language;
cluster functional 0 -ranked 1 -ranked Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
ex b₁ being 0 -ranked RuleSet of S st b₁ is 1 -ranked

proof end;

end;

theorem :: FOMODEL4:1

for Y, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) & Y is X,D1 -derivable holds
Y is X,D2 -derivable by Lm20;

registration

let S be Language;
let Sq be S -sequent-like set ;
cluster {Sq} -> S -sequents-like ;
coherence
{Sq} is S -sequents-like

proof end;

end;

registration

let S be Language;
let SQ1, SQ2 be S -sequents-like set ;
cluster SQ1 \/ SQ2 -> S -sequents-like set ;
coherence
for b₁ being set st b₁ = SQ1 \/ SQ2 holds
b₁ is S -sequents-like

proof end;

end;

registration

let S be Language;
let x, y be S -sequent-like set ;
cluster {x,y} -> S -sequents-like set ;
coherence
for b₁ being set st b₁ = {x,y} holds
b₁ is S -sequents-like

proof end;

end;

Lm40: for m, n being Nat
for x, y, z being set
for S being Language
for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being b₆ -sequents-like set st 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 holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable

proof end;

Lm35: for x, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D1 is isotone or D2 is isotone ) & x is X,D1 -provable holds
x is X,D2 -provable

proof end;

Lm22: for x, X being set
for S being Language
for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable

proof end;

registration

let S be Language;
let phi1, phi2 be wff string of S;
cluster [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] -> 1,{[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]},{(R6 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] holds
b₁ is 1,{[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]},{(R6 S)} -derivable

proof end;

end;

registration

let S be Language;
let phi1, phi2 be wff string of S;
cluster [{phi1,phi2},phi2] -> 1, {} ,{(R0 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [{phi1,phi2},phi2] holds
b₁ is 1, {} ,{(R0 S)} -derivable

proof end;

end;

theorem Th3: :: FOMODEL4:2

for S being Language
for SQ being b₁ -sequents-like set
for Sq being b₁ -sequent-like set
for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds
Sq in (FuncRule R) . SQ

proof end;

theorem :: FOMODEL4:3

for x, X being set
for S being Language
for R being Rule of S st x in R . X holds
x is 1,X,{R} -derivable by Lm22;

definition

let S be Language;
let D be RuleSet of S;
let X be set ;
redefine attr X is D -expanded means :DefExpanded2: :: FOMODEL4:def 61
for x being set st x is X,D -provable holds
x in X;
compatibility
( X is D -expanded iff for x being set st x is X,D -provable holds
x in X )

proof end;

end;

:: deftheorem DefExpanded2 defines -expanded FOMODEL4:def 61 :
for S being Language
for D being RuleSet of S
for X being set holds
( X is D -expanded iff for x being set st x is X,D -provable holds
x in X );

theorem Lm2: :: FOMODEL4:4

for X being set
for S being Language
for phi being wff string of S st phi in X holds
phi is X,{(R0 S)} -provable

proof end;

theorem :: FOMODEL4:5

for m, n being Nat
for x, y, z being set
for S being Language
for D1, D2, D3 being RuleSet of S
for SQ1, SQ2 being b₆ -sequents-like set st 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 holds
z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable by Lm40;

theorem :: FOMODEL4:6

for m, n being Nat
for y, X, z being set
for S being Language
for D1, D2 being RuleSet of S st D1 is isotone & D1 \/ D2 is isotone & y is m,X,D1 -derivable & z is n,{y},D2 -derivable holds
z is m + n,X,D1 \/ D2 -derivable by Lm28;

theorem :: FOMODEL4:7

for m being Nat
for x, X being set
for S being Language
for D being RuleSet of S st x is m,X,D -derivable holds
{x} is X,D -derivable by Lm29;

registration

let S be Language;
cluster R6 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R6 S holds
b₁ is isotone

proof end;

end;

theorem :: FOMODEL4:8

for x, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D1 is isotone or D2 is isotone ) & x is X,D1 -provable holds
x is X,D2 -provable by Lm35;

theorem :: FOMODEL4:9

for X, Y, x being set
for S being Language
for D being RuleSet of S st X c= Y & x is X,D -provable holds
x is Y,D -provable ;

registration

let S be Language;
cluster R8 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R8 S holds
b₁ is isotone

proof end;

end;

registration

let S be Language;
cluster R1 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R1 S holds
b₁ is isotone

proof end;

end;

theorem :: FOMODEL4:10

for y being set
for S being Language
for D being RuleSet of S
for SQ being b₂ -sequents-like set st {y} is SQ,D -derivable holds
ex mm being Element of NAT st y is mm,SQ,D -derivable

proof end;

registration

let S be Language;
let D be RuleSet of S;
let X be set ;
cluster X,D -derivable -> S -sequents-like set ;
coherence
for b₁ being set st b₁ is X,D -derivable holds
b₁ is S -sequents-like

proof end;

end;

definition

let S be Language;
let D be RuleSet of S;
let X, x be set ;
redefine attr x is X,D -provable means :DefProvable3: :: FOMODEL4:def 62
ex H being set ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable );
compatibility
( x is X,D -provable iff ex H being set ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable ) )

proof end;

end;

:: deftheorem DefProvable3 defines -provable FOMODEL4:def 62 :
for S being Language
for D being RuleSet of S
for X, x being set holds
( x is X,D -provable iff ex H being set ex m being Nat st
( H c= X & [H,x] is m, {} ,D -derivable ) );

theorem Th12: :: FOMODEL4:11

for m being Nat
for x, X being set
for S being Language
for D1, D2 being RuleSet of S st D1 c= D2 & ( D2 is isotone or D1 is isotone ) & x is m,X,D1 -derivable holds
x is m,X,D2 -derivable

proof end;

registration

let S be Language;
cluster R7 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R7 S holds
b₁ is isotone

proof end;

end;

theorem :: FOMODEL4:12

for x, X being set
for S being Language
for D being RuleSet of S st x is X,D -provable holds
x is wff string of S by Lm33;

registration

let S be Language;
let D1 be 0 -ranked 1 -ranked RuleSet of S;
let X be D1 -expanded set ;
cluster (S,X) -freeInterpreter -> S, AllTermsOf S -interpreter-like (X,D1) -termEq -respecting S, AllTermsOf S -interpreter-like Function;
coherence
for b₁ being S, AllTermsOf S -interpreter-like Function st b₁ = (S,X) -freeInterpreter holds
b₁ is (X,D1) -termEq -respecting

proof end;

end;

definition

let S be Language;
let D be 0 -ranked RuleSet of S;
let X be D -expanded set ;
func D Henkin X -> Function equals :: FOMODEL4:def 63
((S,X) -freeInterpreter) quotient ((X,D) -termEq);
coherence
((S,X) -freeInterpreter) quotient ((X,D) -termEq) is Function ;

end;

:: deftheorem defines Henkin FOMODEL4:def 63 :
for S being Language
for D being 0 -ranked RuleSet of S
for X being b₂ -expanded set holds D Henkin X = ((S,X) -freeInterpreter) quotient ((X,D) -termEq);

registration

let S be Language;
let D be 0 -ranked RuleSet of S;
let X be D -expanded set ;
cluster D Henkin X -> OwnSymbolsOf S -defined ;
coherence
D Henkin X is OwnSymbolsOf S -defined ;

end;

registration

let S be Language;
let D1 be 0 -ranked 1 -ranked RuleSet of S;
let X be D1 -expanded set ;
cluster D1 Henkin X -> S, Class ((X,D1) -termEq) -interpreter-like Function;
coherence
for b₁ being Function st b₁ = D1 Henkin X holds
b₁ is S, Class ((X,D1) -termEq) -interpreter-like ;

end;

definition

let S be Language;
let D1 be 0 -ranked 1 -ranked RuleSet of S;
let X be D1 -expanded set ;
:: original: Henkin
redefine func D1 Henkin X -> Element of (Class ((X,D1) -termEq)) -InterpretersOf S;
coherence
D1 Henkin X is Element of (Class ((X,D1) -termEq)) -InterpretersOf S

proof end;

end;

registration

let S be Language;
let phi1, phi2 be wff string of S;
cluster (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 -> {(xnot phi1),(xnot phi2)},{(R0 S)} \/ {(R6 S)} -provable set ;
coherence
for b₁ being set st b₁ = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b₁ is {(xnot phi1),(xnot phi2)},{(R0 S)} \/ {(R6 S)} -provable

proof end;

end;

registration

let S be Language;
cluster 0 -ranked -> non empty 0 -ranked Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
coherence
for b₁ being 0 -ranked RuleSet of S holds not b₁ is empty by DefRank;

end;

definition

let S be Language;
let x be set ;
attr x is S -premises-like means :DefPremLike: :: FOMODEL4:def 64
( x c= AllFormulasOf S & x is finite );

end;

:: deftheorem DefPremLike defines -premises-like FOMODEL4:def 64 :
for S being Language
for x being set holds
( x is S -premises-like iff ( x c= AllFormulasOf S & x is finite ) );

registration

let S be Language;
cluster S -premises-like -> finite set ;
coherence
for b₁ being set st b₁ is S -premises-like holds
b₁ is finite by DefPremLike;

end;

registration

let S be Language;
let phi be wff string of S;
cluster {phi} -> S -premises-like set ;
coherence
for b₁ being set st b₁ = {phi} holds
b₁ is S -premises-like

proof end;

end;

registration

let S be Language;
let e be empty set ;
cluster e null S -> S -premises-like set ;
coherence
for b₁ being set st b₁ = e null S holds
b₁ is S -premises-like

proof end;

end;

registration

let X be set ;
let S be Language;
cluster S -premises-like Element of bool X;
existence
ex b₁ being Subset of X st b₁ is S -premises-like

proof end;

end;

registration

let S be Language;
cluster S -premises-like set ;
existence
ex b₁ being set st b₁ is S -premises-like

proof end;

end;

registration

let S be Language;
let X be S -premises-like set ;
cluster -> S -premises-like Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is S -premises-like

proof end;

end;

definition

let S be Language;
let H2, H1 be S -premises-like set ;
:: original: null
redefine func H1 null H2 -> Subset of (AllFormulasOf S);
coherence
H1 null H2 is Subset of (AllFormulasOf S) by DefPremLike;

end;

registration

let S be Language;
let H be S -premises-like set ;
let x be set ;
cluster H null x -> S -premises-like ;
coherence
H null x is S -premises-like ;

end;

registration

let S be Language;
let H1, H2 be S -premises-like set ;
cluster H1 \/ H2 -> S -premises-like set ;
coherence
for b₁ being set st b₁ = H1 \/ H2 holds
b₁ is S -premises-like

proof end;

end;

registration

let S be Language;
let H be S -premises-like set ;
let phi be wff string of S;
cluster [H,phi] -> S -sequent-like ;
coherence
[H,phi] is S -sequent-like

proof end;

end;

registration

let S be Language;
let H1, H2 be S -premises-like set ;
let phi be wff string of S;
cluster [(H1 \/ H2),phi] -> 1,{[H1,phi]},{(R1 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [(H1 \/ H2),phi] holds
b₁ is 1,{[H1,phi]},{(R1 S)} -derivable

proof end;

end;

registration

let S be Language;
let H be S -premises-like set ;
let phi, phi1, phi2 be wff string of S;
cluster [(H null (phi1 ^ phi2)),(xnot phi)] -> 1,{[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R8 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [(H null (phi1 ^ phi2)),(xnot phi)] holds
b₁ is 1,{[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R8 S)} -derivable

proof end;

end;

registration

let S be Language;
cluster {} null S -> S -sequents-like set ;
coherence
for b₁ being set st b₁ = {} null S holds
b₁ is S -sequents-like

proof end;

end;

registration

let S be Language;
let H be S -premises-like set ;
let phi be wff string of S;
cluster [(H \/ {phi}),phi] -> 1, {} ,{(R0 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [(H \/ {phi}),phi] holds
b₁ is 1, {} ,{(R0 S)} -derivable

proof end;

end;

registration

let S be Language;
let H be S -premises-like set ;
let phi1, phi2 be wff string of S;
cluster [(H null phi2),(xnot phi1)] -> 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R0 S)} \/ {(R1 S)}) \/ {(R8 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [(H null phi2),(xnot phi1)] holds
b₁ is 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R0 S)} \/ {(R1 S)}) \/ {(R8 S)} -derivable

proof end;

end;

registration

let S be Language;
let H be S -premises-like set ;
let phi1, phi2 be wff string of S;
cluster [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] -> 1,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R7 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] holds
b₁ is 1,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R7 S)} -derivable

proof end;

end;

registration

let S be Language;
let H be S -premises-like set ;
let phi1, phi2 be wff string of S;
cluster [(H null phi1),(xnot phi2)] -> 3,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},(({(R0 S)} \/ {(R1 S)}) \/ {(R8 S)}) \/ {(R7 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [(H null phi1),(xnot phi2)] holds
b₁ is 3,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},(({(R0 S)} \/ {(R1 S)}) \/ {(R8 S)}) \/ {(R7 S)} -derivable

proof end;

end;

registration

let S be Language;
let Sq be S -sequent-like set ;
cluster Sq `1 -> S -premises-like set ;
coherence
for b<sub>1</sub> being set st b<sub>1</sub> = Sq `1 holds
b₁ is S -premises-like

proof end;

end;

definition

let S be Language;
let X be set ;
let D be RuleSet of S;
:: original: null
redefine func D null X -> RuleSet of S;
coherence
D null X is RuleSet of S ;

end;

registration

let S be Language;
let phi1, phi2 be wff string of S;
let l1 be literal Element of S;
let H be S -premises-like set ;
let l2 be literal (H \/ {phi1}) \/ {phi2} -absent Element of S;
cluster [((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] -> 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R5 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] holds
b₁ is 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R5 S)} -derivable

proof end;

end;

definition

let S be Language;
let D be RuleSet of S;
let X be set ;
attr X is D -inconsistent means :DefInc: :: FOMODEL4:def 65
ex phi1, phi2 being wff string of S st
( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable );

end;

:: deftheorem DefInc defines -inconsistent FOMODEL4:def 65 :
for S being Language
for D being RuleSet of S
for X being set holds
( X is D -inconsistent iff ex phi1, phi2 being wff string of S st
( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable ) );

registration

let m1 be non zero Nat;
let S be Language;
let H1, H2 be S -premises-like set ;
let phi be wff string of S;
cluster [((H1 \/ H2) null m1),phi] -> m1,{[H1,phi]},{(R1 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [((H1 \/ H2) null m1),phi] holds
b₁ is m1,{[H1,phi]},{(R1 S)} -derivable

proof end;

end;

registration

let S be Language;
cluster non empty functional isotone Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
not for b₁ being isotone RuleSet of S holds b₁ is empty

proof end;

end;

theorem Th14: :: FOMODEL4:13

for X being set
for S being Language
for phi being wff string of S
for D being RuleSet of S st X is D -inconsistent & D is isotone & R1 S in D & R8 S in D holds
xnot phi is X,D -provable

proof end;

registration

let S be Language;
cluster R5 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R5 S holds
b₁ is isotone

proof end;

end;

registration

let S be Language;
let l be literal Element of S;
let t be termal string of S;
let phi be wff string of S;
cluster [{((l,t) SubstIn phi)},(<*l*> ^ phi)] -> 1, {} ,{(R4 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] holds
b₁ is 1, {} ,{(R4 S)} -derivable

proof end;

end;

registration

let S be Language;
cluster R4 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R4 S holds
b₁ is isotone

proof end;

end;

Lm12: for S being Language
for D1 being 0 -ranked 1 -ranked RuleSet of S
for X being b₂ -expanded set
for phi being 0wff string of S holds
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )

proof end;

definition

let S be Language;
let X be set ;
attr X is S -witnessed means :DefWit1: :: FOMODEL4:def 66
for l1 being literal Element of S
for phi1 being wff string of S st <*l1*> ^ phi1 in X holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in X & not l2 in rng phi1 );

end;

:: deftheorem DefWit1 defines -witnessed FOMODEL4:def 66 :
for S being Language
for X being set holds
( X is S -witnessed iff for l1 being literal Element of S
for phi1 being wff string of S st <*l1*> ^ phi1 in X holds
ex l2 being literal Element of S st
( (l1,l2) -SymbolSubstIn phi1 in X & not l2 in rng phi1 ) );

theorem Th15: :: FOMODEL4:14

for S being Language
for psi being wff string of S
for D1 being 0 -ranked 1 -ranked RuleSet of S
for X being b₃ -expanded set st R1 S in D1 & R4 S in D1 & R6 S in D1 & R7 S in D1 & R8 S in D1 & X is S -mincover & X is S -witnessed holds
( (D1 Henkin X) -TruthEval psi = 1 iff psi in X )

proof end;

notation

let S be Language;
let D be RuleSet of S;
let X be set ;
antonym D -consistent X for D -inconsistent ;

end;

theorem Th16: :: FOMODEL4:15

for Y being set
for S being Language
for D being RuleSet of S
for X being Subset of Y st X is D -inconsistent holds
Y is D -inconsistent

proof end;

definition

let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
func (D,phi) AddAsWitnessTo X -> set equals :DefWit2: :: FOMODEL4:def 67
X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} if ( not X \/ {phi} is D -inconsistent & (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} )
otherwise X;
consistency
for b₁ being set holds verum ;
coherence
( ( not X \/ {phi} is D -inconsistent & (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} implies X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} is set ) & ( ( X \/ {phi} is D -inconsistent or not (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} ) implies X is set ) ) ;

end;

:: deftheorem DefWit2 defines AddAsWitnessTo FOMODEL4:def 67 :
for S being Language
for D being RuleSet of S
for X being functional set
for phi being Element of ExFormulasOf S holds
( ( not X \/ {phi} is D -inconsistent & (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} implies (D,phi) AddAsWitnessTo X = X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} ) & ( ( X \/ {phi} is D -inconsistent or not (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} ) implies (D,phi) AddAsWitnessTo X = X ) );

registration

let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
cluster X \ ((D,phi) AddAsWitnessTo X) -> empty set ;
coherence
for b₁ being set st b₁ = X \ ((D,phi) AddAsWitnessTo X) holds
b₁ is empty

proof end;

end;

registration

let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
cluster ((D,phi) AddAsWitnessTo X) \ X -> trivial set ;
coherence
for b₁ being set st b₁ = ((D,phi) AddAsWitnessTo X) \ X holds
b₁ is trivial

proof end;

end;

definition

let S be Language;
let D be RuleSet of S;
let X be functional set ;
let phi be Element of ExFormulasOf S;
:: original: AddAsWitnessTo
redefine func (D,phi) AddAsWitnessTo X -> Subset of (X \/ (AllFormulasOf S));
coherence
(D,phi) AddAsWitnessTo X is Subset of (X \/ (AllFormulasOf S))

proof end;

end;

definition

let S be Language;
let D be RuleSet of S;
attr D is Correct means :DefCorrect: :: FOMODEL4:def 68
for phi being wff string of S
for X being set st phi is X,D -provable holds
for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1;

end;

:: deftheorem DefCorrect defines Correct FOMODEL4:def 68 :
for S being Language
for D being RuleSet of S holds
( D is Correct iff for phi being wff string of S
for X being set st phi is X,D -provable holds
for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1 );

Lm2b: for X being set
for S being Language
for phi being wff string of S
for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & X \/ {phi} is D -inconsistent holds
xnot phi is X,D -provable

proof end;

Lm1: for X being set
for S being Language
for D being RuleSet of S holds
( not X is D -inconsistent iff for Y being finite Subset of X holds not Y is D -inconsistent )

proof end;

Lm8: for X being set
for S being Language
for D being RuleSet of S st R0 S in D & X is S -covering & not X is D -inconsistent holds
( X is S -mincover & X is D -expanded )

proof end;

Lm3: for X being set
for S being Language
for phi being wff string of S
for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & phi is X,D -provable & not X is D -inconsistent holds
not X \/ {phi} is D -inconsistent

proof end;

Lm11: for U being non empty set
for X being set
for S being Language
for D being RuleSet of S
for I being Element of U -InterpretersOf S st D is Correct & X is I -satisfied holds
not X is D -inconsistent

proof end;

registration

let S be Language;
let t1, t2 be termal string of S;
cluster (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> -> empty set ;
coherence
for b₁ being set st b₁ = (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> holds
b₁ is empty

proof end;

end;

Lm36: for U being non empty set
for S being Language
for t1, t2 being termal string of S
for I being b₂,b₁ -interpreter-like Function holds
( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 iff (I -TermEval) . t1 = (I -TermEval) . t2 )

proof end;

definition

let S be Language;
let R be Rule of S;
attr R is Correct means :RuleCorr: :: FOMODEL4:def 69
for X being set st X is S -correct holds
R . X is S -correct ;

end;

:: deftheorem RuleCorr defines Correct FOMODEL4:def 69 :
for S being Language
for R being Rule of S holds
( R is Correct iff for X being set st X is S -correct holds
R . X is S -correct );

registration

let S be Language;
cluster S -sequent-like -> S -null set ;
coherence
for b₁ being set st b₁ is S -sequent-like holds
b₁ is S -null ;

end;

Lm60: for S being Language holds R0 S is Correct

proof end;

registration

let S be Language;
cluster R0 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R0 S holds
b₁ is Correct by Lm60;

end;

registration

let S be Language;
cluster Relation-like bool (S -sequents) -defined bool (S -sequents) -valued Function-like total quasi_total Correct Element of Funcs ((bool (S -sequents)),(bool (S -sequents)));
existence
ex b₁ being Rule of S st b₁ is Correct

proof end;

end;

Lm61: for S being Language holds R1 S is Correct

proof end;

registration

let S be Language;
cluster R1 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R1 S holds
b₁ is Correct by Lm61;

end;

Lm62: for S being Language holds R2 S is Correct

proof end;

registration

let S be Language;
cluster R2 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R2 S holds
b₁ is Correct by Lm62;

end;

Lm63a: for S being Language holds R3a S is Correct

proof end;

registration

let S be Language;
cluster R3a S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3a S holds
b₁ is Correct by Lm63a;

end;

Lm63b: for S being Language holds R3b S is Correct

proof end;

registration

let S be Language;
cluster R3b S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3b S holds
b₁ is Correct by Lm63b;

end;

Lm63d: for S being Language holds R3d S is Correct

proof end;

registration

let S be Language;
cluster R3d S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3d S holds
b₁ is Correct by Lm63d;

end;

Lm63e: for S being Language holds R3e S is Correct

proof end;

registration

let S be Language;
cluster R3e S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R3e S holds
b₁ is Correct by Lm63e;

end;

Lm64: for S being Language holds R4 S is Correct

proof end;

registration

let S be Language;
cluster R4 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R4 S holds
b₁ is Correct by Lm64;

end;

Lm65: for S being Language holds R5 S is Correct

proof end;

registration

let S be Language;
cluster R5 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R5 S holds
b₁ is Correct by Lm65;

end;

Lm66: for S being Language holds R6 S is Correct

proof end;

registration

let S be Language;
cluster R6 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R6 S holds
b₁ is Correct by Lm66;

end;

Lm67: for S being Language holds R7 S is Correct

proof end;

registration

let S be Language;
cluster R7 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R7 S holds
b₁ is Correct by Lm67;

end;

Lm68: for S being Language holds R8 S is Correct

proof end;

registration

let S be Language;
cluster R8 S -> Correct Rule of S;
coherence
for b₁ being Rule of S st b₁ = R8 S holds
b₁ is Correct by Lm68;

end;

theorem Th17: :: FOMODEL4:16

for S being Language
for D being RuleSet of S st ( for R being Rule of S st R in D holds
R is Correct ) holds
D is Correct

proof end;

registration

let S be Language;
let R be Correct Rule of S;
cluster {R} -> Correct RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = {R} holds
b₁ is Correct

proof end;

end;

registration

let S be Language;
cluster S -rules -> Correct RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is Correct

proof end;

end;

registration

let S be Language;
cluster R9 S -> isotone Rule of S;
coherence
for b₁ being Rule of S st b₁ = R9 S holds
b₁ is isotone

proof end;

end;

registration

let S be Language;
let H be S -premises-like set ;
let phi be wff string of S;
cluster [H,phi] null 1 -> 1,{[H,(xnot (xnot phi))]},{(R9 S)} -derivable set ;
coherence
for b₁ being set st b₁ = [H,phi] null 1 holds
b₁ is 1,{[H,(xnot (xnot phi))]},{(R9 S)} -derivable

proof end;

end;

registration

let X be set ;
let S be Language;
cluster non empty Relation-like AtomicFormulaSymbolsOf S -valued Function-like finite FinSequence-like FinSubsequence-like countable V202() 0wff 0 -wff wff X -implied Element of ((AllSymbolsOf S) *) \ {{}};
existence
ex b₁ being 0 -wff string of S st b₁ is X -implied

proof end;

end;

registration

let X be set ;
let S be Language;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like countable V202() wff X -implied Element of ((AllSymbolsOf S) *) \ {{}};
existence
ex b₁ being wff string of S st b₁ is X -implied

proof end;

end;

registration

let S be Language;
let X be set ;
let phi be wff X -implied string of S;
cluster xnot (xnot phi) -> wff X -implied wff string of S;
coherence
for b₁ being wff string of S st b₁ = xnot (xnot phi) holds
b₁ is X -implied

proof end;

end;

definition

let X be set ;
let S be Language;
let phi be wff string of S;
attr phi is X -provable means :DefProvable4: :: FOMODEL4:def 70
phi is X,{(R9 S)} \/ (S -rules) -provable ;

end;

:: deftheorem DefProvable4 defines -provable FOMODEL4:def 70 :
for X being set
for S being Language
for phi being wff string of S holds
( phi is X -provable iff phi is X,{(R9 S)} \/ (S -rules) -provable );

begin

definition

let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
set SS = AllSymbolsOf S;
set EF = ExFormulasOf S;
set FF = AllFormulasOf S;
set Y = X \/ (AllFormulasOf S);
set DD = bool (X \/ (AllFormulasOf S));
func (D,num) AddWitnessesTo X -> Function of NAT,(bool (X \/ (AllFormulasOf S))) means :DefWit3: :: FOMODEL4:def 71
( it . 0 = X & ( for mm being Element of NAT holds it . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (it . mm) ) );
existence
ex b₁ being Function of NAT,(bool (X \/ (AllFormulasOf S))) st
( b₁ . 0 = X & ( for mm being Element of NAT holds b₁ . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b₁ . mm) ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT,(bool (X \/ (AllFormulasOf S))) st b₁ . 0 = X & ( for mm being Element of NAT holds b₁ . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b₁ . mm) ) & b₂ . 0 = X & ( for mm being Element of NAT holds b₂ . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b₂ . mm) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefWit3 defines AddWitnessesTo FOMODEL4:def 71 :
for X being functional set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(ExFormulasOf S)
for b₅ being Function of NAT,(bool (X \/ (AllFormulasOf S))) holds
( b₅ = (D,num) AddWitnessesTo X iff ( b₅ . 0 = X & ( for mm being Element of NAT holds b₅ . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b₅ . mm) ) ) );

notation

let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
synonym (D,num) addw X for (D,num) AddWitnessesTo X;

end;

Lm30: for X being set
for S being Language
for phi being wff string of S
for l1, l2 being literal Element of S
for D being RuleSet of S st D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent & not l2 is X \/ {phi} -occurring holds
X \/ {(<*l1*> ^ phi)} is D -inconsistent

proof end;

theorem Th18: :: FOMODEL4:17

for k, m being Nat
for S being Language
for D being RuleSet of S
for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D -inconsistent holds
( ((D,num) addw X) . k c= ((D,num) addw X) . (k + m) & not (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . m) /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not ((D,num) addw X) . m is D -inconsistent )

proof end;

definition

let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
func X WithWitnessesFrom (D,num) -> Subset of (X \/ (AllFormulasOf S)) equals :: FOMODEL4:def 72
union (rng ((D,num) AddWitnessesTo X));
coherence
union (rng ((D,num) AddWitnessesTo X)) is Subset of (X \/ (AllFormulasOf S))

proof end;

end;

:: deftheorem defines WithWitnessesFrom FOMODEL4:def 72 :
for X being functional set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(ExFormulasOf S) holds X WithWitnessesFrom (D,num) = union (rng ((D,num) AddWitnessesTo X));

notation

let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
synonym X addw (D,num) for X WithWitnessesFrom (D,num);

end;

Lm6: for S being Language
for D being RuleSet of S
for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone & R1 S in D & R2 S in D & R5 S in D & R8 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D -inconsistent holds
not X addw (D,num) is D -inconsistent

proof end;

registration

let X be functional set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(ExFormulasOf S);
cluster X \ (X addw (D,num)) -> empty set ;
coherence
for b₁ being set st b₁ = X \ (X addw (D,num)) holds
b₁ is empty

proof end;

end;

theorem Th19: :: FOMODEL4:18

for Z being set
for S being Language
for D being RuleSet of S
for X being functional set
for num being Function of NAT,(ExFormulasOf S) st D is isotone & R1 S in D & R8 S in D & R2 S in D & R5 S in D & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & X addw (D,num) c= Z & not Z is D -inconsistent & rng num = ExFormulasOf S holds
Z is S -witnessed

proof end;

begin

definition

let X be set ;
let S be Language;
let D be RuleSet of S;
let phi be Element of AllFormulasOf S;
func (D,phi) AddFormulaTo X -> set equals :DefAdd1: :: FOMODEL4:def 73
X \/ {phi} if not xnot phi is X,D -provable
otherwise X \/ {(xnot phi)};
consistency
for b₁ being set holds verum ;
coherence
( ( not xnot phi is X,D -provable implies X \/ {phi} is set ) & ( xnot phi is X,D -provable implies X \/ {(xnot phi)} is set ) ) ;

end;

:: deftheorem DefAdd1 defines AddFormulaTo FOMODEL4:def 73 :
for X being set
for S being Language
for D being RuleSet of S
for phi being Element of AllFormulasOf S holds
( ( not xnot phi is X,D -provable implies (D,phi) AddFormulaTo X = X \/ {phi} ) & ( xnot phi is X,D -provable implies (D,phi) AddFormulaTo X = X \/ {(xnot phi)} ) );

definition

let X be set ;
let S be Language;
let D be RuleSet of S;
let phi be Element of AllFormulasOf S;
:: original: AddFormulaTo
redefine func (D,phi) AddFormulaTo X -> Subset of (X \/ (AllFormulasOf S));
coherence
(D,phi) AddFormulaTo X is Subset of (X \/ (AllFormulasOf S))

proof end;

end;

registration

let X be set ;
let S be Language;
let D be RuleSet of S;
let phi be Element of AllFormulasOf S;
cluster X \ ((D,phi) AddFormulaTo X) -> empty ;
coherence
X \ ((D,phi) AddFormulaTo X) is empty

proof end;

end;

definition

let X be set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(AllFormulasOf S);
set SS = AllSymbolsOf S;
set FF = AllFormulasOf S;
set Y = X \/ (AllFormulasOf S);
set DD = bool (X \/ (AllFormulasOf S));
func (D,num) AddFormulasTo X -> Function of NAT,(bool (X \/ (AllFormulasOf S))) means :DefAdd2: :: FOMODEL4:def 74
( it . 0 = X & ( for m being Nat holds it . (m + 1) = (D,(num . m)) AddFormulaTo (it . m) ) );
existence
ex b₁ being Function of NAT,(bool (X \/ (AllFormulasOf S))) st
( b₁ . 0 = X & ( for m being Nat holds b₁ . (m + 1) = (D,(num . m)) AddFormulaTo (b₁ . m) ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT,(bool (X \/ (AllFormulasOf S))) st b₁ . 0 = X & ( for m being Nat holds b₁ . (m + 1) = (D,(num . m)) AddFormulaTo (b₁ . m) ) & b₂ . 0 = X & ( for m being Nat holds b₂ . (m + 1) = (D,(num . m)) AddFormulaTo (b₂ . m) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefAdd2 defines AddFormulasTo FOMODEL4:def 74 :
for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S)
for b₅ being Function of NAT,(bool (X \/ (AllFormulasOf S))) holds
( b₅ = (D,num) AddFormulasTo X iff ( b₅ . 0 = X & ( for m being Nat holds b₅ . (m + 1) = (D,(num . m)) AddFormulaTo (b₅ . m) ) ) );

Lm4: for k, m being Nat
for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent holds
( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & not ((D,num) AddFormulasTo X) . m is D -inconsistent )

proof end;

definition

let X be set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(AllFormulasOf S);
func (D,num) CompletionOf X -> Subset of (X \/ (AllFormulasOf S)) equals :: FOMODEL4:def 75
union (rng ((D,num) AddFormulasTo X));
coherence
union (rng ((D,num) AddFormulasTo X)) is Subset of (X \/ (AllFormulasOf S))

proof end;

end;

:: deftheorem defines CompletionOf FOMODEL4:def 75 :
for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) holds (D,num) CompletionOf X = union (rng ((D,num) AddFormulasTo X));

registration

let X be set ;
let S be Language;
let D be RuleSet of S;
let num be Function of NAT,(AllFormulasOf S);
cluster X \ ((D,num) CompletionOf X) -> empty set ;
coherence
for b₁ being set st b₁ = X \ ((D,num) CompletionOf X) holds
b₁ is empty

proof end;

end;

Lm5: for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st rng num = AllFormulasOf S holds
(D,num) CompletionOf X is S -covering

proof end;

Lm7: for X being set
for S being Language
for D being RuleSet of S
for num being Function of NAT,(AllFormulasOf S) st D is isotone & R1 S in D & R8 S in D & not X is D -inconsistent holds
not (D,num) CompletionOf X is D -inconsistent

proof end;

theorem :: FOMODEL4:19

for y, X being set
for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents) holds
( y in (FuncRule R) . X iff ( y in S -sequents & [X,y] in R ) ) by Lm1e;

Lm37: for S being Language
for D2 being 2 -ranked RuleSet of S
for X being functional set st AllFormulasOf S is countable & not (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is finite & not X is D2 -inconsistent & D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied

proof end;

Lm38: for S being Language
for D2 being 2 -ranked RuleSet of S
for X being functional set st X is finite & AllFormulasOf S is countable & not X is D2 -inconsistent & D2 is isotone holds
ex U being non empty set ex I being Element of U -InterpretersOf S st X is I -satisfied

proof end;

Lm39: for U being non empty set
for X being set
for S1, S2 being Language
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st S2 is S1 -extending & X c= AllFormulasOf S1 & I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
( X is I1 -satisfied iff X is I2 -satisfied )

proof end;

registration

let S be Language;
let r1, r2 be isotone Rule of S;
cluster {r1,r2} -> isotone RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = {r1,r2} holds
b₁ is isotone

proof end;

end;

registration

let S be Language;
let r1, r2, r3, r4 be isotone Rule of S;
cluster K323(r1,r2,r3,r4) -> isotone RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = {r1,r2,r3,r4} holds
b₁ is isotone

proof end;

end;

registration

let S be Language;
cluster S -rules -> isotone RuleSet of S;
coherence
for b₁ being RuleSet of S st b₁ = S -rules holds
b₁ is isotone

proof end;

end;

registration

let S be Language;
cluster functional isotone Correct Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
ex b₁ being isotone RuleSet of S st b₁ is Correct

proof end;

end;

registration

let S be Language;
cluster functional isotone 2 -ranked Correct Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));
existence
ex b₁ being isotone Correct RuleSet of S st b₁ is 2 -ranked

proof end;

end;

registration

let S be countable Language;
cluster AllFormulasOf S -> countable ;
coherence
AllFormulasOf S is countable ;

end;

theorem Th21: :: FOMODEL4:20

for Z being set
for S being countable Language
for D being RuleSet of S st D is 2 -ranked & D is isotone & D is Correct & not Z is D -inconsistent & Z c= AllFormulasOf S holds
ex U being non empty set ex I being Element of U -InterpretersOf S st Z is I -satisfied

proof end;

Lm55: for Z being set
for S being countable Language
for phi being wff string of S st Z c= AllFormulasOf S & xnot phi is Z -implied holds
xnot phi is Z,S -rules -provable

proof end;

theorem :: FOMODEL4:21

for X being set
for C being countable Language
for phi being wff string of C st X c= AllFormulasOf C & phi is X -implied holds
phi is X -provable

proof end;