let S be Language; for D1 being 0 -ranked 1 -ranked RuleSet of S
for X being b1 -expanded set
for phi being 0wff string of S holds
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )
let D1 be 0 -ranked 1 -ranked RuleSet of S; for X being D1 -expanded set
for phi being 0wff string of S holds
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )
let X be D1 -expanded set ; for phi being 0wff string of S holds
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )
let phi be 0wff string of S; ( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )
R#0 S in D1
by Def62;
then A1:
{(R#0 S)} c= D1
by ZFMISC_1:31;
set TT = AllTermsOf S;
set E = TheEqSymbOf S;
set p = SubTerms phi;
set F = S -firstChar ;
set s = (S -firstChar) . phi;
set n = |.(ar ((S -firstChar) . phi)).|;
set R = (X,D1) -termEq ;
set U = Class ((X,D1) -termEq);
set AF = AtomicFormulasOf S;
set d = (Class ((X,D1) -termEq)) -deltaInterpreter ;
set i = (S,X) -freeInterpreter ;
A2:
|.(ar (TheEqSymbOf S)).| - 2 = 0
;
reconsider I = D1 Henkin X as Element of (Class ((X,D1) -termEq)) -InterpretersOf S ;
set UV = I -TermEval ;
set V = I -AtomicEval phi;
set uv = ((S,X) -freeInterpreter) -TermEval ;
set v = ((S,X) -freeInterpreter) -AtomicEval phi;
set f = (I ===) . ((S -firstChar) . phi);
set G = I . ((S -firstChar) . phi);
set g = ((S,X) -freeInterpreter) . ((S -firstChar) . phi);
set O = OwnSymbolsOf S;
set FF = AllFormulasOf S;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
reconsider pp = SubTerms phi as Element of |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) by FOMODEL0:16;
pp is Element of Funcs ((Seg |.(ar ((S -firstChar) . phi)).|),(AllTermsOf S))
by FOMODEL0:11;
then reconsider fp = pp as Function of (Seg |.(ar ((S -firstChar) . phi)).|),(AllTermsOf S) ;
A3:
2 -tuples_on (((AllSymbolsOf S) *) \ {{}}) = { <*tt1,tt2*> where tt1, tt2 is Element of ((AllSymbolsOf S) *) \ {{}} : verum }
by FINSEQ_2:99;
SubTerms phi in (AllTermsOf S) *
;
then reconsider Pp = SubTerms phi as Element of (((AllSymbolsOf S) *) \ {{}}) * ;
A4:
phi = <*((S -firstChar) . phi)*> ^ ((S -multiCat) . (SubTerms phi))
by FOMODEL1:def 38;
A5:
I -TermEval = (((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)
by FOMODEL3:3;
A6:
((S,X) -freeInterpreter) -TermEval = id (AllTermsOf S)
by FOMODEL3:4;
( |.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) c= (AllTermsOf S) * & (AllTermsOf S) * c= (((AllSymbolsOf S) *) \ {{}}) * )
by FINSEQ_2:142;
then
|.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S) c= (((AllSymbolsOf S) *) \ {{}}) *
by XBOOLE_1:1;
then reconsider nc = (((S -firstChar) . phi) -compound) | (|.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S)) as Function of (|.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S)),(((AllSymbolsOf S) *) \ {{}}) by FUNCT_2:32;
per cases
( (S -firstChar) . phi = TheEqSymbOf S or not (S -firstChar) . phi = TheEqSymbOf S )
;
suppose A7:
(S -firstChar) . phi = TheEqSymbOf S
;
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )reconsider p1 =
SubTerms phi as
(0 + 1) + 1
-element Element of
(AllTermsOf S) * by A7, A2;
Pp in 2
-tuples_on (((AllSymbolsOf S) *) \ {{}})
by A2, A7, FOMODEL0:16;
then consider tt11,
tt22 being
Element of
((AllSymbolsOf S) *) \ {{}} such that A8:
Pp = <*tt11,tt22*>
by A3;
A9:
(S -multiCat) . <*tt11,tt22*> = tt11 ^ tt22
by FOMODEL0:15;
reconsider p2 =
SubTerms phi as
(1 + 1) + 0 -element Element of
(AllTermsOf S) * by A7, A2;
(
{(p1 . (0 + 1))} \ (AllTermsOf S) = {} &
{(p2 . (1 + 1))} \ (AllTermsOf S) = {} )
;
then reconsider tt1 =
(SubTerms phi) . 1,
tt2 =
(SubTerms phi) . 2 as
Element of
AllTermsOf S by ZFMISC_1:60;
reconsider t1 =
tt1,
t2 =
tt2 as
termal string of
S ;
A10:
(
(((X,D1) -termEq) -class) . tt1 = EqClass (
((X,D1) -termEq),
tt1) &
(((X,D1) -termEq) -class) . tt2 = EqClass (
((X,D1) -termEq),
tt2) )
by FOMODEL3:def 13;
A11:
(
tt1 = tt11 &
tt2 = tt22 )
by A8, FINSEQ_1:44;
(
(((((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)) . tt1) \+\ ((((X,D1) -termEq) -class) . ((((S,X) -freeInterpreter) -TermEval) . tt1)) = {} &
(((((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)) . tt2) \+\ ((((X,D1) -termEq) -class) . ((((S,X) -freeInterpreter) -TermEval) . tt2)) = {} )
;
then
(
((((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)) . tt1 = (((X,D1) -termEq) -class) . ((((S,X) -freeInterpreter) -TermEval) . tt1) &
((((X,D1) -termEq) -class) * (((S,X) -freeInterpreter) -TermEval)) . tt2 = (((X,D1) -termEq) -class) . ((((S,X) -freeInterpreter) -TermEval) . tt2) )
by FOMODEL0:29;
then A12:
(
I -AtomicEval phi = 1 iff
EqClass (
((X,D1) -termEq),
tt1)
= EqClass (
((X,D1) -termEq),
tt2) )
by A10, FOMODEL2:15, A5, A7, A6;
then A13:
(
I -AtomicEval phi = 1 iff
[tt1,tt2] in (
X,
D1)
-termEq )
by EQREL_1:35;
A14:
(<*(TheEqSymbOf S)*> ^ t1) ^ t2 = phi
by A4, A8, A9, A11, A7, FINSEQ_1:32;
thus
(
(D1 Henkin X) -AtomicEval phi = 1 implies
phi in X )
( phi in X implies (D1 Henkin X) -AtomicEval phi = 1 )proof
assume
(D1 Henkin X) -AtomicEval phi = 1
;
phi in X
then
[tt1,tt2] in (
X,
D1)
-termEq
by A12, EQREL_1:35;
then consider t11,
t22 being
termal string of
S such that A15:
(
[tt1,tt2] = [t11,t22] &
(<*(TheEqSymbOf S)*> ^ t11) ^ t22 is
X,
D1 -provable )
;
(
t11 = tt1 &
t22 = tt2 )
by A15, XTUPLE_0:1;
then
<*(TheEqSymbOf S)*> ^ (t11 ^ t22) = phi
by A4, A8, FOMODEL0:15, A11, A7;
then
phi is
X,
D1 -provable
by A15, FINSEQ_1:32;
then
{phi} c= X
by Def17;
hence
phi in X
by ZFMISC_1:31;
verum
end; assume
phi in X
;
(D1 Henkin X) -AtomicEval phi = 1then reconsider Xphi =
{phi} as
Subset of
X by ZFMISC_1:31;
{[{phi},phi]} is
{} ,
D1 -derivable
by Lm18, A1;
then
phi is
Xphi,
D1 -provable
;
hence
(D1 Henkin X) -AtomicEval phi = 1
by A13, A14;
verum end; suppose A16:
not
(S -firstChar) . phi = TheEqSymbOf S
;
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X )then reconsider o =
(S -firstChar) . phi as
Element of
OwnSymbolsOf S by FOMODEL1:15;
set gg =
((S,X) -freeInterpreter) . o;
(
(S -firstChar) . phi <> TheEqSymbOf S &
I -AtomicEval phi = ((S,X) -freeInterpreter) -AtomicEval phi &
((S,X) -freeInterpreter) -AtomicEval phi = (((S,X) -freeInterpreter) . o) . ((((S,X) -freeInterpreter) -TermEval) * (SubTerms phi)) )
by FOMODEL3:5, FOMODEL2:14, A16;
then I -AtomicEval phi =
(((S,X) -freeInterpreter) . o) . ((id (AllTermsOf S)) * fp)
by FOMODEL3:4
.=
(((S,X) -freeInterpreter) . o) . fp
by FUNCT_2:17
.=
(X -freeInterpreter o) . (SubTerms phi)
by FOMODEL3:def 4
.=
((chi (X,(AtomicFormulasOf S))) * ((o -compound) | (|.(ar ((S -firstChar) . phi)).| -tuples_on (AllTermsOf S)))) . pp
by FOMODEL3:def 3
.=
(chi (X,(AtomicFormulasOf S))) . (nc . pp)
by FUNCT_2:15
.=
(chi (X,(AtomicFormulasOf S))) . ((o -compound) . pp)
by FUNCT_1:49
.=
(chi (X,(AtomicFormulasOf S))) . (o -compound Pp)
by FOMODEL3:def 2
.=
(chi (X,(AtomicFormulasOf S))) . phi
by FOMODEL1:def 38
;
then
(
I -AtomicEval phi = 1 iff
phi in (chi (X,(AtomicFormulasOf S))) " {1} )
by FOMODEL0:25;
then
(
I -AtomicEval phi = 1 iff
phi in X /\ (AtomicFormulasOf S) )
by FOMODEL0:24;
then
(
phi in AtomicFormulasOf S & (
I -AtomicEval phi = 1 implies (
phi in X &
phi in AtomicFormulasOf S ) ) & (
phi in X &
phi in AtomicFormulasOf S implies
I -AtomicEval phi = 1 ) )
by XBOOLE_0:def 4;
hence
(
(D1 Henkin X) -AtomicEval phi = 1 iff
phi in X )
;
verum end;