begin
Lm1:
for S being Language
for U being non empty set
for f being Interpreter of S,U holds OwnSymbolsOf S c= dom f
Lm2:
for S being Language
for U being non empty set
for f being Function st f is S,U -interpreter-like holds
OwnSymbolsOf S c= dom f
Lm3:
for U being non empty set
for S being Language
for I being b2,b1 -interpreter-like Function
for t being termal string of S holds (abs (ar t)) -tuples_on U = dom (I . ((S -firstChar) . t))
by FUNCT_2:def 1;
Lm4:
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for xx being Function of (AllTermsOf S),U holds
( ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Element of Funcs ((AllTermsOf S),U) & AllTermsOf S c= dom (I * (S -firstChar)) )
definition
let S be
Language;
let U be non
empty set ;
let u be
Element of
U;
let I be
S,
U -interpreter-like Function;
existence
ex b1 being Function of NAT,(Funcs ((AllTermsOf S),U)) st
( b1 . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b1 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b1 . mm),(S -subTerms)____ ) )
uniqueness
for b1, b2 being Function of NAT,(Funcs ((AllTermsOf S),U)) st b1 . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b1 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b1 . mm),(S -subTerms)____ ) & b2 . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b2 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b2 . mm),(S -subTerms)____ ) holds
b1 = b2
end;
Lm5:
for S being Language
for U being non empty set
for u being Element of U
for I being b1,b2 -interpreter-like Function
for t being termal string of S
for mm being Element of NAT holds
( (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . mm) * (SubTerms t)) & ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . ((S -firstChar) . t)) . {} ) )
Lm6:
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for u1, u2 being Element of U
for m being Nat
for t being b6 -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t
definition
let S be
Language;
let U be non
empty set ;
let g be
Element of
PFuncs (
[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN);
existence
ex b1 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g & y = <*v*> ^ w ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -ExFunctor (x,y) ) )
uniqueness
for b1, b2 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g & y = <*v*> ^ w ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -ExFunctor (x,y) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b2 iff ex v being literal Element of S ex w being string of S st
( [x,w] in dom g & y = <*v*> ^ w ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b2 holds
b2 . (x,y) = g -ExFunctor (x,y) ) holds
b1 = b2
end;
definition
let S be
Language;
let U be non
empty set ;
let f be
PartFunc of
[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN;
let I be
Element of
U -InterpretersOf S;
let phi be
Element of
((AllSymbolsOf S) *) \ {{}};
coherence
( ( ex w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( [I,w1] in dom f & f . (I,w1) = FALSE & f . (I,w2) = FALSE & phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) implies TRUE is Element of BOOLEAN ) & ( ( for w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} holds
( not [I,w1] in dom f or not f . (I,w1) = FALSE or not f . (I,w2) = FALSE or not phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) ) implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
end;
::
deftheorem Def18 defines
-NorFunctor FOMODEL2:def 18 :
for S being Language
for U being non empty set
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN
for I being Element of U -InterpretersOf S
for phi being Element of ((AllSymbolsOf S) *) \ {{}} holds
( ( ex w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( [I,w1] in dom f & f . (I,w1) = FALSE & f . (I,w2) = FALSE & phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) implies f -NorFunctor (I,phi) = TRUE ) & ( ( for w1, w2 being Element of ((AllSymbolsOf S) *) \ {{}} holds
( not [I,w1] in dom f or not f . (I,w1) = FALSE or not f . (I,w2) = FALSE or not phi = (<*(TheNorSymbOf S)*> ^ w1) ^ w2 ) ) implies f -NorFunctor (I,phi) = FALSE ) );
definition
let S be
Language;
let U be non
empty set ;
let g be
Element of
PFuncs (
[:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],
BOOLEAN);
existence
ex b1 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -NorFunctor (x,y) ) )
uniqueness
for b1, b2 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b1 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b1 holds
b1 . (x,y) = g -NorFunctor (x,y) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b2 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b2 holds
b2 . (x,y) = g -NorFunctor (x,y) ) holds
b1 = b2
end;
::
deftheorem Def19 defines
NorIterator FOMODEL2:def 19 :
for S being Language
for U being non empty set
for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)
for b4 being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds
( b4 = NorIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b4 iff ex phi1, phi2 being Element of ((AllSymbolsOf S) *) \ {{}} st
( y = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [x,phi1] in dom g & [x,phi2] in dom g ) ) ) & ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} st [x,y] in dom b4 holds
b4 . (x,y) = g -NorFunctor (x,y) ) ) );
Lm7:
for m being Nat
for x being set
for S being Language
for U being non empty set
for n being Nat st x in dom ((S,U) -TruthEval m) holds
( x in dom ((S,U) -TruthEval (m + n)) & ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + n)) . x )
Lm8:
for x, X, Y, Z being set holds
( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) )
Lm9:
for S being Language
for U1, U2 being non empty set
for m being Nat
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval m) holds
[I2,w] in dom ((S,U2) -TruthEval m)
Lm10:
for mm being Element of NAT
for S being Language
for U being non empty set holds curry (((S,U) -TruthEval) . mm) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
Lm11:
for m being Nat
for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN))
Lm12:
for m, n being Nat
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval c= (I,(m + n)) -TruthEval
Lm13:
for m being Nat
for S being Language
for U1, U2 being non empty set
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S holds dom ((I1,m) -TruthEval) c= dom ((I2,m) -TruthEval)
Lm14:
for mm being Element of NAT
for S being Language
for U1, U2 being non empty set
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S holds dom ((I1,mm) -TruthEval) = dom ((I2,mm) -TruthEval)
Lm15:
for m, n being Nat
for S being Language holds S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n)
Lm16:
for S being Language holds S -formulasOfMaxDepth 0 = AtomicFormulasOf S
theorem
for
x,
X,
Y,
Z being
set holds
(
x in (X \/ Y) \/ Z iff (
x in X or
x in Y or
x in Z ) )
by Lm8;
Lm17:
for m being Nat
for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (U -InterpretersOf S),(Funcs ((S -formulasOfMaxDepth m),BOOLEAN))
Lm18:
for m being Nat
for S being Language
for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):]
Lm19:
for m being Nat
for S being Language
for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):]
Lm20:
for m being Nat
for S being Language
for phi being wff string of S st phi in (S -formulasOfMaxDepth m) \ (S -formulasOfMaxDepth 0) holds
ex n being Nat st
( phi is n + 1 -wff & not phi is n -wff & n + 1 <= m )
Lm21:
for m being Nat
for S being Language
for w being string of S st w is m + 1 -wff & not w is m -wff & ( for v being literal Element of S
for phi being b1 -wff string of S holds not w = <*v*> ^ phi ) holds
ex phi1, phi2 being b1 -wff string of S st w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2
Lm22:
for S being Language
for phi being wff string of S st not phi is 0wff holds
Depth phi <> 0
Lm23:
for S being Language
for w being string of S st w is wff & not w is 0wff & not w . 1 in LettersOf S holds
w . 1 = TheNorSymbOf S
Lm24:
for m being Nat
for S being Language holds S -formulasOfMaxDepth m is S -prefix
Lm25:
for S being Language holds AllFormulasOf S is S -prefix
Lm26:
for U being non empty set holds (U -deltaInterpreter) " {1} = (U -concatenation) .: (id (1 -tuples_on U))
Lm27:
for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 & phi is exal holds
phi in m -ExFormulasOf S
Lm28:
for S being Language
for l being literal Element of S
for phi1 being wff string of S holds Depth (<*l*> ^ phi1) > Depth phi1
Lm29:
for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 & not phi is exal holds
phi in m -NorFormulasOf S
Lm30:
for S being Language
for phi1, phi2 being wff string of S holds
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 )
Lm31:
for S being Language
for phi1, phi2 being wff string of S holds Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
Lm32:
for S being Language
for U being non empty set
for I being Relation st I in U -InterpretersOf S holds
dom I = OwnSymbolsOf S
Lm33:
for m being Nat
for S being Language
for w being string of S
for U being non empty set
for I being Element of U -InterpretersOf S st w is m -wff holds
((I,m) -TruthEval) . w = ((S,U) -TruthEval m) . [I,w]
Lm34:
for m being Nat
for S being Language
for U being non empty set
for l being literal Element of S
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -ExFunctor (I,(<*l*> ^ phi1)) = 1 iff ex u being Element of U st f . (((l,u) ReassignIn I),phi1) = TRUE )
Lm35:
for S being Language
for U being non empty set
for l being literal Element of S
for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval (<*l*> ^ phi) = TRUE iff ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 )
Lm36:
for m being Nat
for S being Language
for w2 being string of S
for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
Lm37:
for S being Language
for U being non empty set
for phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) )
Lm38:
for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 & not phi is exal holds
ex phi2 being b1 -wff string of S st tail phi = phi2
Lm39:
for m being Nat
for S being Language
for phi being wff string of S st not phi is 0wff & not phi is exal & phi is m + 1 -wff holds
( head phi is b1 -wff string of S & tail phi is b1 -wff string of S )
Lm40:
for S being Language
for U being non empty set
for phi0 being 0wff string of S
for I being Element of U -InterpretersOf S holds I -TruthEval phi0 = I -AtomicEval phi0
Lm41:
for X being set
for S being Language
for U being non empty set
for I1, I2 being b2,b3 -interpreter-like Function st I1 | X = I2 | X holds
(I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
Lm42:
for S being Language
for w being string of S st w is termal holds
(rng w) /\ (LettersOf S) <> {}
Lm43:
for S being Language
for w being string of S st w is wff holds
(rng w) /\ (LettersOf S) <> {}
::###############################################################
::###############################################################
::# Interpreter of a Language.