let S be Language; :: thesis: 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
let D be RuleSet of S; :: thesis: ( ( for R being Rule of S st R in D holds
R is Correct ) implies D is Correct )
set Q = S -sequents ;
set O = OneStep D;
{} null S is S -correct ;
then reconsider e = {} null (S -sequents) as S -correct Subset of (S -sequents) ;
A1: dom (OneStep D) = bool (S -sequents) by FUNCT_2:def 1;
reconsider RO = rng (OneStep D) as Subset of (bool (S -sequents)) by RELAT_1:def 19;
assume A2: for R being Rule of S st R in D holds
R is Correct ; :: thesis: D is Correct
defpred S₁[ Nat] means for X being S -correct Subset of (S -sequents) holds (($1,D) -derivables) . X is S -correct ;
A3: S₁[ 0 ]

proof

set f = (0,D) -derivables ;
A4: (0,D) -derivables = id (field (OneStep D)) by FUNCT_7:68
.= id ((bool (S -sequents)) \/ RO) by A1
.= id (bool (S -sequents)) ;
let X be S -correct Subset of (S -sequents); :: thesis: ((0,D) -derivables) . X is S -correct
((id (bool (S -sequents))) . X) \+\ X = {} ;
hence ((0,D) -derivables) . X is S -correct by A4, FOMODEL0:29; :: thesis: verum

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
let X be S -correct Subset of (S -sequents); :: thesis: (((n + 1),D) -derivables) . X is S -correct
set DM = ((n + 1),D) -derivables ;
set Dm = (n,D) -derivables ;
A7: dom ((n,D) -derivables) = bool (S -sequents) by FUNCT_2:def 1;
reconsider oldSeqs = ((n,D) -derivables) . X as S -correct Subset of (S -sequents) by A6;
A8: ((n + 1),D) -derivables = (OneStep D) * ((n,D) -derivables) by FUNCT_7:71;

now :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S
for H being b₂ -satisfied set
for phi being wff string of S st [H,phi] in (((n + 1),D) -derivables) . X holds
I -TruthEval phi = 1

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S
for H being b₁ -satisfied set
for phi being wff string of S st [H,phi] in (((n + 1),D) -derivables) . X holds
I -TruthEval phi = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: for H being I -satisfied set
for phi being wff string of S st [H,phi] in (((n + 1),D) -derivables) . X holds
I -TruthEval phi = 1
let H be I -satisfied set ; :: thesis: for phi being wff string of S st [H,phi] in (((n + 1),D) -derivables) . X holds
I -TruthEval phi = 1
let phi be wff string of S; :: thesis: ( [H,phi] in (((n + 1),D) -derivables) . X implies I -TruthEval phi = 1 )
assume A9: [H,phi] in (((n + 1),D) -derivables) . X ; :: thesis: I -TruthEval phi = 1
set Fam = { (R .: {oldSeqs}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ;
(((n + 1),D) -derivables) . X = (OneStep D) . oldSeqs by A7, A8, FUNCT_1:13
.= union (union { (R .: {oldSeqs}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ) by Lm6 ;
then consider x being set such that
A10: ( [H,phi] in x & x in union { (R .: {oldSeqs}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ) by A9, TARSKI:def 4;
consider y being set such that
A11: ( x in y & y in { (R .: {oldSeqs}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D } ) by A10, TARSKI:def 4;
consider R being Subset of [:(bool (S -sequents)),(bool (S -sequents)):] such that
A12: ( y = R .: {oldSeqs} & R in D ) by A11;
reconsider RR = R as Correct Rule of S by A2, A12;
reconsider newSeqs = RR . oldSeqs as S -correct Subset of (S -sequents) by Def69;
dom RR = bool (S -sequents) by FUNCT_2:def 1;
then ( y = Im (R,oldSeqs) & Im (RR,oldSeqs) = {(RR . oldSeqs)} ) by A12, FUNCT_1:59;
then [H,phi] in newSeqs by A10, A11, TARSKI:def 1;
hence I -TruthEval phi = 1 by FOMODEL2:def 44; :: thesis: verum

end;

hence (((n + 1),D) -derivables) . X is S -correct by FOMODEL2:def 44; :: thesis: verum

end;

A13: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A5);

now :: thesis: 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

let phi be wff string of S; :: thesis: 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
let X be set ; :: thesis: ( phi is X,D -provable implies for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1 )
assume phi is X,D -provable ; :: thesis: for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1
then consider H being set , m being Nat such that
A14: ( H c= X & [H,phi] is m, {} ,D -derivable ) by Def62;
reconsider HH = H as Subset of X by A14;
reconsider seqt = [H,phi] as Element of S -sequents by Def2, A14;
reconsider okSeqs = ((m,D) -derivables) . e as S -correct Subset of (S -sequents) by A13;

hereby :: thesis: verum

let U be non empty set ; :: thesis: for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: ( X is I -satisfied implies I -TruthEval phi = 1 )
assume X is I -satisfied ; :: thesis: I -TruthEval phi = 1
then reconsider XX = X as I -satisfied set ;
reconsider HHH = HH as I -satisfied Subset of XX ;
[HHH,phi] in okSeqs by A14, Def7;
hence I -TruthEval phi = 1 by FOMODEL2:def 44; :: thesis: verum

end;

end;

hence D is Correct by Def68; :: thesis: verum