let k, m be 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 )
let X be 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 )
let S be 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 )
let D be 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 )
set FF = AllFormulasOf S;
let num be sequence of (AllFormulasOf S); ( D is isotone & R#1 S in D & R#8 S in D & X is D -consistent implies ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent ) )
set f = (D,num) AddFormulasTo X;
assume A1:
( D is isotone & R#1 S in D & R#8 S in D )
; ( not X is D -consistent or ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent ) )
assume A2:
X is D -consistent
; ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent )
defpred S1[ Nat] means ( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + $1) & ((D,num) AddFormulasTo X) . $1 is D -consistent );
A3:
S1[ 0 ]
by A2, Def74;
A4:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
set fkn1 = (
D,
(num . (k + n)))
AddFormulaTo (((D,num) AddFormulasTo X) . (k + n));
set fkn =
((D,num) AddFormulasTo X) . (k + n);
assume A5:
S1[
n]
;
S1[n + 1]
A6:
(((D,num) AddFormulasTo X) . (k + n)) \ ((D,(num . (k + n))) AddFormulaTo (((D,num) AddFormulasTo X) . (k + n))) = {}
;
((D,num) AddFormulasTo X) . (k + (n + 1)) =
((D,num) AddFormulasTo X) . ((k + n) + 1)
.=
(
D,
(num . (k + n)))
AddFormulaTo (((D,num) AddFormulasTo X) . (k + n))
by Def74
;
then
((D,num) AddFormulasTo X) . (k + n) c= ((D,num) AddFormulasTo X) . (k + (n + 1))
by A6, XBOOLE_1:37;
hence
((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + (n + 1))
by XBOOLE_1:1, A5;
((D,num) AddFormulasTo X) . (n + 1) is D -consistent
reconsider phii =
num . n as
Element of
AllFormulasOf S ;
reconsider phi =
phii as
wff string of
S ;
reconsider psi =
xnot phi as
wff string of
S ;
reconsider psii =
psi as
Element of
AllFormulasOf S by FOMODEL2:16;
set fn =
((D,num) AddFormulasTo X) . n;
set fN = (
D,
(num . n))
AddFormulaTo (((D,num) AddFormulasTo X) . n);
defpred S2[]
means xnot phii is
((D,num) AddFormulasTo X) . n,
D -provable ;
A7:
((D,num) AddFormulasTo X) . (n + 1) = (
D,
(num . n))
AddFormulaTo (((D,num) AddFormulasTo X) . n)
by Def74;
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A3, A4);
hence
( ((D,num) AddFormulasTo X) . k c= ((D,num) AddFormulasTo X) . (k + m) & ((D,num) AddFormulasTo X) . m is D -consistent )
; verum