let S be Language; R#3a S is Correct
now for X being set st X is S -correct holds
(R#3a S) . X is S -correct set f =
R#3a S;
set R =
P#3a S;
set Q =
S -sequents ;
set E =
TheEqSymbOf S;
set N =
TheNorSymbOf S;
set FF =
AllFormulasOf S;
set TT =
AllTermsOf S;
set SS =
AllSymbolsOf S;
set F =
S -firstChar ;
set C =
S -multiCat ;
let X be
set ;
( X is S -correct implies (R#3a S) . X is S -correct )assume A1:
X is
S -correct
;
(R#3a S) . X is S -correct now for U being non empty set
for I being Element of U -InterpretersOf S
for x being b2 -satisfied set
for psi being wff string of S st [x,psi] in (R#3a S) . X holds
I -TruthEval psi = 1let U be non
empty set ;
for I being Element of U -InterpretersOf S
for x being b1 -satisfied set
for psi being wff string of S st [x,psi] in (R#3a S) . X holds
I -TruthEval psi = 1set II =
U -InterpretersOf S;
let I be
Element of
U -InterpretersOf S;
for x being I -satisfied set
for psi being wff string of S st [x,psi] in (R#3a S) . X holds
I -TruthEval psi = 1let x be
I -satisfied set ;
for psi being wff string of S st [x,psi] in (R#3a S) . X holds
I -TruthEval psi = 1let psi be
wff string of
S;
( [x,psi] in (R#3a S) . X implies I -TruthEval psi = 1 )set s =
[x,psi];
set TE =
I -TermEval ;
set d =
U -deltaInterpreter ;
assume A3:
[x,psi] in (R#3a S) . X
;
I -TruthEval psi = 1then A4:
(
[x,psi] in S -sequents &
[X,[x,psi]] in P#3a S )
by Lm30;
then
X in dom (P#3a S)
by XTUPLE_0:def 12;
then reconsider Seqts =
X as
S -correct Subset of
(S -sequents) by A1;
reconsider seqt =
[x,psi] as
Element of
S -sequents by A3, Lm30;
seqt Rule3a Seqts
by A4, Def37;
then consider t1,
t2,
t3 being
termal string of
S such that A5:
seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)]
;
reconsider phi1 =
(<*(TheEqSymbOf S)*> ^ t1) ^ t2,
phi2 =
(<*(TheEqSymbOf S)*> ^ t2) ^ t3,
phi =
(<*(TheEqSymbOf S)*> ^ t1) ^ t3 as
0wff string of
S ;
A6:
(
{phi1,phi2} \+\ (seqt `1) = {} &
phi \+\ (seqt `2) = {} )
by A5;
then
(
{phi1,phi2} is
I -satisfied &
phi = psi &
{phi1} \ {phi1,phi2} = {} &
{phi2} \ {phi1,phi2} = {} )
by FOMODEL0:29;
then
(
I -TruthEval phi1 = 1 &
I -TruthEval phi2 = 1 )
by ZFMISC_1:60;
then
(
(I -TermEval) . t1 = (I -TermEval) . t2 &
(I -TermEval) . t2 = (I -TermEval) . t3 )
by Lm54;
then
I -TruthEval phi = 1
by Lm54;
hence
I -TruthEval psi = 1
by A6, FOMODEL0:29;
verum end; hence
(R#3a S) . X is
S -correct
;
verum end;
hence
R#3a S is Correct
; verum