:: by Marco B. Caminati

::

:: Received December 29, 2010

:: Copyright (c) 2010-2017 Association of Mizar Users

definition

let S be Language;

{ [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite } is set ;

end;
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 } ;

{ [premises,conclusion] where premises is Subset of (AllFormulasOf S), conclusion is wff string of S : premises is finite } is set ;

:: 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 } ;

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
end;

:: deftheorem Def2 defines -sequent-like FOMODEL4:def 2 :

for S being Language

for x being object holds

( x is S -sequent-like iff x in S -sequents );

for S being Language

for x being object holds

( x is S -sequent-like iff x in S -sequents );

:: deftheorem Def3 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 );

for S being Language

for X being set holds

( X is S -sequents-like iff X c= S -sequents );

registration

let S be Language;

coherence

for b_{1} being Subset of (S -sequents) holds b_{1} is S -sequents-like
;

coherence

for b_{1} being Element of S -sequents holds b_{1} is S -sequent-like
;

end;
coherence

for b

coherence

for b

registration

let S be Language;

existence

ex b_{1} being Element of S -sequents st b_{1} is S -sequent-like

ex b_{1} being Subset of (S -sequents) st b_{1} is S -sequents-like

end;
existence

ex b

proof end;

existence ex b

proof end;

registration

let S be Language;

existence

ex b_{1} being object st b_{1} is S -sequent-like

ex b_{1} being set st b_{1} is S -sequents-like

end;
existence

ex b

proof end;

existence ex b

proof end;

definition
end;

definition

let S be Language;

mode RuleSet of S is Subset of (Funcs ((bool (S -sequents)),(bool (S -sequents))));

end;
mode RuleSet of S is Subset of (Funcs ((bool (S -sequents)),(bool (S -sequents))));

registration

let S be Language;

let Sq be S -sequent-like object ;

coherence

{Sq} is S -sequents-like by ZFMISC_1:31, Def2;

end;
let Sq be S -sequent-like object ;

coherence

{Sq} is S -sequents-like by ZFMISC_1:31, Def2;

registration

let S be Language;

let SQ1, SQ2 be S -sequents-like set ;

coherence

SQ1 \/ SQ2 is S -sequents-like

end;
let SQ1, SQ2 be S -sequents-like set ;

coherence

SQ1 \/ SQ2 is S -sequents-like

proof end;

registration

let S be Language;

let x, y be S -sequent-like object ;

coherence

{x,y} is S -sequents-like

end;
let x, y be S -sequent-like object ;

coherence

{x,y} is S -sequents-like

proof end;

registration

let S be Language;

let phi be wff string of S;

let Phi1, Phi2 be finite Subset of (AllFormulasOf S);

coherence

[(Phi1 \/ Phi2),phi] is S -sequent-like ;

end;
let phi be wff string of S;

let Phi1, Phi2 be finite Subset of (AllFormulasOf S);

coherence

[(Phi1 \/ Phi2),phi] is S -sequent-like ;

registration

let S be Language;

let Y be set ;

let X be S -sequents-like set ;

coherence

X /\ Y is S -sequents-like

end;
let Y be set ;

let X be S -sequents-like set ;

coherence

X /\ Y is S -sequents-like

proof end;

registration

let S be Language;

let premises be finite Subset of (AllFormulasOf S);

let phi be wff string of S;

coherence

[premises,phi] is S -sequent-like ;

end;
let premises be finite Subset of (AllFormulasOf S);

let phi be wff string of S;

coherence

[premises,phi] is S -sequent-like ;

registration

let S be Language;

let phi1, phi2 be wff string of S;

coherence

[{phi1},phi2] is S -sequent-like

coherence

[{phi1,phi2},phi3] is S -sequent-like

end;
let phi1, phi2 be wff string of S;

coherence

[{phi1},phi2] is S -sequent-like

proof end;

let phi3 be wff string of S;coherence

[{phi1,phi2},phi3] is S -sequent-like

proof end;

registration

let S be Language;

let phi1, phi2 be wff string of S;

let Phi be finite Subset of (AllFormulasOf S);

coherence

[(Phi \/ {phi1}),phi2] is S -sequent-like

end;
let phi1, phi2 be wff string of S;

let Phi be finite Subset of (AllFormulasOf S);

coherence

[(Phi \/ {phi1}),phi2] is S -sequent-like

proof 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;
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 ;

:: deftheorem Def4 defines -premises-like FOMODEL4:def 4 :

for S being Language

for x being set holds

( x is S -premises-like iff ( x c= AllFormulasOf S & x is finite ) );

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;

coherence

for b_{1} being set st b_{1} is S -premises-like holds

b_{1} is finite
;

end;
coherence

for b

b

registration

let S be Language;

let phi be wff string of S;

coherence

{phi} is S -premises-like by FOMODEL2:16, ZFMISC_1:31;

end;
let phi be wff string of S;

coherence

{phi} is S -premises-like by FOMODEL2:16, ZFMISC_1:31;

registration
end;

registration

let X be set ;

let S be Language;

existence

ex b_{1} being Subset of X st b_{1} is S -premises-like

end;
let S be Language;

existence

ex b

proof end;

registration
end;

registration

let S be Language;

let X be S -premises-like set ;

coherence

for b_{1} being Subset of X holds b_{1} is S -premises-like

end;
let X be S -premises-like set ;

coherence

for b

proof 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 Def4;

end;
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 Def4;

registration

let S be Language;

let H be S -premises-like set ;

let x be set ;

coherence

H null x is S -premises-like ;

end;
let H be S -premises-like set ;

let x be set ;

coherence

H null x is S -premises-like ;

registration

let S be Language;

let H1, H2 be S -premises-like set ;

coherence

H1 \/ H2 is S -premises-like

end;
let H1, H2 be S -premises-like set ;

coherence

H1 \/ H2 is S -premises-like

proof end;

registration

let S be Language;

let H be S -premises-like set ;

let phi be wff string of S;

coherence

[H,phi] is S -sequent-like

end;
let H be S -premises-like set ;

let phi be wff string of S;

coherence

[H,phi] is S -sequent-like

proof end;

definition

let S be Language;

let D be RuleSet of S;

ex b_{1} being Rule of S st

for Seqs being Element of bool (S -sequents) holds b_{1} . Seqs = union ((union D) .: {Seqs})

for b_{1}, b_{2} being Rule of S st ( for Seqs being Element of bool (S -sequents) holds b_{1} . Seqs = union ((union D) .: {Seqs}) ) & ( for Seqs being Element of bool (S -sequents) holds b_{2} . Seqs = union ((union D) .: {Seqs}) ) holds

b_{1} = b_{2}

end;
let D be RuleSet of S;

func OneStep D -> Rule of S means :Def5: :: FOMODEL4:def 5

for Seqs being Element of bool (S -sequents) holds it . Seqs = union ((union D) .: {Seqs});

existence for Seqs being Element of bool (S -sequents) holds it . Seqs = union ((union D) .: {Seqs});

ex b

for Seqs being Element of bool (S -sequents) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines OneStep FOMODEL4:def 5 :

for S being Language

for D being RuleSet of S

for b_{3} being Rule of S holds

( b_{3} = OneStep D iff for Seqs being Element of bool (S -sequents) holds b_{3} . Seqs = union ((union D) .: {Seqs}) );

for S being Language

for D being RuleSet of S

for b

( b

Lm1: 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

( 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;

coherence

iter ((OneStep D),m) is Rule of S

end;
let D be RuleSet of S;

let m be Nat;

coherence

iter ((OneStep D),m) is Rule of S

proof end;

:: deftheorem defines -derivables FOMODEL4:def 6 :

for S being Language

for D being RuleSet of S

for m being Nat holds (m,D) -derivables = iter ((OneStep D),m);

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 be object ;

let Seqs2 be set ;

end;
let D be RuleSet of S;

let Seqs1 be object ;

let Seqs2 be set ;

attr Seqs2 is Seqs1,D -derivable means :Def7: :: FOMODEL4:def 7

Seqs2 c= union (((OneStep D) [*]) .: {Seqs1});

Seqs2 c= union (((OneStep D) [*]) .: {Seqs1});

:: deftheorem Def7 defines -derivable FOMODEL4:def 7 :

for S being Language

for D being RuleSet of S

for Seqs1 being object

for Seqs2 being set holds

( Seqs2 is Seqs1,D -derivable iff Seqs2 c= union (((OneStep D) [*]) .: {Seqs1}) );

for S being Language

for D being RuleSet of S

for Seqs1 being object

for Seqs2 being set holds

( Seqs2 is Seqs1,D -derivable iff Seqs2 c= union (((OneStep D) [*]) .: {Seqs1}) );

definition
end;

:: deftheorem defines -derivable FOMODEL4:def 8 :

for m being Nat

for S being Language

for D being RuleSet of S

for Seqts being set

for seqt being object holds

( seqt is m,Seqts,D -derivable iff seqt in ((m,D) -derivables) . Seqts );

for m being Nat

for S being Language

for D being RuleSet of S

for Seqts being set

for seqt being object 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;

{ (iter ((OneStep D),mm)) where mm is Element of NAT : verum } is Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):]

end;
let D be RuleSet of S;

func D -iterators -> Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):] equals :: FOMODEL4:def 9

{ (iter ((OneStep D),mm)) where mm is Element of NAT : verum } ;

coherence { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } ;

{ (iter ((OneStep D),mm)) where mm is Element of NAT : verum } is Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):]

proof end;

:: deftheorem defines -iterators FOMODEL4:def 9 :

for S being Language

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

for S being Language

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

:: deftheorem Def10 defines isotone FOMODEL4:def 10 :

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 );

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 );

Lm2: 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 ) )

by FUNCT_2:8;

registration

let S be Language;

ex b_{1} being Rule of S st b_{1} is isotone

end;
cluster Relation-like bool (S -sequents) -defined bool (S -sequents) -valued Function-like total quasi_total isotone for Element of Funcs ((bool (S -sequents)),(bool (S -sequents)));

existence ex b

proof end;

:: deftheorem Def11 defines isotone FOMODEL4:def 11 :

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 ) );

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;

coherence

for b_{1} being RuleSet of S st b_{1} = {M} holds

b_{1} is isotone

end;
let M be isotone Rule of S;

coherence

for b

b

proof end;

registration
end;

:: deftheorem defines -derivable FOMODEL4:def 12 :

for S being Language

for D being RuleSet of S

for Seqts being set holds

( Seqts is D -derivable iff Seqts is {} ,D -derivable );

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;

coherence

for b_{1} being set st b_{1} is D -derivable holds

b_{1} is {} ,D -derivable
;

coherence

for b_{1} being set st b_{1} is {} ,D -derivable holds

b_{1} is D -derivable
;

end;
let D be RuleSet of S;

coherence

for b

b

coherence

for b

b

registration

let S be Language;

let D be RuleSet of S;

let Seqts be empty set ;

coherence

for b_{1} being set st b_{1} is Seqts,D -derivable holds

b_{1} is D -derivable
;

end;
let D be RuleSet of S;

let Seqts be empty set ;

coherence

for b

b

:: deftheorem defines -provable FOMODEL4:def 13 :

for S being Language

for D being RuleSet of S

for X being set

for phi being object holds

( phi is X,D -provable iff ( {[X,phi]} is D -derivable or ex seqt being object st

( seqt `1 c= X & seqt `2 = phi & {seqt} is D -derivable ) ) );

for S being Language

for D being RuleSet of S

for X being set

for phi being object holds

( phi is X,D -provable iff ( {[X,phi]} is D -derivable or ex seqt being object 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 ;

( x is X,D -provable iff ex seqt being object st

( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) )

end;
let D be RuleSet of S;

let X, x be set ;

redefine attr x is X,D -provable means :Def14: :: FOMODEL4:def 14

ex seqt being object st

( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable );

compatibility ex seqt being object st

( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable );

( x is X,D -provable iff ex seqt being object st

( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) )

proof end;

:: deftheorem Def14 defines -provable FOMODEL4:def 14 :

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 object st

( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) );

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 object st

( seqt `1 c= X & seqt `2 = x & {seqt} is D -derivable ) );

definition

let S be Language;

let D be RuleSet of S;

let X be set ;

end;
let D be RuleSet of S;

let X be set ;

attr X is D -inconsistent means :: FOMODEL4:def 15

ex phi1, phi2 being wff string of S st

( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable );

ex phi1, phi2 being wff string of S st

( phi1 is X,D -provable & (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 is X,D -provable );

:: deftheorem defines -inconsistent FOMODEL4:def 15 :

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 ) );

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 ) );

Lm3: 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

by Def14;

registration

let S be Language;

let D be RuleSet of S;

let Phi1, Phi2 be set ;

coherence

for b_{1} being set st b_{1} is Phi1 \ Phi2,D -provable holds

b_{1} is Phi1,D -provable
by Lm3;

end;
let D be RuleSet of S;

let Phi1, Phi2 be set ;

coherence

for b

b

registration

let S be Language;

let D be RuleSet of S;

let Phi1, Phi2 be set ;

coherence

for b_{1} being set st b_{1} is Phi1 \ Phi2,D -provable holds

b_{1} is Phi1 \/ Phi2,D -provable
by XBOOLE_1:7, Lm3;

end;
let D be RuleSet of S;

let Phi1, Phi2 be set ;

coherence

for b

b

registration

let S be Language;

let D be RuleSet of S;

let Phi1, Phi2 be set ;

coherence

for b_{1} being set st b_{1} is Phi1 /\ Phi2,D -provable holds

b_{1} is Phi1,D -provable
by Lm3;

end;
let D be RuleSet of S;

let Phi1, Phi2 be set ;

coherence

for b

b

registration

let S be Language;

let D be RuleSet of S;

let X be set ;

let x be Subset of X;

coherence

for b_{1} being set st b_{1} is x,D -provable holds

b_{1} is X,D -provable
by Lm3;

end;
let D be RuleSet of S;

let X be set ;

let x be Subset of X;

coherence

for b

b

Lm4: 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

;

definition

let S be Language;

let D be RuleSet of S;

let Phi be set ;

{ [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } is set ;

end;
let D be RuleSet of S;

let Phi be set ;

func (Phi,D) -termEq -> set equals :: FOMODEL4:def 16

{ [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } ;

coherence { [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } ;

{ [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } is set ;

:: deftheorem defines -termEq FOMODEL4:def 16 :

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 } ;

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 } ;

:: deftheorem Def17 defines -expanded FOMODEL4:def 17 :

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 );

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 D be RuleSet of S;

let X be set ;

( X is D -expanded iff for x being set st x is X,D -provable holds

x in X )

end;
let D be RuleSet of S;

let X be set ;

redefine attr X is D -expanded means :Def18: :: FOMODEL4:def 18

for x being set st x is X,D -provable holds

x in X;

compatibility for x being set st x is X,D -provable holds

x in X;

( X is D -expanded iff for x being set st x is X,D -provable holds

x in X )

proof end;

:: deftheorem Def18 defines -expanded FOMODEL4:def 18 :

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 );

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 );

:: deftheorem defines -null FOMODEL4:def 19 :

for S being Language

for x being set holds

( x is S -null iff verum );

for S being Language

for x being set holds

( x is S -null iff verum );

registration

let S be Language;

coherence

for b_{1} being set st b_{1} is S -sequent-like holds

b_{1} is S -null
;

end;
coherence

for b

b

::#####################################################################

::#####################################################################

::#####################################################################

::#Type Tuning

::#####################################################################

::#####################################################################

::#Type Tuning

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)

end;
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;

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

end;
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;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} is S -sequent-like holds

b_{1} is S -null
;

end;
coherence

for b

b

registration
end;

registration

let m be Nat;

let S be Language;

let D be RuleSet of S;

let X be set ;

coherence

((m,D) -derivables) . X is S -sequents-like

end;
let S be Language;

let D be RuleSet of S;

let X be set ;

coherence

((m,D) -derivables) . X is S -sequents-like

proof end;

registration

let S be Language;

let D be RuleSet of S;

let m be Nat;

let X be set ;

coherence

for b_{1} being object st b_{1} is m,X,D -derivable holds

b_{1} is S -sequent-like

end;
let D be RuleSet of S;

let m be Nat;

let X be set ;

coherence

for b

b

proof end;

Lm5: 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;

Lm6: for S being Language

for R being Rule of S holds R = OneStep {R}

proof end;

Lm7: 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;

Lm8: for S being Language

for D being RuleSet of S

for Seqts being Subset of (S -sequents)

for y being object st {y} is Seqts,D -derivable holds

ex mm being Element of NAT st y is mm,Seqts,D -derivable

proof end;

Lm9: 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;

Lm10: 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;

Lm11: 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;

Lm12: for m being Nat

for X being set

for S being Language

for D being RuleSet of S

for x being object st x is m,X,D -derivable holds

{x} is X,D -derivable

proof end;

Lm13: 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;

Lm14: 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;

Lm15: for m being Nat

for S being Language

for D1, D2 being RuleSet of S

for SQ1, SQ2 being b

((m,D1) -derivables) . SQ1 c= ((m,D2) -derivables) . SQ2

proof end;

Lm16: 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;

Lm17: 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;

Lm18: for X, Y 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;

Lm19: 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;

Lm20: 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;

Lm21: for m, n being Nat

for Z being set

for S being Language

for D1, D2 being RuleSet of S

for SQ1, SQ2 being b

Z c= (iter ((OneStep (D1 \/ D2)),(m + n))) . SQ1

proof end;

Lm22: for m, n being Nat

for X being set

for S being Language

for D1, D2 being RuleSet of S

for y, z being object 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;

Lm24: for S being Language

for Sq being b

proof end;

Lm25: 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;

Lm26: 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;

ex b_{1} being Subset of (AllFormulasOf S) st b_{1} is D -expanded

end;
let D be RuleSet of S;

cluster V18() functional V42() FinSequence-membered with_non-empty_elements D -expanded for Element of bool (AllFormulasOf S);

existence ex b

proof end;

registration

let S be Language;

let D be RuleSet of S;

existence

ex b_{1} being set st b_{1} is D -expanded

end;
let D be RuleSet of S;

existence

ex b

proof end;

registration

let S be Language;

let D be RuleSet of S;

let X be set ;

coherence

for b_{1} being set st b_{1} is X,D -derivable holds

b_{1} is S -sequents-like

end;
let D be RuleSet of S;

let X be set ;

coherence

for b

b

proof end;

definition

let S be Language;

let D be RuleSet of S;

let X, x be set ;

( x is X,D -provable iff ex H being set ex m being Nat st

( H c= X & [H,x] is m, {} ,D -derivable ) )

end;
let D be RuleSet of S;

let X, x be set ;

redefine attr x is X,D -provable means :Def20: :: FOMODEL4:def 20

ex H being set ex m being Nat st

( H c= X & [H,x] is m, {} ,D -derivable );

compatibility ex H being set ex m being Nat st

( H c= X & [H,x] is m, {} ,D -derivable );

( 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;

:: deftheorem Def20 defines -provable FOMODEL4:def 20 :

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 ) );

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 :: FOMODEL4:1

for y being set

for S being Language

for D being RuleSet of S

for SQ being b_{2} -sequents-like set st {y} is SQ,D -derivable holds

ex mm being Element of NAT st y is mm,SQ,D -derivable

for S being Language

for D being RuleSet of S

for SQ being b

ex mm being Element of NAT st y is mm,SQ,D -derivable

proof end;

theorem Th2: :: FOMODEL4:2

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

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;

::############################################################################

::# Encoding of modified Gentzen rules

::# Encoding of modified Gentzen rules

definition

let Seqts be set ;

let S be Language;

let seqt be S -null set ;

end;
let S be Language;

let seqt be S -null set ;

::# assumption rule; could be weakened to seqt`1={seqt`2}, since the

::# stronger form overlaps with Rule1

::# stronger form overlaps with Rule1

pred seqt Rule1 Seqts means :: FOMODEL4:def 22

ex y being set st

( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 );

ex y being set st

( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 );

pred seqt Rule2 Seqts means :: FOMODEL4:def 23

( seqt `1 is empty & ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t );

( seqt `1 is empty & ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t );

pred seqt Rule3a Seqts means :: FOMODEL4:def 24

ex t1, t2, t3 being termal string of S st seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)];

ex t1, t2, t3 being termal string of S st seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)];

pred seqt Rule3b Seqts means :: FOMODEL4:def 25

ex t1, t2 being termal string of S st

( seqt `1 = {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & seqt `2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 );

ex t1, t2 being termal string of S st

( seqt `1 = {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & seqt `2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 );

pred seqt Rule3d Seqts means :: FOMODEL4:def 26

ex s being low-compounding Element of S ex T, U being |.(ar b_{1}).| -element Element of (AllTermsOf S) * st

( s is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) );

ex s being low-compounding Element of S ex T, U being |.(ar b

( s is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) );

pred seqt Rule3e Seqts means :: FOMODEL4:def 27

ex s being relational Element of S ex T, U being |.(ar b_{1}).| -element Element of (AllTermsOf S) * st

( seqt `1 = {(s -compound T)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = s -compound U );

ex s being relational Element of S ex T, U being |.(ar b

( seqt `1 = {(s -compound T)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = s -compound U );

pred seqt Rule4 Seqts means :: FOMODEL4:def 28

ex l being literal Element of S 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 );

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 :: FOMODEL4:def 29

ex v1, v2 being literal Element of S ex x being set ex p being FinSequence st

( seqt `1 = x \/ {(<*v1*> ^ p)} & v2 is (x \/ {p}) \/ {(seqt `2)} -absent & [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts );

ex v1, v2 being literal Element of S ex x being set ex p being FinSequence st

( seqt `1 = x \/ {(<*v1*> ^ p)} & v2 is (x \/ {p}) \/ {(seqt `2)} -absent & [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts );

pred seqt Rule6 Seqts means :: FOMODEL4:def 30

ex y1, y2 being set 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 );

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 :: FOMODEL4:def 31

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 );

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 defines Rule0 FOMODEL4:def 21 :

for Seqts being set

for S being Language

for seqt being b_{2} -null set holds

( seqt Rule0 Seqts iff seqt `2 in seqt `1 );

for Seqts being set

for S being Language

for seqt being b

( seqt Rule0 Seqts iff seqt `2 in seqt `1 );

:: deftheorem defines Rule1 FOMODEL4:def 22 :

for Seqts being set

for S being Language

for seqt being b_{2} -null set holds

( seqt Rule1 Seqts iff ex y being set st

( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 ) );

for Seqts being set

for S being Language

for seqt being b

( seqt Rule1 Seqts iff ex y being set st

( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 ) );

:: deftheorem defines Rule2 FOMODEL4:def 23 :

for Seqts being set

for S being Language

for seqt being b_{2} -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 ) );

for Seqts being set

for S being Language

for seqt being b

( seqt Rule2 Seqts iff ( seqt `1 is empty & ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t ) );

:: deftheorem defines Rule3a FOMODEL4:def 24 :

for Seqts being set

for S being Language

for seqt being b_{2} -null set holds

( seqt Rule3a Seqts iff ex t1, t2, t3 being termal string of S st seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] );

for Seqts being set

for S being Language

for seqt being b

( seqt Rule3a Seqts iff ex t1, t2, t3 being termal string of S st seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] );

:: deftheorem defines Rule3b FOMODEL4:def 25 :

for Seqts being set

for S being Language

for seqt being b_{2} -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 ) );

for Seqts being set

for S being Language

for seqt being b

( 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 defines Rule3d FOMODEL4:def 26 :

for Seqts being set

for S being Language

for seqt being b_{2} -null set holds

( seqt Rule3d Seqts iff ex s being low-compounding Element of S ex T, U being |.(ar b_{4}).| -element Element of (AllTermsOf S) * st

( s is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) ) );

for Seqts being set

for S being Language

for seqt being b

( seqt Rule3d Seqts iff ex s being low-compounding Element of S ex T, U being |.(ar b

( s is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) ) );

:: deftheorem defines Rule3e FOMODEL4:def 27 :

for Seqts being set

for S being Language

for seqt being b_{2} -null set holds

( seqt Rule3e Seqts iff ex s being relational Element of S ex T, U being |.(ar b_{4}).| -element Element of (AllTermsOf S) * st

( seqt `1 = {(s -compound T)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = s -compound U ) );

for Seqts being set

for S being Language

for seqt being b

( seqt Rule3e Seqts iff ex s being relational Element of S ex T, U being |.(ar b

( seqt `1 = {(s -compound T)} \/ { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg |.(ar s).|, TT, UU is Function of (Seg |.(ar s).|),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = s -compound U ) );

:: deftheorem defines Rule4 FOMODEL4:def 28 :

for Seqts being set

for S being Language

for seqt being b_{2} -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 ) );

for Seqts being set

for S being Language

for seqt being b

( 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 defines Rule5 FOMODEL4:def 29 :

for Seqts being set

for S being Language

for seqt being b_{2} -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)} & v2 is (x \/ {p}) \/ {(seqt `2)} -absent & [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts ) );

for Seqts being set

for S being Language

for seqt being b

( 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)} & v2 is (x \/ {p}) \/ {(seqt `2)} -absent & [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts ) );

:: deftheorem defines Rule6 FOMODEL4:def 30 :

for Seqts being set

for S being Language

for seqt being b_{2} -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 ) );

for Seqts being set

for S being Language

for seqt being b

( 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 defines Rule7 FOMODEL4:def 31 :

for Seqts being set

for S being Language

for seqt being b_{2} -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 ) );

for Seqts being set

for S being Language

for seqt being b

( 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 defines Rule8 FOMODEL4:def 32 :

for Seqts being set

for S being Language

for seqt being b_{2} -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 ) );

for Seqts being set

for S being Language

for seqt being b

( 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 defines Rule9 FOMODEL4:def 33 :

for Seqts being set

for S being Language

for seqt being b_{2} -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) ) );

for Seqts being set

for S being Language

for seqt being b

( 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;

ex b_{1} 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_{1} iff seqt Rule0 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule0 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule0 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule1 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule1 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule1 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule2 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule2 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule2 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule3a Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule3a Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3a Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule3b Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule3b Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3b Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule3d Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule3d Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3d Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule3e Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule3e Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3e Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule4 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule4 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule4 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule5 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule5 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule5 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule6 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule6 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule6 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule7 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule7 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule7 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule8 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule8 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule8 Seqts ) ) holds

b_{1} = b_{2}

ex b_{1} 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_{1} iff seqt Rule9 Seqts )

for b_{1}, b_{2} 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_{1} iff seqt Rule9 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule9 Seqts ) ) holds

b_{1} = b_{2}

end;
func P#0 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def34: :: 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 Rule0 Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule0 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#1 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def35: :: 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 Rule1 Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule1 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#2 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def36: :: 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 Rule2 Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule2 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#3a S -> Relation of (bool (S -sequents)),(S -sequents) means :Def37: :: 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 Rule3a Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule3a Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#3b S -> Relation of (bool (S -sequents)),(S -sequents) means :Def38: :: 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 Rule3b Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule3b Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#3d S -> Relation of (bool (S -sequents)),(S -sequents) means :Def39: :: 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 Rule3d Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule3d Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#3e S -> Relation of (bool (S -sequents)),(S -sequents) means :Def40: :: 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 Rule3e Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule3e Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#4 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def41: :: 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 Rule4 Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule4 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#5 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def42: :: 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 Rule5 Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule5 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#6 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def43: :: 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 Rule6 Seqts );

existence for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule6 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#7 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def44: :: FOMODEL4:def 44

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 for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule7 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#8 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def45: :: FOMODEL4:def 45

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 for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule8 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

func P#9 S -> Relation of (bool (S -sequents)),(S -sequents) means :Def46: :: FOMODEL4:def 46

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 for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in it iff seqt Rule9 Seqts );

ex b

for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

proof end;

uniqueness for b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

b

proof end;

:: deftheorem Def34 defines P#0 FOMODEL4:def 34 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#0 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule0 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def35 defines P#1 FOMODEL4:def 35 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#1 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule1 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def36 defines P#2 FOMODEL4:def 36 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#2 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule2 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def37 defines P#3a FOMODEL4:def 37 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#3a S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3a Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def38 defines P#3b FOMODEL4:def 38 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#3b S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3b Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def39 defines P#3d FOMODEL4:def 39 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#3d S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3d Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def40 defines P#3e FOMODEL4:def 40 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#3e S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule3e Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def41 defines P#4 FOMODEL4:def 41 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#4 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule4 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def42 defines P#5 FOMODEL4:def 42 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#5 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule5 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def43 defines P#6 FOMODEL4:def 43 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#6 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule6 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def44 defines P#7 FOMODEL4:def 44 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#7 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule7 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def45 defines P#8 FOMODEL4:def 45 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#8 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule8 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

:: deftheorem Def46 defines P#9 FOMODEL4:def 46 :

for S being Language

for b_{2} being Relation of (bool (S -sequents)),(S -sequents) holds

( b_{2} = P#9 S iff for Seqts being Element of bool (S -sequents)

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b_{2} iff seqt Rule9 Seqts ) );

for S being Language

for b

( b

for seqt being Element of S -sequents holds

( [Seqts,seqt] in b

definition

let S be Language;

let R be Relation of (bool (S -sequents)),(S -sequents);

ex b_{1} being Rule of S st

for inseqs being set st inseqs in bool (S -sequents) holds

b_{1} . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R }

for b_{1}, b_{2} being Rule of S st ( for inseqs being set st inseqs in bool (S -sequents) holds

b_{1} . 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_{2} . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) holds

b_{1} = b_{2}

end;
let R be Relation of (bool (S -sequents)),(S -sequents);

func FuncRule R -> Rule of S means :Def47: :: FOMODEL4:def 47

for inseqs being set st inseqs in bool (S -sequents) holds

it . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ;

existence 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 } ;

ex b

for inseqs being set st inseqs in bool (S -sequents) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def47 defines FuncRule FOMODEL4:def 47 :

for S being Language

for R being Relation of (bool (S -sequents)),(S -sequents)

for b_{3} being Rule of S holds

( b_{3} = FuncRule R iff for inseqs being set st inseqs in bool (S -sequents) holds

b_{3} . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } );

for S being Language

for R being Relation of (bool (S -sequents)),(S -sequents)

for b

( b

b

Lm27: 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;

theorem Th3: :: FOMODEL4:3

for S being Language

for SQ being b_{1} -sequents-like set

for Sq being b_{1} -sequent-like object

for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds

Sq in (FuncRule R) . SQ

for SQ being b

for Sq being b

for R being Relation of (bool (S -sequents)),(S -sequents) st [SQ,Sq] in R holds

Sq in (FuncRule R) . SQ

proof end;

Lm28: for S being Language

for SQ being b

for Sq being b

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;

Lm29: for y being set

for S being Language

for SQ being b

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;

Lm30: for X, y 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;

coherence

FuncRule (P#0 S) is Rule of S ;

coherence

FuncRule (P#1 S) is Rule of S ;

coherence

FuncRule (P#2 S) is Rule of S ;

coherence

FuncRule (P#3a S) is Rule of S ;

coherence

FuncRule (P#3b S) is Rule of S ;

coherence

FuncRule (P#3d S) is Rule of S ;

coherence

FuncRule (P#3e S) is Rule of S ;

coherence

FuncRule (P#4 S) is Rule of S ;

coherence

FuncRule (P#5 S) is Rule of S ;

coherence

FuncRule (P#6 S) is Rule of S ;

coherence

FuncRule (P#7 S) is Rule of S ;

coherence

FuncRule (P#8 S) is Rule of S ;

coherence

FuncRule (P#9 S) is Rule of S ;

end;
coherence

FuncRule (P#0 S) is Rule of S ;

coherence

FuncRule (P#1 S) is Rule of S ;

coherence

FuncRule (P#2 S) is Rule of S ;

coherence

FuncRule (P#3a S) is Rule of S ;

coherence

FuncRule (P#3b S) is Rule of S ;

coherence

FuncRule (P#3d S) is Rule of S ;

coherence

FuncRule (P#3e S) is Rule of S ;

coherence

FuncRule (P#4 S) is Rule of S ;

coherence

FuncRule (P#5 S) is Rule of S ;

coherence

FuncRule (P#6 S) is Rule of S ;

coherence

FuncRule (P#7 S) is Rule of S ;

coherence

FuncRule (P#8 S) is Rule of S ;

coherence

FuncRule (P#9 S) is Rule of S ;

registration

let S be Language;

let t be termal string of S;

coherence

for b_{1} being set st b_{1} = {[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} holds

b_{1} is {(R#2 S)} -derivable

end;
let t be termal string of S;

coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#1 S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#2 S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

Lm31: for X being set

for S being Language

for D being RuleSet of S st {(R#2 S)} c= D holds

(X,D) -termEq is total

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#3b S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

Lm32: for X being set

for S being Language

for D being RuleSet of S st {(R#3b S)} c= D & X is D -expanded holds

(X,D) -termEq is symmetric

proof end;

registration

let S be Language;

let phi be wff string of S;

let Phi be finite Subset of (AllFormulasOf S);

coherence

for b_{1} being object st b_{1} = [(Phi \/ {phi}),phi] holds

b_{1} is 1, {} ,{(R#0 S)} -derivable

end;
let phi be wff string of S;

let Phi be finite Subset of (AllFormulasOf S);

coherence

for b

b

proof end;

registration

let S be Language;

let phi1, phi2 be wff string of S;

coherence

for b_{1} being object st b_{1} = [{phi1,phi2},phi1] holds

b_{1} is 1, {} ,{(R#0 S)} -derivable

end;
let phi1, phi2 be wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let phi be wff string of S;

coherence

for b_{1} being object st b_{1} = [{phi},phi] holds

b_{1} is 1, {} ,{(R#0 S)} -derivable

end;
let phi be wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let phi be wff string of S;

coherence

for b_{1} being set st b_{1} = {[{phi},phi]} holds

b_{1} is {} ,{(R#0 S)} -derivable
by Lm12;

end;
let phi be wff string of S;

coherence

for b

b

registration

let S be Language;

set E = TheEqSymbOf S;

coherence

for b_{1} being Rule of S st b_{1} = R#0 S holds

b_{1} is isotone

for b_{1} being Rule of S st b_{1} = R#3a S holds

b_{1} is isotone

for b_{1} being Rule of S st b_{1} = R#3d S holds

b_{1} is isotone

for b_{1} being Rule of S st b_{1} = R#3e S holds

b_{1} is isotone

coherence

for b_{1} being RuleSet of S st b_{1} = K1 \/ K2 holds

b_{1} is isotone

end;
set E = TheEqSymbOf S;

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

let K1, K2 be isotone RuleSet of S;coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#6 S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#8 S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#7 S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

registration

let S be Language;

let t1, t2, t3 be termal string of S;

for b_{1} being object st b_{1} = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] holds

b_{1} is 1, {} ,{(R#3a S)} -derivable

end;
let t1, t2, t3 be termal string of S;

cluster [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] -> 1, {} ,{(R#3a S)} -derivable for object ;

coherence for b

b

proof end;

registration

let S be Language;

let H1, H2 be S -premises-like set ;

let phi be wff string of S;

coherence

for b_{1} being object st b_{1} = [(H1 \/ H2),phi] holds

b_{1} is 1,{[H1,phi]},{(R#1 S)} -derivable

end;
let H1, H2 be S -premises-like set ;

let phi be wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let H be S -premises-like set ;

let phi be wff string of S;

coherence

for b_{1} being object st b_{1} = [(H \/ {phi}),phi] holds

b_{1} is 1, {} ,{(R#0 S)} -derivable

end;
let H be S -premises-like set ;

let phi be wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let H be S -premises-like set ;

let phi1, phi2 be wff string of S;

for b_{1} being object st b_{1} = [H,((<*(TheNorSymbOf S)*> ^ phi2) ^ phi1)] holds

b_{1} is 1,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#7 S)} -derivable

end;
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)]},{(R#7 S)} -derivable for object ;

coherence for b

b

proof end;

registration

let S be Language;

let Sq be S -sequent-like object ;

coherence

for b_{1} being set st b_{1} = Sq `1 holds

b_{1} is S -premises-like

end;
let Sq be S -sequent-like object ;

coherence

for b

b

proof 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;

for b_{1} being object st b_{1} = [((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] holds

b_{1} is 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R#5 S)} -derivable

end;
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]},{(R#5 S)} -derivable for object ;

coherence for b

b

proof end;

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;

coherence

for b_{1} being object st b_{1} = [((H1 \/ H2) null m1),phi] holds

b_{1} is m1,{[H1,phi]},{(R#1 S)} -derivable

end;
let S be Language;

let H1, H2 be S -premises-like set ;

let phi be wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

not for b_{1} being isotone RuleSet of S holds b_{1} is empty

end;
cluster non empty functional isotone for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

existence not for b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#5 S holds

b_{1} is isotone

end;
coherence

for b

b

proof 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;

coherence

for b_{1} being object st b_{1} = [{((l,t) SubstIn phi)},(<*l*> ^ phi)] holds

b_{1} is 1, {} ,{(R#4 S)} -derivable

end;
let l be literal Element of S;

let t be termal string of S;

let phi be wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let H be S -premises-like set ;

let phi, phi1, phi2 be wff string of S;

for b_{1} being object st b_{1} = [(H null (phi1 ^ phi2)),(xnot phi)] holds

b_{1} is 1,{[(H \/ {phi}),phi1],[(H \/ {phi}),((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},{(R#8 S)} -derivable

end;
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)]},{(R#8 S)} -derivable for object ;

coherence for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#4 S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

Lm33: for X being set

for S being Language

for D being RuleSet of S st {(R#3a S)} c= D & X is D -expanded holds

(X,D) -termEq is transitive

proof end;

Lm34: for X being set

for S being Language

for D being RuleSet of S st {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded holds

(X,D) -termEq is Equivalence_Relation of (AllTermsOf S)

proof end;

definition

let S be Language;

let m be non zero Nat;

let T, U be m -element Element of (AllTermsOf S) * ;

{ ((<*(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;
let m be non zero Nat;

let T, U be m -element Element of (AllTermsOf S) * ;

func PairWiseEq (T,U) -> set equals :: FOMODEL4:def 61

{ ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg m, TT, UU is Function of (Seg m),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } ;

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 ) } ;

{ ((<*(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 ;

:: deftheorem defines PairWiseEq FOMODEL4:def 61 :

for S being Language

for m being non zero Nat

for T, U being b_{2} -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 ) } ;

for S being Language

for m being non zero Nat

for T, U being b

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)

end;
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;

registration

let S be Language;

let m be non zero Nat;

let T, U be m -element Element of (AllTermsOf S) * ;

coherence

PairWiseEq (T,U) is finite

end;
let m be non zero Nat;

let T, U be m -element Element of (AllTermsOf S) * ;

coherence

PairWiseEq (T,U) is finite

proof end;

Lm35: for S being Language

for s being low-compounding Element of S

for T, U being |.(ar b

{[(PairWiseEq (T,U)),((<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U))]} is {} ,{(R#3d S)} -derivable

proof end;

Lm36: for S being Language

for s being relational Element of S

for T1, T2 being |.(ar b

proof end;

registration

let S be Language;

let s be relational Element of S;

let T1, T2 be |.(ar s).| -element Element of (AllTermsOf S) * ;

{[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e S)} -derivable by Lm36;

end;
let s be relational Element of S;

let T1, T2 be |.(ar s).| -element Element of (AllTermsOf S) * ;

cluster {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} -> {} ,{(R#3e S)} -derivable ;

coherence {[((PairWiseEq (T1,T2)) \/ {(s -compound T1)}),(s -compound T2)]} is {} ,{(R#3e S)} -derivable by Lm36;

Lm37: 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 |.(ar s).| -placesOf ((X,D) -termEq) holds

ex T, U being |.(ar b

( T = x1 & U = x2 & PairWiseEq (T,U) c= X )

proof end;

Lm38: for X being set

for S being Language

for D being RuleSet of S

for s being low-compounding Element of S st {(R#3d S)} c= D & X is D -expanded & s is termal holds

X -freeInterpreter s is (X,D) -termEq -respecting

proof end;

Lm39: for X, x1, x2 being set

for S being Language

for r being relational Element of S

for D being RuleSet of S st {(R#3e S)} c= D & X is D -expanded & [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) & (r -compound) . x1 in X holds

(r -compound) . x2 in X

proof end;

Lm40: for X, x1, x2 being set

for S being Language

for r being relational Element of S

for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded & [x1,x2] in |.(ar r).| -placesOf ((X,D) -termEq) holds

( (r -compound) . x1 in X iff (r -compound) . x2 in X )

proof end;

Lm41: for X being set

for S being Language

for r being relational Element of S

for D being RuleSet of S st {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds

X -freeInterpreter r is (X,D) -termEq -respecting

proof end;

Lm42: for X being set

for S being Language

for l being literal Element of S

for D being RuleSet of S st {(R#3a S)} c= D & {(R#2 S),(R#3b S)} c= D & X is D -expanded holds

X -freeInterpreter l is (X,D) -termEq -respecting

proof end;

Lm43: for X being set

for S being Language

for a being ofAtomicFormula Element of S

for D being RuleSet of S st {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e 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;

( ( m = 0 & m = 1 implies ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) ) ) & ( m = 0 & m = 2 implies ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D iff ( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) ) ) & ( m = 1 & m = 2 implies ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D iff ( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) ) ) ) ;

end;
let S be Language;

let D be RuleSet of S;

attr D is m -ranked means :Def62: :: FOMODEL4:def 62

( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D ) if m = 0

( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) if m = 1

( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) if m = 2

otherwise D = {} ;

consistency ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D ) if m = 0

( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) if m = 1

( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) if m = 2

otherwise D = {} ;

( ( m = 0 & m = 1 implies ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) ) ) & ( m = 0 & m = 2 implies ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D iff ( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) ) ) & ( m = 1 & m = 2 implies ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D iff ( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) ) ) ) ;

:: deftheorem Def62 defines -ranked FOMODEL4:def 62 :

for m being Nat

for S being Language

for D being RuleSet of S holds

( ( m = 0 implies ( D is m -ranked iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D ) ) ) & ( m = 1 implies ( D is m -ranked iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) ) ) & ( m = 2 implies ( D is m -ranked iff ( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) ) ) & ( not m = 0 & not m = 1 & not m = 2 implies ( D is m -ranked iff D = {} ) ) );

for m being Nat

for S being Language

for D being RuleSet of S holds

( ( m = 0 implies ( D is m -ranked iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D ) ) ) & ( m = 1 implies ( D is m -ranked iff ( R#0 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D ) ) ) & ( m = 2 implies ( D is m -ranked iff ( R#0 S in D & R#1 S in D & R#2 S in D & R#3a S in D & R#3b S in D & R#3d S in D & R#3e S in D & R#4 S in D & R#5 S in D & R#6 S in D & R#7 S in D & R#8 S in D ) ) ) & ( not m = 0 & not m = 1 & not m = 2 implies ( D is m -ranked iff D = {} ) ) );

registration

let S be Language;

for b_{1} being RuleSet of S st b_{1} is 1 -ranked holds

b_{1} is 0 -ranked

for b_{1} being RuleSet of S st b_{1} is 2 -ranked holds

b_{1} is 1 -ranked

end;
cluster 1 -ranked -> 0 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

coherence for b

b

proof end;

cluster 2 -ranked -> 1 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

coherence for b

b

proof end;

definition

let S be Language;

{(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} is RuleSet of S ;

end;
func S -rules -> RuleSet of S equals :: FOMODEL4:def 63

{(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)};

coherence {(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)};

{(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)} is RuleSet of S ;

:: deftheorem defines -rules FOMODEL4:def 63 :

for S being Language holds S -rules = {(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)};

for S being Language holds S -rules = {(R#0 S),(R#1 S),(R#2 S),(R#3a S),(R#3b S),(R#3d S),(R#3e S),(R#4 S)} \/ {(R#5 S),(R#6 S),(R#7 S),(R#8 S)};

registration

let S be Language;

coherence

for b_{1} being RuleSet of S st b_{1} = S -rules holds

b_{1} is 2 -ranked

end;
coherence

for b

b

proof end;

registration

let S be Language;

ex b_{1} being RuleSet of S st b_{1} is 2 -ranked

end;
cluster functional 2 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

existence ex b

proof end;

registration

let S be Language;

ex b_{1} being RuleSet of S st b_{1} is 1 -ranked

end;
cluster functional 1 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

existence ex b

proof end;

registration

let S be Language;

ex b_{1} being RuleSet of S st b_{1} is 0 -ranked

end;
cluster functional 0 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

existence ex b

proof end;

Lm44: 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;

coherence

for b_{1} being Interpreter of a, AllTermsOf S st b_{1} = X -freeInterpreter a holds

b_{1} is (X,D) -termEq -respecting
by Lm44;

end;
let D be 1 -ranked RuleSet of S;

let X be D -expanded set ;

let a be ofAtomicFormula Element of S;

coherence

for b

b

Lm45: 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 ;

coherence

for b_{1} being Relation of (AllTermsOf S) st b_{1} = (X,D) -termEq holds

( b_{1} is total & b_{1} is symmetric & b_{1} is transitive )
by Lm45;

end;
let D be 0 -ranked RuleSet of S;

let X be D -expanded set ;

coherence

for b

( b

registration

let S be Language;

ex b_{1} being 0 -ranked RuleSet of S st b_{1} is 1 -ranked

end;
cluster functional 0 -ranked 1 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

existence ex b

proof end;

theorem :: FOMODEL4:4

for X, Y 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 Lm18;

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 Lm18;

Lm46: for m, n being Nat

for S being Language

for D1, D2, D3 being RuleSet of S

for SQ1, SQ2 being b

for x, y, z being object 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;

registration

let S be Language;

let H be S -premises-like set ;

let phi1, phi2 be wff string of S;

[(H null phi2),(xnot phi1)] is 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)} -derivable

end;
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)]},({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)} -derivable ;

coherence [(H null phi2),(xnot phi1)] is 2,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)} -derivable

proof end;

registration

let S be Language;

let H be S -premises-like set ;

let phi1, phi2 be wff string of S;

for b_{1} being object st b_{1} = [(H null phi1),(xnot phi2)] holds

b_{1} is 3,{[H,((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)]},(({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)}) \/ {(R#7 S)} -derivable

end;
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)]},(({(R#0 S)} \/ {(R#1 S)}) \/ {(R#8 S)}) \/ {(R#7 S)} -derivable for object ;

coherence for b

b

proof end;

Lm47: 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 & R#1 S in D & R#8 S in D & X \/ {phi} is D -inconsistent holds

xnot phi is X,D -provable

proof end;

Lm48: 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 & R#1 S in D & R#8 S in D holds

xnot phi is X,D -provable

proof end;

Lm49: 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 & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & X \/ {((l1,l2) -SymbolSubstIn phi)} is D -inconsistent & l2 is X \/ {phi} -absent holds

X \/ {(<*l1*> ^ phi)} is D -inconsistent

proof end;

registration

let S be Language;

let phi1, phi2 be wff string of S;

for b_{1} being object st b_{1} = [{(xnot phi1),(xnot phi2)},((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)] holds

b_{1} is 1,{[{(xnot phi1),(xnot phi2)},(xnot phi1)],[{(xnot phi1),(xnot phi2)},(xnot phi2)]},{(R#6 S)} -derivable

end;
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)]},{(R#6 S)} -derivable for object ;

coherence for b

b

proof end;

registration

let S be Language;

let phi1, phi2 be wff string of S;

coherence

for b_{1} being object st b_{1} = [{phi1,phi2},phi2] holds

b_{1} is 1, {} ,{(R#0 S)} -derivable

end;
let phi1, phi2 be wff string of S;

coherence

for b

b

proof end;

theorem :: FOMODEL4:5

theorem Th6: :: FOMODEL4:6

for X being set

for S being Language

for phi being wff string of S st phi in X holds

phi is X,{(R#0 S)} -provable

for S being Language

for phi being wff string of S st phi in X holds

phi is X,{(R#0 S)} -provable

proof end;

theorem :: FOMODEL4:7

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_{6} -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 Lm46;

for x, y, z being set

for S being Language

for D1, D2, D3 being RuleSet of S

for SQ1, SQ2 being b

z is m + n,SQ1 \/ SQ2,(D1 \/ D2) \/ D3 -derivable by Lm46;

theorem :: FOMODEL4:8

for m, n being Nat

for X, y, 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 Lm22;

for X, y, 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 Lm22;

theorem :: FOMODEL4:9

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 Lm12;

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 Lm12;

theorem :: FOMODEL4:10

theorem :: FOMODEL4:11

theorem :: FOMODEL4:12

registration

let S be Language;

let D1 be 0 -ranked 1 -ranked RuleSet of S;

let X be D1 -expanded set ;

for b_{1} being S, AllTermsOf S -interpreter-like Function st b_{1} = (S,X) -freeInterpreter holds

b_{1} is (X,D1) -termEq -respecting

end;
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 for S, AllTermsOf S -interpreter-like Function;

coherence for b

b

proof end;

definition

let S be Language;

let D be 0 -ranked RuleSet of S;

let X be D -expanded set ;

((S,X) -freeInterpreter) quotient ((X,D) -termEq) is Function ;

end;
let D be 0 -ranked RuleSet of S;

let X be D -expanded set ;

func D Henkin X -> Function equals :: FOMODEL4:def 64

((S,X) -freeInterpreter) quotient ((X,D) -termEq);

coherence ((S,X) -freeInterpreter) quotient ((X,D) -termEq);

((S,X) -freeInterpreter) quotient ((X,D) -termEq) is Function ;

:: deftheorem defines Henkin FOMODEL4:def 64 :

for S being Language

for D being 0 -ranked RuleSet of S

for X being b_{2} -expanded set holds D Henkin X = ((S,X) -freeInterpreter) quotient ((X,D) -termEq);

for S being Language

for D being 0 -ranked RuleSet of S

for X being b

registration

let S be Language;

let D be 0 -ranked RuleSet of S;

let X be D -expanded set ;

coherence

D Henkin X is OwnSymbolsOf S -defined ;

end;
let D be 0 -ranked RuleSet of S;

let X be D -expanded set ;

coherence

D Henkin X is OwnSymbolsOf S -defined ;

registration

let S be Language;

let D1 be 0 -ranked 1 -ranked RuleSet of S;

let X be D1 -expanded set ;

coherence

for b_{1} being Function st b_{1} = D1 Henkin X holds

b_{1} is S, Class ((X,D1) -termEq) -interpreter-like
;

end;
let D1 be 0 -ranked 1 -ranked RuleSet of S;

let X be D1 -expanded set ;

coherence

for b

b

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

end;
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;

registration

let S be Language;

let phi1, phi2 be wff string of S;

for b_{1} being set st b_{1} = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds

b_{1} is {(xnot phi1),(xnot phi2)},{(R#0 S)} \/ {(R#6 S)} -provable

end;
let phi1, phi2 be wff string of S;

cluster (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 -> {(xnot phi1),(xnot phi2)},{(R#0 S)} \/ {(R#6 S)} -provable for set ;

coherence for b

b

proof end;

registration

let S be Language;

for b_{1} being 0 -ranked RuleSet of S holds not b_{1} is empty
by Def62;

end;
cluster 0 -ranked -> non empty 0 -ranked for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

coherence for b

Lm50: for S being Language

for D1 being 0 -ranked 1 -ranked RuleSet of S

for X being b

for phi being 0wff string of S holds

( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )

proof end;

:: deftheorem defines -witnessed FOMODEL4:def 65 :

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 ) );

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 ) );

notation
end;

theorem :: FOMODEL4:13

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 ;

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 ;

definition

let S be Language;

let D be RuleSet of S;

let X be functional set ;

let phi be Element of ExFormulasOf S;

for b_{1} being set holds verum
;

coherence

( ( X \/ {phi} is D -consistent & (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 ) & ( ( not X \/ {phi} is D -consistent or not (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} ) implies X is set ) ) ;

end;
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 :Def66: :: FOMODEL4:def 66

X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} if ( X \/ {phi} is D -consistent & (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} )

otherwise X;

consistency X \/ {((((S -firstChar) . phi), the Element of (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)})))) -SymbolSubstIn (head phi))} if ( X \/ {phi} is D -consistent & (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} )

otherwise X;

for b

coherence

( ( X \/ {phi} is D -consistent & (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 ) & ( ( not X \/ {phi} is D -consistent or not (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} ) implies X is set ) ) ;

:: deftheorem Def66 defines AddAsWitnessTo FOMODEL4:def 66 :

for S being Language

for D being RuleSet of S

for X being functional set

for phi being Element of ExFormulasOf S holds

( ( X \/ {phi} is D -consistent & (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))} ) & ( ( not X \/ {phi} is D -consistent or not (LettersOf S) \ (SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ (X \/ {(head phi)}))) <> {} ) implies (D,phi) AddAsWitnessTo X = X ) );

for S being Language

for D being RuleSet of S

for X being functional set

for phi being Element of ExFormulasOf S holds

( ( X \/ {phi} is D -consistent & (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))} ) & ( ( not X \/ {phi} is D -consistent 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;

coherence

for b_{1} being set st b_{1} = X \ ((D,phi) AddAsWitnessTo X) holds

b_{1} is empty

end;
let D be RuleSet of S;

let X be functional set ;

let phi be Element of ExFormulasOf S;

coherence

for b

b

proof end;

registration

let S be Language;

let D be RuleSet of S;

let X be functional set ;

let phi be Element of ExFormulasOf S;

coherence

for b_{1} being set st b_{1} = ((D,phi) AddAsWitnessTo X) \ X holds

b_{1} is trivial

end;
let D be RuleSet of S;

let X be functional set ;

let phi be Element of ExFormulasOf S;

coherence

for b

b

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;

:: original: AddAsWitnessTo

redefine func (D,phi) AddAsWitnessTo X -> Subset of (X \/ (AllFormulasOf S));

coherence

(D,phi) AddAsWitnessTo X is Subset of (X \/ (AllFormulasOf S))

end;
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;

definition

let S be Language;

let D be RuleSet of S;

end;
let D be RuleSet of S;

attr D is Correct means :: FOMODEL4:def 67

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;

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;

:: deftheorem defines Correct FOMODEL4:def 67 :

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 );

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 );

Lm51: for X being set

for S being Language

for D being RuleSet of S holds

( X is D -consistent iff for Y being finite Subset of X holds Y is D -consistent )

proof end;

Lm52: for X being set

for S being Language

for D being RuleSet of S st R#0 S in D & X is S -covering & X is D -consistent holds

( X is S -mincover & X is D -expanded )

proof end;

Lm53: 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

X is D -consistent

proof end;

registration

let S be Language;

let t1, t2 be termal string of S;

coherence

for b_{1} being set st b_{1} = (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> holds

b_{1} is empty

end;
let t1, t2 be termal string of S;

coherence

for b

b

proof end;

Lm54: for U being non empty set

for S being Language

for t1, t2 being termal string of S

for I being b

( I -AtomicEval ((<*(TheEqSymbOf S)*> ^ t1) ^ t2) = 1 iff (I -TermEval) . t1 = (I -TermEval) . t2 )

proof end;

:: deftheorem Def68 defines Correct FOMODEL4:def 68 :

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 );

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 );

Lm55: for S being Language holds R#0 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#0 S holds

b_{1} is Correct
by Lm55;

end;
coherence

for b

b

registration

let S be Language;

ex b_{1} being Rule of S st b_{1} is Correct

end;
cluster Relation-like bool (S -sequents) -defined bool (S -sequents) -valued Function-like total quasi_total Correct for Element of Funcs ((bool (S -sequents)),(bool (S -sequents)));

existence ex b

proof end;

Lm56: for S being Language holds R#1 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#1 S holds

b_{1} is Correct
by Lm56;

end;
coherence

for b

b

Lm57: for S being Language holds R#2 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#2 S holds

b_{1} is Correct
by Lm57;

end;
coherence

for b

b

Lm58: for S being Language holds R#3a S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#3a S holds

b_{1} is Correct
by Lm58;

end;
coherence

for b

b

Lm59: for S being Language holds R#3b S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#3b S holds

b_{1} is Correct
by Lm59;

end;
coherence

for b

b

Lm60: for S being Language holds R#3d S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#3d S holds

b_{1} is Correct
by Lm60;

end;
coherence

for b

b

Lm61: for S being Language holds R#3e S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#3e S holds

b_{1} is Correct
by Lm61;

end;
coherence

for b

b

Lm62: for S being Language holds R#4 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#4 S holds

b_{1} is Correct
by Lm62;

end;
coherence

for b

b

Lm63: for S being Language holds R#5 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#5 S holds

b_{1} is Correct
by Lm63;

end;
coherence

for b

b

Lm64: for S being Language holds R#6 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#6 S holds

b_{1} is Correct
by Lm64;

end;
coherence

for b

b

Lm65: for S being Language holds R#7 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#7 S holds

b_{1} is Correct
by Lm65;

end;
coherence

for b

b

Lm66: for S being Language holds R#8 S is Correct

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#8 S holds

b_{1} is Correct
by Lm66;

end;
coherence

for b

b

theorem Th14: :: FOMODEL4:14

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

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;

coherence

for b_{1} being RuleSet of S st b_{1} = {R} holds

b_{1} is Correct

end;
let R be Correct Rule of S;

coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being RuleSet of S st b_{1} = S -rules holds

b_{1} is Correct

end;
coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being Rule of S st b_{1} = R#9 S holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

registration

let S be Language;

let H be S -premises-like set ;

let phi be wff string of S;

coherence

for b_{1} being set st b_{1} = [H,phi] null 1 holds

b_{1} is 1,{[H,(xnot (xnot phi))]},{(R#9 S)} -derivable

end;
let H be S -premises-like set ;

let phi be wff string of S;

coherence

for b

b

proof end;

registration

let X be set ;

let S be Language;

ex b_{1} being 0 -wff string of S st b_{1} is X -implied

end;
let S be Language;

cluster Relation-like NAT -defined AtomicFormulaSymbolsOf S -valued non empty non zero Function-like finite FinSequence-like FinSubsequence-like countable V220() 0wff 0 -wff wff X -implied for Element of ((AllSymbolsOf S) *) \ {{}};

existence ex b

proof end;

registration

let X be set ;

let S be Language;

ex b_{1} being wff string of S st b_{1} is X -implied

end;
let S be Language;

cluster Relation-like NAT -defined non empty non zero Function-like finite FinSequence-like FinSubsequence-like countable V220() wff X -implied for Element of ((AllSymbolsOf S) *) \ {{}};

existence ex b

proof end;

registration

let S be Language;

let X be set ;

let phi be wff X -implied string of S;

coherence

for b_{1} being wff string of S st b_{1} = xnot (xnot phi) holds

b_{1} is X -implied

end;
let X be set ;

let phi be wff X -implied string of S;

coherence

for b

b

proof end;

:: deftheorem defines -provable FOMODEL4:def 69 :

for X being set

for S being Language

for phi being wff string of S holds

( phi is X -provable iff phi is X,{(R#9 S)} \/ (S -rules) -provable );

for X being set

for S being Language

for phi being wff string of S holds

( phi is X -provable iff phi is X,{(R#9 S)} \/ (S -rules) -provable );

registration

let S be Language;

let r1, r2 be isotone Rule of S;

coherence

for b_{1} being RuleSet of S st b_{1} = {r1,r2} holds

b_{1} is isotone

end;
let r1, r2 be isotone Rule of S;

coherence

for b

b

proof end;

registration

let S be Language;

let r1, r2, r3, r4 be isotone Rule of S;

coherence

for b_{1} being RuleSet of S st b_{1} = {r1,r2,r3,r4} holds

b_{1} is isotone

end;
let r1, r2, r3, r4 be isotone Rule of S;

coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being RuleSet of S st b_{1} = S -rules holds

b_{1} is isotone

end;
coherence

for b

b

proof end;

registration

let S be Language;

ex b_{1} being isotone RuleSet of S st b_{1} is Correct

end;
cluster functional isotone Correct for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

existence ex b

proof end;

registration

let S be Language;

ex b_{1} being isotone Correct RuleSet of S st b_{1} is 2 -ranked

end;
cluster functional isotone 2 -ranked Correct for Element of bool (Funcs ((bool (S -sequents)),(bool (S -sequents))));

existence ex b

proof end;

theorem :: FOMODEL4:15

theorem Th16: :: FOMODEL4:16

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_{3} -expanded set st R#1 S in D1 & R#4 S in D1 & R#6 S in D1 & R#7 S in D1 & R#8 S in D1 & X is S -mincover & X is S -witnessed holds

( (D1 Henkin X) -TruthEval psi = 1 iff psi in X )

for psi being wff string of S

for D1 being 0 -ranked 1 -ranked RuleSet of S

for X being b

( (D1 Henkin X) -TruthEval psi = 1 iff psi in X )

proof end;

definition

let S be Language;

let D be RuleSet of S;

let X be set ;

end;
let D be RuleSet of S;

let X be set ;

attr X is D -inconsistentStrong means :: FOMODEL4:def 70

for phi being wff string of S holds phi is X,D -provable ;

for phi being wff string of S holds phi is X,D -provable ;

:: deftheorem defines -inconsistentStrong FOMODEL4:def 70 :

for S being Language

for D being RuleSet of S

for X being set holds

( X is D -inconsistentStrong iff for phi being wff string of S holds phi is X,D -provable );

for S being Language

for D being RuleSet of S

for X being set holds

( X is D -inconsistentStrong iff for phi being wff string of S holds phi is X,D -provable );

notation

let S be Language;

let D be RuleSet of S;

let X be set ;

antonym D -consistentWeak X for D -inconsistentStrong ;

end;
let D be RuleSet of S;

let X be set ;

antonym D -consistentWeak X for D -inconsistentStrong ;

definition

let X be functional set ;

let S be Language;

let D be RuleSet of S;

let num be sequence of (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));

ex b_{1} being sequence of (bool (X \/ (AllFormulasOf S))) st

( b_{1} . 0 = X & ( for mm being Element of NAT holds b_{1} . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b_{1} . mm) ) )

for b_{1}, b_{2} being sequence of (bool (X \/ (AllFormulasOf S))) st b_{1} . 0 = X & ( for mm being Element of NAT holds b_{1} . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b_{1} . mm) ) & b_{2} . 0 = X & ( for mm being Element of NAT holds b_{2} . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b_{2} . mm) ) holds

b_{1} = b_{2}

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (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 -> sequence of (bool (X \/ (AllFormulasOf S))) means :Def71: :: FOMODEL4:def 71

( it . 0 = X & ( for mm being Element of NAT holds it . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (it . mm) ) );

existence ( it . 0 = X & ( for mm being Element of NAT holds it . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (it . mm) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def71 defines AddWitnessesTo FOMODEL4:def 71 :

for X being functional set

for S being Language

for D being RuleSet of S

for num being sequence of (ExFormulasOf S)

for b_{5} being sequence of (bool (X \/ (AllFormulasOf S))) holds

( b_{5} = (D,num) AddWitnessesTo X iff ( b_{5} . 0 = X & ( for mm being Element of NAT holds b_{5} . (mm + 1) = (D,(num . mm)) AddAsWitnessTo (b_{5} . mm) ) ) );

for X being functional set

for S being Language

for D being RuleSet of S

for num being sequence of (ExFormulasOf S)

for b

( b

notation

let X be functional set ;

let S be Language;

let D be RuleSet of S;

let num be sequence of (ExFormulasOf S);

synonym (D,num) addw X for (D,num) AddWitnessesTo X;

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (ExFormulasOf S);

synonym (D,num) addw X for (D,num) AddWitnessesTo X;

theorem Th17: :: 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 sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds

( ((D,num) addw X) . k c= ((D,num) addw X) . (k + m) & (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . m) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & ((D,num) addw X) . m is D -consistent )

for S being Language

for D being RuleSet of S

for X being functional set

for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds

( ((D,num) addw X) . k c= ((D,num) addw X) . (k + m) & (LettersOf S) \ (SymbolsOf ((((D,num) addw X) . m) /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & ((D,num) addw X) . m is D -consistent )

proof end;

Lm67: for S being Language

for D being RuleSet of S

for X being functional set

for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds

rng ((D,num) addw X) is c=directed

proof end;

definition

let X be functional set ;

let S be Language;

let D be RuleSet of S;

let num be sequence of (ExFormulasOf S);

union (rng ((D,num) AddWitnessesTo X)) is Subset of (X \/ (AllFormulasOf S))

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (ExFormulasOf S);

func X WithWitnessesFrom (D,num) -> Subset of (X \/ (AllFormulasOf S)) equals :: FOMODEL4:def 72

union (rng ((D,num) AddWitnessesTo X));

coherence union (rng ((D,num) AddWitnessesTo X));

union (rng ((D,num) AddWitnessesTo X)) is Subset of (X \/ (AllFormulasOf S))

proof 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 sequence of (ExFormulasOf S) holds X WithWitnessesFrom (D,num) = union (rng ((D,num) AddWitnessesTo X));

for X being functional set

for S being Language

for D being RuleSet of S

for num being sequence of (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 sequence of (ExFormulasOf S);

synonym X addw (D,num) for X WithWitnessesFrom (D,num);

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (ExFormulasOf S);

synonym X addw (D,num) for X WithWitnessesFrom (D,num);

registration

let X be functional set ;

let S be Language;

let D be RuleSet of S;

let num be sequence of (ExFormulasOf S);

coherence

for b_{1} being set st b_{1} = X \ (X addw (D,num)) holds

b_{1} is empty

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (ExFormulasOf S);

coherence

for b

b

proof end;

Lm68: for S being Language

for D being RuleSet of S

for X being functional set

for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#2 S in D & R#5 S in D & R#8 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D -consistent holds

X addw (D,num) is D -consistent

proof end;

theorem Th18: :: FOMODEL4:18

for Z being set

for S being Language

for D being RuleSet of S

for X being functional set

for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S holds

Z is S -witnessed

for S being Language

for D being RuleSet of S

for X being functional set

for num being sequence of (ExFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & R#2 S in D & R#5 S in D & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X addw (D,num) c= Z & Z is D -consistent & rng num = ExFormulasOf S holds

Z is S -witnessed

proof end;

::# constructions for countable languages

::# Consistently maximizing a set of formulas (Lindenbaum's lemma)

::# of a countable language

::# Consistently maximizing a set of formulas (Lindenbaum's lemma)

::# of a countable language

definition

let X be set ;

let S be Language;

let D be RuleSet of S;

let phi be Element of AllFormulasOf S;

for b_{1} being object holds verum
;

coherence

( ( not xnot phi is X,D -provable implies X \/ {phi} is object ) & ( xnot phi is X,D -provable implies X \/ {(xnot phi)} is object ) ) ;

end;
let S be Language;

let D be RuleSet of S;

let phi be Element of AllFormulasOf S;

func (D,phi) AddFormulaTo X -> object equals :Def73: :: FOMODEL4:def 73

X \/ {phi} if not xnot phi is X,D -provable

otherwise X \/ {(xnot phi)};

consistency X \/ {phi} if not xnot phi is X,D -provable

otherwise X \/ {(xnot phi)};

for b

coherence

( ( not xnot phi is X,D -provable implies X \/ {phi} is object ) & ( xnot phi is X,D -provable implies X \/ {(xnot phi)} is object ) ) ;

:: deftheorem Def73 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)} ) );

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))

end;
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;

registration

let X be set ;

let S be Language;

let D be RuleSet of S;

let phi be Element of AllFormulasOf S;

coherence

for b_{1} being set st b_{1} = X \ ((D,phi) AddFormulaTo X) holds

b_{1} is empty

end;
let S be Language;

let D be RuleSet of S;

let phi be Element of AllFormulasOf S;

coherence

for b

b

proof end;

definition

let X be set ;

let S be Language;

let D be RuleSet of S;

let num be sequence of (AllFormulasOf S);

set SS = AllSymbolsOf S;

set FF = AllFormulasOf S;

set Y = X \/ (AllFormulasOf S);

set DD = bool (X \/ (AllFormulasOf S));

ex b_{1} being sequence of (bool (X \/ (AllFormulasOf S))) st

( b_{1} . 0 = X & ( for m being Nat holds b_{1} . (m + 1) = (D,(num . m)) AddFormulaTo (b_{1} . m) ) )

for b_{1}, b_{2} being sequence of (bool (X \/ (AllFormulasOf S))) st b_{1} . 0 = X & ( for m being Nat holds b_{1} . (m + 1) = (D,(num . m)) AddFormulaTo (b_{1} . m) ) & b_{2} . 0 = X & ( for m being Nat holds b_{2} . (m + 1) = (D,(num . m)) AddFormulaTo (b_{2} . m) ) holds

b_{1} = b_{2}

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (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 -> sequence of (bool (X \/ (AllFormulasOf S))) means :Def74: :: FOMODEL4:def 74

( it . 0 = X & ( for m being Nat holds it . (m + 1) = (D,(num . m)) AddFormulaTo (it . m) ) );

existence ( it . 0 = X & ( for m being Nat holds it . (m + 1) = (D,(num . m)) AddFormulaTo (it . m) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def74 defines AddFormulasTo FOMODEL4:def 74 :

for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (AllFormulasOf S)

for b_{5} being sequence of (bool (X \/ (AllFormulasOf S))) holds

( b_{5} = (D,num) AddFormulasTo X iff ( b_{5} . 0 = X & ( for m being Nat holds b_{5} . (m + 1) = (D,(num . m)) AddFormulaTo (b_{5} . m) ) ) );

for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (AllFormulasOf S)

for b

( b

definition

let X be set ;

let S be Language;

let D be RuleSet of S;

let num be sequence of (AllFormulasOf S);

union (rng ((D,num) AddFormulasTo X)) is Subset of (X \/ (AllFormulasOf S))

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (AllFormulasOf S);

func (D,num) CompletionOf X -> Subset of (X \/ (AllFormulasOf S)) equals :: FOMODEL4:def 75

union (rng ((D,num) AddFormulasTo X));

coherence union (rng ((D,num) AddFormulasTo X));

union (rng ((D,num) AddFormulasTo X)) is Subset of (X \/ (AllFormulasOf S))

proof end;

:: deftheorem defines CompletionOf FOMODEL4:def 75 :

for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (AllFormulasOf S) holds (D,num) CompletionOf X = union (rng ((D,num) AddFormulasTo X));

for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (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 sequence of (AllFormulasOf S);

coherence

for b_{1} being set st b_{1} = X \ ((D,num) CompletionOf X) holds

b_{1} is empty

end;
let S be Language;

let D be RuleSet of S;

let num be sequence of (AllFormulasOf S);

coherence

for b

b

proof end;

Lm69: for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (AllFormulasOf S) st rng num = AllFormulasOf S holds

(D,num) CompletionOf X is S -covering

proof end;

definition

let S be Language;

{ [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } is Function

end;
func S -diagFormula -> Function equals :: FOMODEL4:def 76

{ [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } ;

coherence { [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } ;

{ [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } is Function

proof end;

:: deftheorem defines -diagFormula FOMODEL4:def 76 :

for S being Language holds S -diagFormula = { [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } ;

for S being Language holds S -diagFormula = { [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } ;

Lm70: for S being Language

for t being termal string of S holds

( (S -diagFormula) . t = (<*(TheEqSymbOf S)*> ^ t) ^ t & S -diagFormula is Function of (AllTermsOf S),(AtomicFormulasOf S) & S -diagFormula is one-to-one )

proof end;

definition

let S be Language;

:: original: -diagFormula

redefine func S -diagFormula -> Function of (AllTermsOf S),(AtomicFormulasOf S);

coherence

S -diagFormula is Function of (AllTermsOf S),(AtomicFormulasOf S) by Lm70;

end;
:: original: -diagFormula

redefine func S -diagFormula -> Function of (AllTermsOf S),(AtomicFormulasOf S);

coherence

S -diagFormula is Function of (AllTermsOf S),(AtomicFormulasOf S) by Lm70;

registration

let S be Language;

coherence

for b_{1} being Function st b_{1} = S -diagFormula holds

b_{1} is one-to-one
by Lm70;

end;
coherence

for b

b

Lm71: 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 & R#1 S in D & R#8 S in D & phi is X,D -provable & X is D -consistent holds

X \/ {phi} is D -consistent

proof end;

Lm72: for k, m being Nat

for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds

( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent )

proof end;

Lm73: for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds

rng ((D,num) AddFormulasTo X) is c=directed

proof end;

Lm74: for X being set

for S being Language

for D being RuleSet of S

for num being sequence of (AllFormulasOf S) st D is isotone & R#1 S in D & R#8 S in D & X is D -consistent holds

(D,num) CompletionOf X is D -consistent

proof end;

Lm75: for S being Language

for D2 being 2 -ranked RuleSet of S

for X being functional set st AllFormulasOf S is countable & (LettersOf S) \ (SymbolsOf (X /\ (((AllSymbolsOf S) *) \ {{}}))) is infinite & X is D2 -consistent & D2 is isotone holds

ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied

proof end;

Lm76: for S being Language

for X being functional set

for D2 being 2 -ranked RuleSet of S st X is finite & AllFormulasOf S is countable & X is D2 -consistent & D2 is isotone holds

ex U being non empty countable set ex I being Element of U -InterpretersOf S st X is I -satisfied

proof end;

theorem Th19: :: FOMODEL4:19

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 & Z is D -consistent & Z c= AllFormulasOf S holds

ex U being non empty countable set ex I being Element of U -InterpretersOf S st Z is I -satisfied

for S being countable Language

for D being RuleSet of S st D is 2 -ranked & D is isotone & D is Correct & Z is D -consistent & Z c= AllFormulasOf S holds

ex U being non empty countable set ex I being Element of U -InterpretersOf S st Z is I -satisfied

proof end;

Lm77: 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:20

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

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;

::# countable downward Lowenheim-Skolem theorem ("weak version", Skolem 1922)

::# cfr. Ebbinghaus-Flum-Thomas, theorem VI.1.1

::# cfr. Ebbinghaus-Flum-Thomas, theorem VI.1.1

theorem :: FOMODEL4:21

for U being non empty set

for S2 being Language

for X2 being countable Subset of (AllFormulasOf S2)

for I2 being Element of U -InterpretersOf S2 st X2 is I2 -satisfied holds

ex U1 being non empty countable set ex I1 being Element of U1 -InterpretersOf S2 st X2 is I1 -satisfied

for S2 being Language

for X2 being countable Subset of (AllFormulasOf S2)

for I2 being Element of U -InterpretersOf S2 st X2 is I2 -satisfied holds

ex U1 being non empty countable set ex I1 being Element of U1 -InterpretersOf S2 st X2 is I1 -satisfied

proof end;

::#Definitions and auxiliary lemmas