let U be non empty set ; for S being Language
for l being literal Element of S
for psi being wff string of S
for tt being Element of AllTermsOf S holds
( Depth ((l,tt) SubstIn psi) = Depth psi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi ) )
let S be Language; for l being literal Element of S
for psi being wff string of S
for tt being Element of AllTermsOf S holds
( Depth ((l,tt) SubstIn psi) = Depth psi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi ) )
let l be literal Element of S; for psi being wff string of S
for tt being Element of AllTermsOf S holds
( Depth ((l,tt) SubstIn psi) = Depth psi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi ) )
let psi be wff string of S; for tt being Element of AllTermsOf S holds
( Depth ((l,tt) SubstIn psi) = Depth psi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi ) )
let tt be Element of AllTermsOf S; ( Depth ((l,tt) SubstIn psi) = Depth psi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi ) )
set II = U -InterpretersOf S;
set TT = AllTermsOf S;
set AF = AtomicFormulasOf S;
set F = S -firstChar ;
set L = LettersOf S;
set f0 = l AtomicSubst tt;
set f1 = l Subst1 tt;
set f4 = (l,tt) Subst4 (l Subst1 tt);
set FF = AllFormulasOf S;
set N = TheNorSymbOf S;
defpred S1[ Nat] means for phi being wff string of S st Depth phi <= $1 holds
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) );
tt null {} is {} \/ (rng tt) -valued FinSequence
;
then
tt is FinSequence of rng tt
by FOMODEL0:26;
then reconsider ttt = tt as Element of (rng tt) * ;
A1:
S1[ 0 ]
proof
let phi be
wff string of
S;
( Depth phi <= 0 implies ( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) ) )
set d =
Depth phi;
set IT = (
l,
tt)
SubstIn phi;
assume A2:
Depth phi <= 0
;
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) )
reconsider phii =
phi as
0wff string of
S by A2;
Depth ((l,tt) SubstIn phii) = 0
;
hence
Depth ((l,tt) SubstIn phi) = Depth phi
;
for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi
let I be
Element of
U -InterpretersOf S;
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi
set u =
(I -TermEval) . tt;
set J = (
l,
((I -TermEval) . tt))
ReassignIn I;
I -TruthEval ((l,tt) AtomicSubst phii) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii
by Th8;
hence
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi
;
verum
end;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
let phi be
wff string of
S;
( Depth phi <= n + 1 implies ( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) ) )
reconsider X =
(LettersOf S) \ (((rng tt) \/ (rng (head phi))) \/ {l}) as
infinite Subset of
(LettersOf S) ;
reconsider XX =
X as non
empty Subset of
(LettersOf S) ;
set ll2 = the
Element of
X;
reconsider l2 = the
Element of
X as
literal Element of
S by TARSKI:def 3;
assume C0:
Depth phi <= n + 1
;
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) )
not
l2 in ((rng tt) \/ (rng (head phi))) \/ {l}
by XBOOLE_0:def 5;
then
( not
l2 in (rng tt) \/ (rng (head phi)) & not
l2 in {l} )
by XBOOLE_0:def 3;
then A5:
(
l2 <> l & not
l2 in rng tt & not
l2 in rng (head phi) )
by XBOOLE_0:def 3, TARSKI:def 1;
per cases
( phi is exal or ( not phi is exal & not phi is 0wff ) or phi is 0wff )
;
suppose
phi is
exal
;
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) )then reconsider phii =
phi as non
0wff wff exal string of
S ;
consider m being
Nat such that A6:
Depth phii = m + 1
by NAT_1:6;
reconsider mm =
m as
Element of
NAT by ORDINAL1:def 12;
D1:
m <= n
by XREAL_1:8, C0, A6;
reconsider phii =
phii as non
0wff m + 1
-wff exal string of
S by A6, FOMODEL2:def 31;
set IT = (
l,
tt)
SubstIn phii;
set d =
Depth phii;
reconsider l1 =
(S -firstChar) . phii as
literal Element of
S ;
reconsider phi1 =
head phii as
Element of
AllFormulasOf S by FOMODEL2:16;
set d1 =
Depth phi1;
reconsider phi2 =
tail phii as
empty set ;
reconsider psi = (
l1,
l2)
-SymbolSubstIn phi as
m + 1
-wff string of
S ;
reconsider psi1 = (
l1,
l2)
-SymbolSubstIn (head phii) as
m -wff string of
S ;
(Depth psi1) \+\ (Depth phi1) = {}
;
then A7:
Depth psi1 = Depth phi1
by FOMODEL0:29;
reconsider Phi1 = (
l,
tt)
SubstIn psi1 as
wff string of
S ;
A8:
phii =
(<*l1*> ^ phi1) ^ phi2
by FOMODEL2:23
.=
<*l1*> ^ phi1
;
Depth phi1 <= m
by FOMODEL2:def 31;
then A9:
Depth phi1 <= n
by XXREAL_0:2, D1;
then A10:
Depth Phi1 = Depth (head phii)
by A4, A7;
reconsider m1 =
m - (Depth phi1) as
Nat ;
reconsider new1 = (
l,
tt)
SubstIn phi1 as
wff string of
S ;
set d11 =
Depth new1;
A11:
(
l,
tt)
SubstIn phii = (
l,
tt,
m,
(((l,tt) Subst4 (l Subst1 tt)) . mm))
Subst2 phii
by A6, Lm44;
per cases
( l1 <> l or l1 = l )
;
suppose
l1 <> l
;
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) )then A12: (
l,
tt)
SubstIn phii =
<*l2*> ^ ((((l,tt) Subst4 (l Subst1 tt)) . mm) . ((l1,l2) -SymbolSubstIn phi1))
by A6, Def20, A11
.=
<*l2*> ^ ((l,tt) SubstIn psi1)
by Lm46
;
then Depth ((l,tt) SubstIn phii) =
(Depth phi1) + 1
by A10, FOMODEL2:17
.=
Depth phi
by A8, FOMODEL2:17
;
hence
Depth ((l,tt) SubstIn phi) = Depth phi
;
for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval philet I be
Element of
U -InterpretersOf S;
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phiset tu =
(I -TermEval) . tt;
set It = (
l,
((I -TermEval) . tt))
ReassignIn I;
(
I -TruthEval ((l,tt) SubstIn phii) = 1 iff
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 )
proof
hereby ( ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 implies I -TruthEval ((l,tt) SubstIn phii) = 1 )
assume
I -TruthEval ((l,tt) SubstIn phii) = 1
;
1 = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phiithen consider u being
Element of
U such that A13:
((l2,u) ReassignIn I) -TruthEval Phi1 = 1
by A12, FOMODEL2:19;
set I2 = (
l2,
u)
ReassignIn I;
1 =
((l,((((l2,u) ReassignIn I) -TermEval) . tt)) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1
by A13, A7, A9, A4
.=
((l,((I -TermEval) . tt)) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1
by A5, FOMODEL2:25
.=
((l2,u) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval psi1
by A5, FOMODEL0:43
.=
((l1,u) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval (head phii)
by A5, Th9
;
hence
1
= ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii
by A8, FOMODEL2:19;
verum
end;
assume
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1
;
I -TruthEval ((l,tt) SubstIn phii) = 1
then consider u1 being
Element of
U such that A14:
((l1,u1) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval (head phii) = 1
by A8, FOMODEL2:19;
1 =
((l2,u1) ReassignIn ((l,((I -TermEval) . tt)) ReassignIn I)) -TruthEval psi1
by A14, Th9, A5
.=
((l,((I -TermEval) . tt)) ReassignIn ((l2,u1) ReassignIn I)) -TruthEval psi1
by FOMODEL0:43, A5
.=
((l,((((l2,u1) ReassignIn I) -TermEval) . tt)) ReassignIn ((l2,u1) ReassignIn I)) -TruthEval psi1
by FOMODEL2:25, A5
.=
((l2,u1) ReassignIn I) -TruthEval Phi1
by A7, A9, A4
;
hence
I -TruthEval ((l,tt) SubstIn phii) = 1
by A12, FOMODEL2:19;
verum
end; then
(
I -TruthEval ((l,tt) SubstIn phii) = 1 iff not
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 0 )
by FOMODEL0:39;
hence
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi
by FOMODEL0:39;
verum end; suppose A15:
l1 = l
;
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) )then A16:
phi = (
l,
tt)
SubstIn phii
by Lm45;
thus
Depth ((l,tt) SubstIn phi) = Depth phi
by A15, Lm45;
for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval philet I be
Element of
U -InterpretersOf S;
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phiset tu =
(I -TermEval) . tt;
set It = (
l,
((I -TermEval) . tt))
ReassignIn I;
(
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 iff
I -TruthEval phii = 1 )
then
(
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi = 1 iff not
I -TruthEval phi = 0 )
by FOMODEL0:39;
hence
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi
by A16, FOMODEL0:39;
verum end; end; end; suppose
( not
phi is
exal & not
phi is
0wff )
;
( Depth ((l,tt) SubstIn phi) = Depth phi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi ) )then reconsider phii =
phi as non
0wff wff non
exal string of
S ;
set IT = (
l,
tt)
SubstIn phii;
set d =
Depth phii;
consider m being
Nat such that A19:
Depth phii = m + 1
by NAT_1:6;
W1:
(m + 1) + (- 1) <= (n + 1) - 1
by XREAL_1:8, C0, A19;
reconsider mm =
m as
Element of
NAT by ORDINAL1:def 12;
reconsider phii =
phii as non
0wff m + 1
-wff non
exal string of
S by A19, FOMODEL2:def 31;
reconsider phi1 =
head phii,
phi2 =
tail phii as
Element of
AllFormulasOf S by FOMODEL2:16;
set d1 =
Depth phi1;
set d2 =
Depth phi2;
(
((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {} &
phii = (<*((S -firstChar) . phii)*> ^ phi1) ^ phi2 )
by FOMODEL2:23;
then A20:
phii = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
by FOMODEL0:29;
D2:
(
Depth phi1 <= m &
Depth phi2 <= m )
by FOMODEL2:def 31;
reconsider m1 =
m - (Depth phi1),
m2 =
m - (Depth phi2) as
Nat ;
reconsider new1 = (
l,
tt)
SubstIn phi1,
new2 = (
l,
tt)
SubstIn phi2 as
wff string of
S ;
set d11 =
Depth new1;
set d22 =
Depth new2;
A21:
(
Depth phi1 <= n &
Depth phi2 <= n )
by W1, D2, XXREAL_0:2;
A22: (
l,
tt)
SubstIn phii =
(
l,
tt,
m,
(((l,tt) Subst4 (l Subst1 tt)) . mm))
Subst2 phii
by A19, Lm44
.=
(<*(TheNorSymbOf S)*> ^ ((((l,tt) Subst4 (l Subst1 tt)) . ((Depth phi1) + m1)) . phi1)) ^ ((((l,tt) Subst4 (l Subst1 tt)) . ((Depth phi2) + m2)) . phi2)
by Def20, A19
.=
(<*(TheNorSymbOf S)*> ^ new1) ^ ((((l,tt) Subst4 (l Subst1 tt)) . ((Depth phi2) + m2)) . phi2)
by Lm45
.=
(<*(TheNorSymbOf S)*> ^ new1) ^ new2
by Lm45
;
then Depth ((l,tt) SubstIn phii) =
1
+ (max ((Depth new1),(Depth new2)))
by FOMODEL2:17
.=
1
+ (max ((Depth phi1),(Depth new2)))
by A21, A4
.=
1
+ (max ((Depth phi1),(Depth phi2)))
by A21, A4
.=
Depth phii
by FOMODEL2:17, A20
;
hence
Depth ((l,tt) SubstIn phi) = Depth phi
;
for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval philet I be
Element of
U -InterpretersOf S;
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phiset TE =
I -TermEval ;
set u =
(I -TermEval) . tt;
set J = (
l,
((I -TermEval) . tt))
ReassignIn I;
set LH =
I -TruthEval ((l,tt) SubstIn phii);
set RH =
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii;
(
I -TruthEval new1 = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi1 &
I -TruthEval new2 = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi2 )
by A21, A4;
then
(
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 1 iff (
I -TruthEval new1 = 0 &
I -TruthEval new2 = 0 ) )
by A20, FOMODEL2:19;
then
(
I -TruthEval ((l,tt) SubstIn phii) = 1 iff not
((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phii = 0 )
by FOMODEL2:19, A22, FOMODEL0:39;
hence
I -TruthEval ((l,tt) SubstIn phi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval phi
by FOMODEL0:39;
verum end; end;
end;
A23:
for m being Nat holds S1[m]
from NAT_1:sch 2(A1, A3);
set m = Depth psi;
thus
Depth ((l,tt) SubstIn psi) = Depth psi
by A23; for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi
let I be Element of U -InterpretersOf S; I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi
thus
I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi
by A23; verum