:: First order languages: syntax, part two; semantics.
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users


begin

definition
let S be Language;
:: original: TheNorSymbOf
redefine func TheNorSymbOf S -> Element of S;
coherence
TheNorSymbOf S is Element of S
;
end;

definition
let U be non empty set ;
func U -deltaInterpreter -> Function of (2 -tuples_on U),BOOLEAN equals :: FOMODEL2:def 1
chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U));
coherence
chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U)) is Function of (2 -tuples_on U),BOOLEAN
;
end;

:: deftheorem defines -deltaInterpreter FOMODEL2:def 1 :
for U being non empty set holds U -deltaInterpreter = chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U));

definition
let X be set ;
:: original: id
redefine func id X -> Equivalence_Relation of X;
coherence
id X is Equivalence_Relation of X
by EQREL_1:6;
end;

definition
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
mode Interpreter of s,U -> set means :DefInterpreter1: :: FOMODEL2:def 2
it is Function of ((abs (ar s)) -tuples_on U),BOOLEAN if s is relational
otherwise it is Function of ((abs (ar s)) -tuples_on U),U;
existence
( ( s is relational implies ex b1 being set st b1 is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ) & ( not s is relational implies ex b1 being set st b1 is Function of ((abs (ar s)) -tuples_on U),U ) )
proof end;
consistency
for b1 being set holds verum
;
end;

:: deftheorem DefInterpreter1 defines Interpreter FOMODEL2:def 2 :
for S being Language
for U being non empty set
for s being ofAtomicFormula Element of S
for b4 being set holds
( ( s is relational implies ( b4 is Interpreter of s,U iff b4 is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ) ) & ( not s is relational implies ( b4 is Interpreter of s,U iff b4 is Function of ((abs (ar s)) -tuples_on U),U ) ) );

definition
let S be Language;
let U be non empty set ;
let s be ofAtomicFormula Element of S;
:: original: Interpreter
redefine mode Interpreter of s,U -> Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN);
coherence
for b1 being Interpreter of s,U holds b1 is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN)
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let s be termal Element of S;
cluster -> U -valued Interpreter of s,U;
coherence
for b1 being Interpreter of s,U holds b1 is U -valued
by DefInterpreter1;
end;

registration
let S be Language;
cluster literal -> own Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is literal holds
b1 is own
;
end;

definition
let S be Language;
let U be non empty set ;
mode Interpreter of S,U -> Function means :DefInterpreter2: :: FOMODEL2:def 3
for s being own Element of S holds it . s is Interpreter of s,U;
existence
ex b1 being Function st
for s being own Element of S holds b1 . s is Interpreter of s,U
proof end;
end;

:: deftheorem DefInterpreter2 defines Interpreter FOMODEL2:def 3 :
for S being Language
for U being non empty set
for b3 being Function holds
( b3 is Interpreter of S,U iff for s being own Element of S holds b3 . s is Interpreter of s,U );

definition
let S be Language;
let U be non empty set ;
let f be Function;
attr f is S,U -interpreter-like means :DefInterpreterLike: :: FOMODEL2:def 4
( f is Interpreter of S,U & f is Function-yielding );
end;

:: deftheorem DefInterpreterLike defines -interpreter-like FOMODEL2:def 4 :
for S being Language
for U being non empty set
for f being Function holds
( f is S,U -interpreter-like iff ( f is Interpreter of S,U & f is Function-yielding ) );

registration
let S be Language;
let U be non empty set ;
cluster Relation-like Function-like S,U -interpreter-like -> Function-yielding set ;
coherence
for b1 being Function st b1 is S,U -interpreter-like holds
b1 is Function-yielding
by DefInterpreterLike;
end;

registration
let S be Language;
let U be non empty set ;
let s be own Element of S;
cluster -> non empty Interpreter of s,U;
coherence
for b1 being Interpreter of s,U holds not b1 is empty
;
end;

Lm2: for S being Language
for U being non empty set
for f being Interpreter of S,U holds OwnSymbolsOf S c= dom f
proof end;

Lm18: 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
proof end;

registration
let S be Language;
let U be non empty set ;
cluster Relation-like Function-like S,U -interpreter-like set ;
existence
ex b1 being Function st b1 is S,U -interpreter-like
proof end;
end;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let s be own Element of S;
:: original: .
redefine func I . s -> Interpreter of s,U;
coherence
I . s is Interpreter of s,U
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let x be own Element of S;
let f be Interpreter of x,U;
cluster I +* (x .--> f) -> S,U -interpreter-like ;
coherence
I +* (x .--> f) is S,U -interpreter-like
proof end;
end;

definition
let f be Function;
let x, y be set ;
func (x,y) ReassignIn f -> Function equals :: FOMODEL2:def 5
f +* (x .--> ({} .--> y));
coherence
f +* (x .--> ({} .--> y)) is Function
;
end;

:: deftheorem defines ReassignIn FOMODEL2:def 5 :
for f being Function
for x, y being set holds (x,y) ReassignIn f = f +* (x .--> ({} .--> y));

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let x be literal Element of S;
let u be Element of U;
cluster (x,u) ReassignIn I -> S,U -interpreter-like ;
coherence
(x,u) ReassignIn I is S,U -interpreter-like
proof end;
end;

registration
let S be Language;
cluster AllSymbolsOf S -> non empty ;
coherence
not AllSymbolsOf S is empty
;
end;

registration
let Y be set ;
let X, Z be non empty set ;
cluster Function-like quasi_total -> Function-yielding Element of bool [:X,(Funcs (Y,Z)):];
coherence
for b1 being Function of X,(Funcs (Y,Z)) holds b1 is Function-yielding
;
end;

registration
let X, Y, Z be non empty set ;
cluster non empty Relation-like X -defined Funcs (Y,Z) -valued Function-like total quasi_total Function-yielding Element of bool [:X,(Funcs (Y,Z)):];
existence
ex b1 being Function of X,(Funcs (Y,Z)) st b1 is Function-yielding
proof end;
end;

definition
let f be Function-yielding Function;
let g be Function;
func ^^^g,f__ -> Function means :Def6: :: FOMODEL2:def 6
( dom it = dom f & ( for x being set st x in dom f holds
it . x = g * (f . x) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = g * (f . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = g * (f . x) ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = g * (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines ^^^ FOMODEL2:def 6 :
for f being Function-yielding Function
for g, b3 being Function holds
( b3 = ^^^g,f__ iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = g * (f . x) ) ) );

registration
let f be empty Function;
let g be Function;
cluster ^^^g,f__ -> empty ;
coherence
^^^g,f__ is empty
proof end;
end;

definition
let f be Function-yielding Function;
let g be Function;
func ^^^f,g__ -> Function means :Def7: :: FOMODEL2:def 7
( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds
it . x = (f . x) . (g . x) ) );
existence
ex b1 being Function st
( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = (f . x) . (g . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = (f . x) . (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds
b2 . x = (f . x) . (g . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines ^^^ FOMODEL2:def 7 :
for f being Function-yielding Function
for g, b3 being Function holds
( b3 = ^^^f,g__ iff ( dom b3 = (dom f) /\ (dom g) & ( for x being set st x in dom b3 holds
b3 . x = (f . x) . (g . x) ) ) );

registration
let f be Function-yielding Function;
let g be empty Function;
cluster ^^^f,g__ -> empty ;
coherence
^^^f,g__ is empty
proof end;
end;

registration
let X be FinSequence-membered set ;
cluster Relation-like X -valued Function-like -> Function-yielding set ;
coherence
for b1 being Function st b1 is X -valued holds
b1 is Function-yielding
proof end;
end;

registration
let E, D be non empty set ;
let p be D -valued FinSequence;
let h be Function of D,E;
cluster h (*) p -> len p -element FinSequence;
coherence
for b1 being FinSequence st b1 = h * p holds
b1 is len p -element
proof end;
end;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
let p be X -valued FinSequence;
cluster f (*) p -> FinSequence-like ;
coherence
f * p is FinSequence-like
;
end;

registration
let E, D be non empty set ;
let n be Nat;
let p be D -valued n -element FinSequence;
let h be Function of D,E;
cluster h (*) p -> n -element FinSequence of E;
coherence
for b1 being FinSequence of E st b1 = h * p holds
b1 is n -element
;
end;

Lm15: 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;

theorem :: FOMODEL2:1
for S being Language
for t0 being 0 -termal string of S holds t0 = <*((S -firstChar) . t0)*>
proof end;

Lm20: 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)) )
proof end;

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;
func (I,u) -TermEval -> Function of NAT,(Funcs ((AllTermsOf S),U)) means :DefTermEval1: :: FOMODEL2:def 8
( it . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds it . (mm + 1) = ^^^(I * (S -firstChar)),^^^(it . mm),(S -subTerms)____ ) );
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)____ ) )
proof end;
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
proof end;
end;

:: deftheorem DefTermEval1 defines -TermEval FOMODEL2:def 8 :
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 b5 being Function of NAT,(Funcs ((AllTermsOf S),U)) holds
( b5 = (I,u) -TermEval iff ( b5 . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b5 . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b5 . mm),(S -subTerms)____ ) ) );

Lm21: 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)) . {} ) )
proof end;

Lm1: 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
proof end;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let t be Element of AllTermsOf S;
func I -TermEval t -> Element of U means :DefTermEval2: :: FOMODEL2:def 9
for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
it = (((I,u1) -TermEval) . (mm + 1)) . t;
existence
ex b1 being Element of U st
for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b1 = (((I,u1) -TermEval) . (mm + 1)) . t
proof end;
uniqueness
for b1, b2 being Element of U st ( for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b1 = (((I,u1) -TermEval) . (mm + 1)) . t ) & ( for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b2 = (((I,u1) -TermEval) . (mm + 1)) . t ) holds
b1 = b2
proof end;
end;

:: deftheorem DefTermEval2 defines -TermEval FOMODEL2:def 9 :
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for t being Element of AllTermsOf S
for b5 being Element of U holds
( b5 = I -TermEval t iff for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b5 = (((I,u1) -TermEval) . (mm + 1)) . t );

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
func I -TermEval -> Function of (AllTermsOf S),U means :DefTermEval3: :: FOMODEL2:def 10
for t being Element of AllTermsOf S holds it . t = I -TermEval t;
existence
ex b1 being Function of (AllTermsOf S),U st
for t being Element of AllTermsOf S holds b1 . t = I -TermEval t
proof end;
uniqueness
for b1, b2 being Function of (AllTermsOf S),U st ( for t being Element of AllTermsOf S holds b1 . t = I -TermEval t ) & ( for t being Element of AllTermsOf S holds b2 . t = I -TermEval t ) holds
b1 = b2
proof end;
end;

:: deftheorem DefTermEval3 defines -TermEval FOMODEL2:def 10 :
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for b4 being Function of (AllTermsOf S),U holds
( b4 = I -TermEval iff for t being Element of AllTermsOf S holds b4 . t = I -TermEval t );

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
func I === -> Function equals :: FOMODEL2:def 11
I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter));
coherence
I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter)) is Function
;
end;

:: deftheorem defines === FOMODEL2:def 11 :
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function holds I === = I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter));

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let x be set ;
attr x is I -extension means :DefExtension: :: FOMODEL2:def 12
x = I === ;
end;

:: deftheorem DefExtension defines -extension FOMODEL2:def 12 :
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for x being set holds
( x is I -extension iff x = I === );

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster I === -> I -extension Function;
coherence
for b1 being Function st b1 = I === holds
b1 is I -extension
by DefExtension;
cluster I -extension -> Function-like set ;
coherence
for b1 being set st b1 is I -extension holds
b1 is Function-like
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster Relation-like Function-like I -extension set ;
existence
ex b1 being Function st b1 is I -extension
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster I === -> S,U -interpreter-like ;
coherence
I === is S,U -interpreter-like
proof end;
end;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let f be I -extension Function;
let s be ofAtomicFormula Element of S;
:: original: .
redefine func f . s -> Interpreter of s,U;
coherence
f . s is Interpreter of s,U
proof end;
end;

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let phi be 0wff string of S;
func I -AtomicEval phi -> set equals :: FOMODEL2:def 13
((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi));
coherence
((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) is set
;
end;

:: deftheorem defines -AtomicEval FOMODEL2:def 13 :
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for phi being 0wff string of S holds I -AtomicEval phi = ((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi));

definition
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
let phi be 0wff string of S;
:: original: -AtomicEval
redefine func I -AtomicEval phi -> Element of BOOLEAN ;
coherence
I -AtomicEval phi is Element of BOOLEAN
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster I | (OwnSymbolsOf S) -> PFuncs ((U *),(U \/ BOOLEAN)) -valued Function;
coherence
for b1 being Function st b1 = I | (OwnSymbolsOf S) holds
b1 is PFuncs ((U *),(U \/ BOOLEAN)) -valued
proof end;
cluster I | (OwnSymbolsOf S) -> S,U -interpreter-like Function;
coherence
for b1 being Function st b1 = I | (OwnSymbolsOf S) holds
b1 is S,U -interpreter-like
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster I | (OwnSymbolsOf S) -> OwnSymbolsOf S -defined total OwnSymbolsOf S -defined Relation;
coherence
for b1 being OwnSymbolsOf S -defined Relation st b1 = I | (OwnSymbolsOf S) holds
b1 is total
proof end;
end;

definition
let S be Language;
let U be non empty set ;
func U -InterpretersOf S -> set equals :: FOMODEL2:def 14
{ f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like } ;
coherence
{ f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like } is set
;
end;

:: deftheorem defines -InterpretersOf FOMODEL2:def 14 :
for S being Language
for U being non empty set holds U -InterpretersOf S = { f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like } ;

definition
let S be Language;
let U be non empty set ;
:: original: -InterpretersOf
redefine func U -InterpretersOf S -> Subset of (Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))));
coherence
U -InterpretersOf S is Subset of (Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))))
proof end;
end;

registration
let S be Language;
let U be non empty set ;
cluster U -InterpretersOf S -> non empty ;
coherence
not U -InterpretersOf S is empty
proof end;
end;

registration
let S be Language;
let U be non empty set ;
cluster -> S,U -interpreter-like Element of U -InterpretersOf S;
coherence
for b1 being Element of U -InterpretersOf S holds b1 is S,U -interpreter-like
proof end;
end;

definition
let S be Language;
let U be non empty set ;
func S -TruthEval U -> Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN means :DefTruth6: :: FOMODEL2:def 15
for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds it . (I,phi) = I -AtomicEval phi;
existence
ex b1 being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN st
for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b1 . (I,phi) = I -AtomicEval phi
proof end;
uniqueness
for b1, b2 being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN st ( for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b1 . (I,phi) = I -AtomicEval phi ) & ( for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b2 . (I,phi) = I -AtomicEval phi ) holds
b1 = b2
proof end;
end;

:: deftheorem DefTruth6 defines -TruthEval FOMODEL2:def 15 :
for S being Language
for U being non empty set
for b3 being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN holds
( b3 = S -TruthEval U iff for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b3 . (I,phi) = I -AtomicEval phi );

definition
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let f be PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN;
let phi be Element of ((AllSymbolsOf S) *) \ {{}};
func f -ExFunctor (I,phi) -> Element of BOOLEAN equals :DefExFunc: :: FOMODEL2:def 16
TRUE if ex u being Element of U ex v being literal Element of S st
( phi . 1 = v & f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE )
otherwise FALSE ;
coherence
( ( ex u being Element of U ex v being literal Element of S st
( phi . 1 = v & f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) implies TRUE is Element of BOOLEAN ) & ( ( for u being Element of U
for v being literal Element of S holds
( not phi . 1 = v or not f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) ) implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
end;

:: deftheorem DefExFunc defines -ExFunctor FOMODEL2:def 16 :
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN
for phi being Element of ((AllSymbolsOf S) *) \ {{}} holds
( ( ex u being Element of U ex v being literal Element of S st
( phi . 1 = v & f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) implies f -ExFunctor (I,phi) = TRUE ) & ( ( for u being Element of U
for v being literal Element of S holds
( not phi . 1 = v or not f . (((v,u) ReassignIn I),(phi /^ 1)) = TRUE ) ) implies f -ExFunctor (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);
func ExIterator g -> PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN means :DefExIter: :: FOMODEL2:def 17
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom it 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 it holds
it . (x,y) = g -ExFunctor (x,y) ) );
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) ) )
proof end;
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
proof end;
end;

:: deftheorem DefExIter defines ExIterator FOMODEL2:def 17 :
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 = ExIterator 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 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 b4 holds
b4 . (x,y) = g -ExFunctor (x,y) ) ) );

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) *) \ {{}};
func f -NorFunctor (I,phi) -> Element of BOOLEAN equals :DefNew: :: FOMODEL2:def 18
TRUE if 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 )
otherwise FALSE ;
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 DefNew 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);
func NorIterator g -> PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN means :DefNorIter: :: FOMODEL2:def 19
( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom it 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 it holds
it . (x,y) = g -NorFunctor (x,y) ) );
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) ) )
proof end;
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
proof end;
end;

:: deftheorem DefNorIter 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) ) ) );

definition
let S be Language;
let U be non empty set ;
func (S,U) -TruthEval -> Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) means :DefTruth1: :: FOMODEL2:def 20
( it . 0 = S -TruthEval U & ( for mm being Element of NAT holds it . (mm + 1) = ((ExIterator (it . mm)) +* (NorIterator (it . mm))) +* (it . mm) ) );
existence
ex b1 being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) st
( b1 . 0 = S -TruthEval U & ( for mm being Element of NAT holds b1 . (mm + 1) = ((ExIterator (b1 . mm)) +* (NorIterator (b1 . mm))) +* (b1 . mm) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) st b1 . 0 = S -TruthEval U & ( for mm being Element of NAT holds b1 . (mm + 1) = ((ExIterator (b1 . mm)) +* (NorIterator (b1 . mm))) +* (b1 . mm) ) & b2 . 0 = S -TruthEval U & ( for mm being Element of NAT holds b2 . (mm + 1) = ((ExIterator (b2 . mm)) +* (NorIterator (b2 . mm))) +* (b2 . mm) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefTruth1 defines -TruthEval FOMODEL2:def 20 :
for S being Language
for U being non empty set
for b3 being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) holds
( b3 = (S,U) -TruthEval iff ( b3 . 0 = S -TruthEval U & ( for mm being Element of NAT holds b3 . (mm + 1) = ((ExIterator (b3 . mm)) +* (NorIterator (b3 . mm))) +* (b3 . mm) ) ) );

theorem Th2: :: FOMODEL2:2
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function holds I | (OwnSymbolsOf S) in U -InterpretersOf S
proof end;

definition
let S be Language;
let m be Nat;
let U be non empty set ;
func (S,U) -TruthEval m -> Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) means :DefTruth2: :: FOMODEL2:def 21
for mm being Element of NAT st m = mm holds
it = ((S,U) -TruthEval) . mm;
existence
ex b1 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st
for mm being Element of NAT st m = mm holds
b1 = ((S,U) -TruthEval) . mm
proof end;
uniqueness
for b1, b2 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st ( for mm being Element of NAT st m = mm holds
b1 = ((S,U) -TruthEval) . mm ) & ( for mm being Element of NAT st m = mm holds
b2 = ((S,U) -TruthEval) . mm ) holds
b1 = b2
proof end;
end;

:: deftheorem DefTruth2 defines -TruthEval FOMODEL2:def 21 :
for S being Language
for m being Nat
for U being non empty set
for b4 being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) holds
( b4 = (S,U) -TruthEval m iff for mm being Element of NAT st m = mm holds
b4 = ((S,U) -TruthEval) . mm );

Lm26: 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 )
proof end;

Lm25: 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 ) )
proof end;

Lm23: 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)
proof end;

Lm22: 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))
proof end;

Lm28: 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))
proof end;

definition
let S be Language;
let U be non empty set ;
let m be Nat;
let I be Element of U -InterpretersOf S;
func (I,m) -TruthEval -> Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN) equals :: FOMODEL2:def 22
(curry ((S,U) -TruthEval m)) . I;
coherence
(curry ((S,U) -TruthEval m)) . I is Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)
proof end;
end;

:: deftheorem defines -TruthEval FOMODEL2:def 22 :
for S being Language
for U being non empty set
for m being Nat
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval = (curry ((S,U) -TruthEval m)) . I;

Lm29: 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
proof end;

Lm24: 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)
proof end;

Lm27: 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)
proof end;

definition
let S be Language;
let m be Nat;
func S -formulasOfMaxDepth m -> Subset of (((AllSymbolsOf S) *) \ {{}}) means :DefFormula1: :: FOMODEL2:def 23
for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
it = dom ((I,mm) -TruthEval);
existence
ex b1 being Subset of (((AllSymbolsOf S) *) \ {{}}) st
for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b1 = dom ((I,mm) -TruthEval)
proof end;
uniqueness
for b1, b2 being Subset of (((AllSymbolsOf S) *) \ {{}}) st ( for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b1 = dom ((I,mm) -TruthEval) ) & ( for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b2 = dom ((I,mm) -TruthEval) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefFormula1 defines -formulasOfMaxDepth FOMODEL2:def 23 :
for S being Language
for m being Nat
for b3 being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b3 = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S
for mm being Element of NAT st m = mm holds
b3 = dom ((I,mm) -TruthEval) );

Lm4: for m, n being Nat
for S being Language holds S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n)
proof end;

Lm3: for S being Language holds S -formulasOfMaxDepth 0 = AtomicFormulasOf S
proof end;

definition
let S be Language;
let m be Nat;
let w be string of S;
attr w is m -wff means :DefWff1: :: FOMODEL2:def 24
w in S -formulasOfMaxDepth m;
end;

:: deftheorem DefWff1 defines -wff FOMODEL2:def 24 :
for S being Language
for m being Nat
for w being string of S holds
( w is m -wff iff w in S -formulasOfMaxDepth m );

definition
let S be Language;
let w be string of S;
attr w is wff means :DefWff2: :: FOMODEL2:def 25
ex m being Nat st w is m -wff ;
end;

:: deftheorem DefWff2 defines wff FOMODEL2:def 25 :
for S being Language
for w being string of S holds
( w is wff iff ex m being Nat st w is m -wff );

registration
let S be Language;
cluster 0 -wff -> 0wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b1 being string of S st b1 is 0 -wff holds
b1 is 0wff
proof end;
cluster 0wff -> 0 -wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b1 being string of S st b1 is 0wff holds
b1 is 0 -wff
proof end;
let m be Nat;
cluster m -wff -> wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b1 being string of S st b1 is m -wff holds
b1 is wff
by DefWff2;
let n be Nat;
cluster m + (0 * n) -wff -> m + n -wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b1 being string of S st b1 is m + (0 * n) -wff holds
b1 is m + n -wff
proof end;
end;

registration
let S be Language;
let m be Nat;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like V192() m -wff Element of ((AllSymbolsOf S) *) \ {{}};
existence
ex b1 being string of S st b1 is m -wff
proof end;
end;

registration
let S be Language;
let m be Nat;
cluster S -formulasOfMaxDepth m -> non empty ;
coherence
not S -formulasOfMaxDepth m is empty
proof end;
end;

registration
let S be Language;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like V192() wff Element of ((AllSymbolsOf S) *) \ {{}};
existence
ex b1 being string of S st b1 is wff
proof end;
end;

definition
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let w be wff string of S;
func I -TruthEval w -> Element of BOOLEAN means :DefTruth4: :: FOMODEL2:def 26
for m being Nat st w is m -wff holds
it = ((I,m) -TruthEval) . w;
existence
ex b1 being Element of BOOLEAN st
for m being Nat st w is m -wff holds
b1 = ((I,m) -TruthEval) . w
proof end;
uniqueness
for b1, b2 being Element of BOOLEAN st ( for m being Nat st w is m -wff holds
b1 = ((I,m) -TruthEval) . w ) & ( for m being Nat st w is m -wff holds
b2 = ((I,m) -TruthEval) . w ) holds
b1 = b2
proof end;
end;

:: deftheorem DefTruth4 defines -TruthEval FOMODEL2:def 26 :
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S
for w being wff string of S
for b5 being Element of BOOLEAN holds
( b5 = I -TruthEval w iff for m being Nat st w is m -wff holds
b5 = ((I,m) -TruthEval) . w );

definition
let S be Language;
func AllFormulasOf S -> set equals :: FOMODEL2:def 27
{ w where w is string of S : ex m being Nat st w is m -wff } ;
coherence
{ w where w is string of S : ex m being Nat st w is m -wff } is set
;
end;

:: deftheorem defines AllFormulasOf FOMODEL2:def 27 :
for S being Language holds AllFormulasOf S = { w where w is string of S : ex m being Nat st w is m -wff } ;

registration
let S be Language;
cluster AllFormulasOf S -> non empty ;
coherence
not AllFormulasOf S is empty
proof end;
end;

theorem Th3: :: FOMODEL2:3
for m being Nat
for S being Language
for U being non empty set
for u being Element of U
for t being termal string of S
for I being b2,b3 -interpreter-like Function holds
( (((I,u) -TermEval) . (m + 1)) . t = (I . ((S -firstChar) . t)) . ((((I,u) -TermEval) . m) * (SubTerms t)) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . ((S -firstChar) . t)) . {} ) )
proof end;

theorem :: FOMODEL2:4
for m, n being Nat
for S being Language
for U being non empty set
for u1, u2 being Element of U
for I being b3,b4 -interpreter-like Function
for t being b1 -termal string of S holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t by Lm1;

theorem :: FOMODEL2:5
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)) by Lm28;

theorem :: FOMODEL2:6
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 Lm25;

theorem :: FOMODEL2:7
for S being Language holds S -formulasOfMaxDepth 0 = AtomicFormulasOf S by Lm3;

definition
let S be Language;
let m be Nat;
redefine func S -formulasOfMaxDepth m means :DefFormulas: :: FOMODEL2:def 28
for U being non empty set
for I being Element of U -InterpretersOf S holds it = dom ((I,m) -TruthEval);
compatibility
for b1 being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b1 = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds b1 = dom ((I,m) -TruthEval) )
proof end;
end;

:: deftheorem DefFormulas defines -formulasOfMaxDepth FOMODEL2:def 28 :
for S being Language
for m being Nat
for b3 being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b3 = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds b3 = dom ((I,m) -TruthEval) );

Lm31: 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))
proof end;

theorem Lm32: :: FOMODEL2:8
for m being Nat
for S being Language
for U being non empty set holds
( (S,U) -TruthEval m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) & ((S,U) -TruthEval) . m in Funcs ([:(U -InterpretersOf S),(S -formulasOfMaxDepth m):],BOOLEAN) )
proof end;

definition
let S be Language;
let m be Nat;
func m -ExFormulasOf S -> set equals :: FOMODEL2:def 29
{ (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum } ;
coherence
{ (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum } is set
;
func m -NorFormulasOf S -> set equals :: FOMODEL2:def 30
{ ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } ;
coherence
{ ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } is set
;
end;

:: deftheorem defines -ExFormulasOf FOMODEL2:def 29 :
for S being Language
for m being Nat holds m -ExFormulasOf S = { (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum } ;

:: deftheorem defines -NorFormulasOf FOMODEL2:def 30 :
for S being Language
for m being Nat holds m -NorFormulasOf S = { ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } ;

definition
let S be Language;
let w1, w2 be string of S;
:: original: ^
redefine func w1 ^ w2 -> string of S;
coherence
w1 ^ w2 is string of S
proof end;
end;

definition
let S be Language;
let s be Element of S;
:: original: <*
redefine func <*s*> -> string of S;
coherence
<*s*> is string of S
proof end;
end;

Lm33: 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):]
proof end;

Lm35: 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):]
proof end;

theorem Lm37: :: FOMODEL2:9
for m being Nat
for S being Language holds S -formulasOfMaxDepth (m + 1) = ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)
proof end;

theorem Th10: :: FOMODEL2:10
for S being Language holds AtomicFormulasOf S is S -prefix
proof end;

registration
let S be Language;
cluster AtomicFormulasOf S -> S -prefix set ;
coherence
for b1 being set st b1 = AtomicFormulasOf S holds
b1 is S -prefix
by Th10;
end;

registration
let S be Language;
cluster S -formulasOfMaxDepth 0 -> S -prefix set ;
coherence
for b1 being set st b1 = S -formulasOfMaxDepth 0 holds
b1 is S -prefix
proof end;
end;

definition
let S be Language;
let phi be wff string of S;
func Depth phi -> Nat means :DefDepth: :: FOMODEL2:def 31
( phi is it -wff & ( for n being Nat st phi is n -wff holds
it <= n ) );
existence
ex b1 being Nat st
( phi is b1 -wff & ( for n being Nat st phi is n -wff holds
b1 <= n ) )
proof end;
uniqueness
for b1, b2 being Nat st phi is b1 -wff & ( for n being Nat st phi is n -wff holds
b1 <= n ) & phi is b2 -wff & ( for n being Nat st phi is n -wff holds
b2 <= n ) holds
b1 = b2
proof end;
end;

:: deftheorem DefDepth defines Depth FOMODEL2:def 31 :
for S being Language
for phi being wff string of S
for b3 being Nat holds
( b3 = Depth phi iff ( phi is b3 -wff & ( for n being Nat st phi is n -wff holds
b3 <= n ) ) );

Lm16: 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 )
proof end;

Lm8: 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
proof end;

registration
let S be Language;
let m be Nat;
let phi1, phi2 be m -wff string of S;
cluster (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 -> m + 1 -wff string of S;
coherence
for b1 being string of S st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b1 is m + 1 -wff
proof end;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 -> wff string of S;
coherence
for b1 being string of S st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b1 is wff
proof end;
end;

registration
let S be Language;
let m be Nat;
let phi be m -wff string of S;
let v be literal Element of S;
cluster <*v*> ^ phi -> m + 1 -wff string of S;
coherence
for b1 being string of S st b1 = <*v*> ^ phi holds
b1 is m + 1 -wff
proof end;
end;

registration
let S be Language;
let l be literal Element of S;
let phi be wff string of S;
cluster <*l*> ^ phi -> wff string of S;
coherence
for b1 being string of S st b1 = <*l*> ^ phi holds
b1 is wff
proof end;
end;

registration
let S be Language;
let w be string of S;
let s be non relational Element of S;
cluster <*s*> ^ w -> non 0wff string of S;
coherence
for b1 being string of S st b1 = <*s*> ^ w holds
not b1 is 0wff
proof end;
end;

registration
let S be Language;
let w1, w2 be string of S;
let s be non relational Element of S;
cluster (<*s*> ^ w1) ^ w2 -> non 0wff string of S;
coherence
for b1 being string of S st b1 = (<*s*> ^ w1) ^ w2 holds
not b1 is 0wff
proof end;
end;

registration
let S be Language;
cluster TheNorSymbOf S -> non relational Element of S;
coherence
for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is relational
;
end;

registration
let S be Language;
let w be string of S;
cluster <*(TheNorSymbOf S)*> ^ w -> non 0wff string of S;
coherence
for b1 being string of S st b1 = <*(TheNorSymbOf S)*> ^ w holds
not b1 is 0wff
;
end;

registration
let S be Language;
let l be literal Element of S;
let w be string of S;
cluster <*l*> ^ w -> non 0wff string of S;
coherence
for b1 being string of S st b1 = <*l*> ^ w holds
not b1 is 0wff
;
end;

definition
let S be Language;
let w be string of S;
attr w is exal means :DefExal: :: FOMODEL2:def 32
(S -firstChar) . w is literal ;
end;

:: deftheorem DefExal defines exal FOMODEL2:def 32 :
for S being Language
for w being string of S holds
( w is exal iff (S -firstChar) . w is literal );

registration
let S be Language;
let w be string of S;
let l be literal Element of S;
cluster <*l*> ^ w -> exal string of S;
coherence
for b1 being string of S st b1 = <*l*> ^ w holds
b1 is exal
proof end;
end;

registration
let S be Language;
let m1 be non zero Nat;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like V192() m1 -wff wff exal Element of ((AllSymbolsOf S) *) \ {{}};
existence
ex b1 being m1 -wff string of S st b1 is exal
proof end;
end;

registration
let S be Language;
cluster exal -> non 0wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b1 being string of S st b1 is exal holds
not b1 is 0wff
proof end;
end;

registration
let S be Language;
let m1 be non zero Nat;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like V192() non 0wff m1 -wff wff exal Element of ((AllSymbolsOf S) *) \ {{}};
existence
not for b1 being m1 -wff exal string of S holds b1 is 0wff
proof end;
end;

registration
let S be Language;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like V192() non 0wff wff exal Element of ((AllSymbolsOf S) *) \ {{}};
existence
not for b1 being wff exal string of S holds b1 is 0wff
proof end;
end;

Lm5: for S being Language
for phi being wff string of S st not phi is 0wff holds
Depth phi <> 0
proof end;

registration
let S be Language;
let phi be non 0wff wff string of S;
cluster Depth phi -> non zero Nat;
coherence
for b1 being Nat st b1 = Depth phi holds
not b1 is empty
by Lm5;
end;

Lm30: 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
proof end;

registration
let S be Language;
let w be non 0wff wff string of S;
cluster (S -firstChar) . w -> non relational Element of S;
coherence
for b1 being Element of S st b1 = (S -firstChar) . w holds
not b1 is relational
proof end;
end;

Lm6: for m being Nat
for S being Language holds S -formulasOfMaxDepth m is S -prefix
proof end;

registration
let S be Language;
let m be Nat;
cluster S -formulasOfMaxDepth m -> S -prefix set ;
coherence
for b1 being set st b1 = S -formulasOfMaxDepth m holds
b1 is S -prefix
by Lm6;
end;

definition
let S be Language;
:: original: AllFormulasOf
redefine func AllFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}});
coherence
AllFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
proof end;
end;

registration
let S be Language;
cluster -> wff Element of AllFormulasOf S;
coherence
for b1 being Element of AllFormulasOf S holds b1 is wff
proof end;
end;

Lm11: for S being Language holds AllFormulasOf S is S -prefix
proof end;

registration
let S be Language;
cluster AllFormulasOf S -> S -prefix set ;
coherence
for b1 being set st b1 = AllFormulasOf S holds
b1 is S -prefix
by Lm11;
end;

theorem :: FOMODEL2:11
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):] by Lm33;

theorem :: FOMODEL2:12
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):] by Lm35;

Lm12: for U being non empty set holds (U -deltaInterpreter) " {1} = (U -concatenation) .: (id (1 -tuples_on U))
proof end;

theorem Th13: :: FOMODEL2:13
for U being non empty set holds (U -deltaInterpreter) " {1} = { <*u,u*> where u is Element of U : verum }
proof end;

definition
let S be Language;
:: original: TheEqSymbOf
redefine func TheEqSymbOf S -> Element of S;
coherence
TheEqSymbOf S is Element of S
;
end;

registration
let S be Language;
cluster (ar (TheEqSymbOf S)) + 2 -> zero number ;
coherence
for b1 being number st b1 = (ar (TheEqSymbOf S)) + 2 holds
b1 is empty
proof end;
cluster (abs (ar (TheEqSymbOf S))) - 2 -> zero number ;
coherence
for b1 being number st b1 = (abs (ar (TheEqSymbOf S))) - 2 holds
b1 is empty
proof end;
end;

theorem Th14: :: FOMODEL2:14
for S being Language
for U being non empty set
for phi being 0wff string of S
for I being b1,b2 -interpreter-like Function holds
( ( (S -firstChar) . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) ) & ( (S -firstChar) . phi = TheEqSymbOf S implies I -AtomicEval phi = (U -deltaInterpreter) . ((I -TermEval) * (SubTerms phi)) ) )
proof end;

theorem :: FOMODEL2:15
for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for phi being 0wff string of S st (S -firstChar) . phi = TheEqSymbOf S holds
( I -AtomicEval phi = 1 iff (I -TermEval) . ((SubTerms phi) . 1) = (I -TermEval) . ((SubTerms phi) . 2) )
proof end;

registration
let S be Language;
let m be Nat;
cluster m -ExFormulasOf S -> non empty set ;
coherence
for b1 being set st b1 = m -ExFormulasOf S holds
not b1 is empty
proof end;
end;

registration
let S be Language;
let m be Nat;
cluster m -NorFormulasOf S -> non empty set ;
coherence
for b1 being set st b1 = m -NorFormulasOf S holds
not b1 is empty
proof end;
end;

definition
let S be Language;
let m be Nat;
:: original: -NorFormulasOf
redefine func m -NorFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}});
coherence
m -NorFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
proof end;
end;

registration
let S be Language;
let w be exal string of S;
cluster (S -firstChar) . w -> literal Element of S;
coherence
for b1 being Element of S st b1 = (S -firstChar) . w holds
b1 is literal
by DefExal;
end;

registration
let S be Language;
let m be Nat;
cluster -> non exal Element of m -NorFormulasOf S;
coherence
for b1 being Element of m -NorFormulasOf S holds not b1 is exal
proof end;
end;

Lm14: 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
proof end;

Lm44: for S being Language
for l being literal Element of S
for phi1 being wff string of S holds Depth (<*l*> ^ phi1) > Depth phi1
proof end;

definition
let S be Language;
let m be Nat;
:: original: -ExFormulasOf
redefine func m -ExFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}});
coherence
m -ExFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})
proof end;
end;

registration
let S be Language;
let m be Nat;
cluster -> exal Element of m -ExFormulasOf S;
coherence
for b1 being Element of m -ExFormulasOf S holds b1 is exal
proof end;
end;

Lm13: 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
proof end;

registration
let S be Language;
cluster non literal Element of AllSymbolsOf S;
existence
not for b1 being Element of S holds b1 is literal
proof end;
end;

registration
let S be Language;
let w be string of S;
let s be non literal Element of S;
cluster <*s*> ^ w -> non exal string of S;
coherence
for b1 being string of S st b1 = <*s*> ^ w holds
not b1 is exal
proof end;
end;

registration
let S be Language;
let w1, w2 be string of S;
let s be non literal Element of S;
cluster (<*s*> ^ w1) ^ w2 -> non exal string of S;
coherence
for b1 being string of S st b1 = (<*s*> ^ w1) ^ w2 holds
not b1 is exal
proof end;
end;

registration
let S be Language;
cluster TheNorSymbOf S -> non literal Element of S;
coherence
for b1 being Element of S st b1 = TheNorSymbOf S holds
not b1 is literal
;
end;

theorem Th16: :: FOMODEL2:16
for S being Language
for phi being wff string of S holds phi in AllFormulasOf S
proof end;

Lm39: 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 )
proof end;

Lm40: for S being Language
for phi1, phi2 being wff string of S holds Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
proof end;

notation
let S be Language;
let m be Nat;
let w be string of S;
antonym m -nonwff w for m -wff ;
end;

registration
let m be Nat;
let S be Language;
cluster non m -wff -> m -nonwff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b1 being string of S st not b1 is m -wff holds
not b1 is m -wff
;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 -> max ((Depth phi1),(Depth phi2)) -nonwff string of S;
coherence
for b1 being string of S st b1 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
not b1 is max ((Depth phi1),(Depth phi2)) -wff
proof end;
end;

registration
let S be Language;
let phi be wff string of S;
let l be literal Element of S;
cluster <*l*> ^ phi -> Depth phi -nonwff string of S;
coherence
for b1 being string of S st b1 = <*l*> ^ phi holds
not b1 is Depth phi -wff
proof end;
end;

registration
let S be Language;
let phi be wff string of S;
let l be literal Element of S;
cluster <*l*> ^ phi -> 1 + (Depth phi) -wff string of S;
coherence
for b1 being string of S st b1 = <*l*> ^ phi holds
b1 is 1 + (Depth phi) -wff
proof end;
end;

Lm46: 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
proof end;

registration
let S be Language;
let U be non empty set ;
cluster -> OwnSymbolsOf S -defined Element of U -InterpretersOf S;
coherence
for b1 being Element of U -InterpretersOf S holds b1 is OwnSymbolsOf S -defined
proof end;
end;

registration
let S be Language;
let U be non empty set ;
cluster Relation-like OwnSymbolsOf S -defined Function-like Function-yielding S,U -interpreter-like Element of U -InterpretersOf S;
existence
ex b1 being Element of U -InterpretersOf S st b1 is OwnSymbolsOf S -defined
proof end;
end;

registration
let S be Language;
let U be non empty set ;
cluster OwnSymbolsOf S -defined -> OwnSymbolsOf S -defined total Element of U -InterpretersOf S;
coherence
for b1 being OwnSymbolsOf S -defined Element of U -InterpretersOf S holds b1 is total
proof end;
end;

definition
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let x be literal Element of S;
let u be Element of U;
:: original: ReassignIn
redefine func (x,u) ReassignIn I -> Element of U -InterpretersOf S;
coherence
(x,u) ReassignIn I is Element of U -InterpretersOf S
proof end;
end;

Lm41: 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]
proof end;

Lm43: 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 )
proof end;

Lm47: 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 )
proof end;

Lm38: 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 ) )
proof end;

Lm45: 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 ) )
proof end;

definition
let S be Language;
let w be string of S;
func xnot w -> string of S equals :: FOMODEL2:def 33
(<*(TheNorSymbOf S)*> ^ w) ^ w;
coherence
(<*(TheNorSymbOf S)*> ^ w) ^ w is string of S
;
end;

:: deftheorem defines xnot FOMODEL2:def 33 :
for S being Language
for w being string of S holds xnot w = (<*(TheNorSymbOf S)*> ^ w) ^ w;

registration
let S be Language;
let m be Nat;
let phi be m -wff string of S;
cluster xnot phi -> m + 1 -wff string of S;
coherence
for b1 being string of S st b1 = xnot phi holds
b1 is m + 1 -wff
;
end;

registration
let S be Language;
let phi be wff string of S;
cluster xnot phi -> wff string of S;
coherence
for b1 being string of S st b1 = xnot phi holds
b1 is wff
;
end;

registration
let S be Language;
cluster TheEqSymbOf S -> non own Element of S;
coherence
for b1 being Element of S st b1 = TheEqSymbOf S holds
not b1 is own
proof end;
end;

definition
let S be Language;
let X be set ;
attr X is S -mincover means :DefCover: :: FOMODEL2:def 34
for phi being wff string of S holds
( phi in X iff not xnot phi in X );
end;

:: deftheorem DefCover defines -mincover FOMODEL2:def 34 :
for S being Language
for X being set holds
( X is S -mincover iff for phi being wff string of S holds
( phi in X iff not xnot phi in X ) );

theorem Th17: :: FOMODEL2:17
for S being Language
for l being literal Element of S
for phi1, phi2 being wff string of S holds
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 + (max ((Depth phi1),(Depth phi2))) & Depth (<*l*> ^ phi1) = (Depth phi1) + 1 )
proof end;

theorem :: FOMODEL2:18
for m being Nat
for S being Language
for phi being wff string of S st Depth phi = m + 1 holds
( ( phi is exal implies phi in m -ExFormulasOf S ) & ( phi in m -ExFormulasOf S implies phi is exal ) & ( not phi is exal implies phi in m -NorFormulasOf S ) & ( phi in m -NorFormulasOf S implies not phi is exal ) ) by Lm14, Lm13;

theorem :: FOMODEL2:19
for S being Language
for U being non empty set
for l being literal Element of S
for phi, phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( ( I -TruthEval (<*l*> ^ phi) = TRUE implies ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 ) & ( ex u being Element of U st ((l,u) ReassignIn I) -TruthEval phi = 1 implies I -TruthEval (<*l*> ^ phi) = TRUE ) & ( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE implies ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) ) & ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE implies I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE ) ) by Lm47, Lm45;

theorem Th20: :: FOMODEL2:20
for m being Nat
for S being Language
for U being non empty set
for u being Element of U
for I being b2,b3 -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m)
proof end;

theorem Th21: :: FOMODEL2:21
for S being Language
for U being non empty set
for t being termal string of S
for I being b1,b2 -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))
proof end;

definition
let S be Language;
let phi be wff string of S;
set F = S -firstChar ;
set d = Depth phi;
set s = (S -firstChar) . phi;
set L = LettersOf S;
set N = TheNorSymbOf S;
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
defpred S1[ set ] means ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & $1 = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p );
func SubWffsOf phi -> set means :DefSub1: :: FOMODEL2:def 35
ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & it = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) if not phi is 0wff
otherwise it = [phi,{}];
existence
( ( not phi is 0wff implies ex b1 being set ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b1 = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) & ( phi is 0wff implies ex b1 being set st b1 = [phi,{}] ) )
proof end;
uniqueness
for b1, b2 being set holds
( ( not phi is 0wff & ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b1 = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) & ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b2 = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) implies b1 = b2 ) & ( phi is 0wff & b1 = [phi,{}] & b2 = [phi,{}] implies b1 = b2 ) )
proof end;
consistency
for b1 being set holds verum
;
end;

:: deftheorem DefSub1 defines SubWffsOf FOMODEL2:def 35 :
for S being Language
for phi being wff string of S
for b3 being set holds
( ( not phi is 0wff implies ( b3 = SubWffsOf phi iff ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b3 = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) ) & ( phi is 0wff implies ( b3 = SubWffsOf phi iff b3 = [phi,{}] ) ) );

definition
let S be Language;
let phi be wff string of S;
set IT = SubWffsOf phi;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
func head phi -> wff string of S equals :: FOMODEL2:def 36
(SubWffsOf phi) `1 ;
coherence
(SubWffsOf phi) `1 is wff string of S
proof end;
func tail phi -> Element of (AllSymbolsOf S) * equals :: FOMODEL2:def 37
(SubWffsOf phi) `2 ;
coherence
(SubWffsOf phi) `2 is Element of (AllSymbolsOf S) *
proof end;
end;

:: deftheorem defines head FOMODEL2:def 36 :
for S being Language
for phi being wff string of S holds head phi = (SubWffsOf phi) `1 ;

:: deftheorem defines tail FOMODEL2:def 37 :
for S being Language
for phi being wff string of S holds tail phi = (SubWffsOf phi) `2 ;

registration
let S be Language;
let m be Nat;
cluster (S -formulasOfMaxDepth m) \ (AllFormulasOf S) -> empty set ;
coherence
for b1 being set st b1 = (S -formulasOfMaxDepth m) \ (AllFormulasOf S) holds
b1 is empty
proof end;
end;

registration
let S be Language;
cluster (AtomicFormulasOf S) \ (AllFormulasOf S) -> empty set ;
coherence
for b1 being set st b1 = (AtomicFormulasOf S) \ (AllFormulasOf S) holds
b1 is empty
proof end;
end;

theorem :: FOMODEL2:22
for S being Language
for l being literal Element of S
for phi1, phi2 being wff string of S holds
( Depth (<*l*> ^ phi1) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 ) by Lm44, Lm39;

theorem Th23: :: FOMODEL2:23
for x being set
for S being Language
for p2 being FinSequence
for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) )
proof end;

registration
let S be Language;
let m1 be non zero Nat;
cluster non empty Relation-like Function-like finite FinSequence-like FinSubsequence-like V192() non 0wff m1 -wff wff non exal Element of ((AllSymbolsOf S) *) \ {{}};
existence
not for b1 being non 0wff m1 -wff string of S holds b1 is exal
proof end;
end;

registration
let S be Language;
let phi be wff exal string of S;
cluster tail phi -> empty set ;
coherence
for b1 being set st b1 = tail phi holds
b1 is empty
proof end;
end;

Lm49: 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
proof end;

definition
let S be Language;
let phi be non 0wff wff non exal string of S;
:: original: tail
redefine func tail phi -> wff string of S;
coherence
tail phi is wff string of S
proof end;
end;

registration
let S be Language;
let phi be non 0wff wff non exal string of S;
cluster tail phi -> wff string of S;
coherence
for b1 being string of S st b1 = tail phi holds
b1 is wff
;
end;

registration
let S be Language;
let phi0 be 0wff string of S;
identify head phi0 with phi0 null ;
compatibility
head phi0 = phi0 null
proof end;
end;

registration
let S be Language;
let phi be non 0wff wff non exal string of S;
cluster ((S -firstChar) . phi) \+\ (TheNorSymbOf S) -> empty set ;
coherence
for b1 being set st b1 = ((S -firstChar) . phi) \+\ (TheNorSymbOf S) holds
b1 is empty
proof end;
end;

Lm50: 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 )
proof end;

registration
let m be Nat;
let S be Language;
let phi be m + 1 -wff string of S;
cluster head phi -> m -wff string of S;
coherence
for b1 being string of S st b1 = head phi holds
b1 is m -wff
proof end;
end;

registration
let m be Nat;
let S be Language;
let phi be non 0wff m + 1 -wff non exal string of S;
cluster tail phi -> m -wff string of S;
coherence
for b1 being string of S st b1 = tail phi holds
b1 is m -wff
by Lm50;
end;

theorem Th24: :: FOMODEL2:24
for m being Nat
for S being Language
for U being non empty set
for I being Element of U -InterpretersOf S holds (I,m) -TruthEval in Funcs ((S -formulasOfMaxDepth m),BOOLEAN)
proof end;

Lm51: 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
proof end;

registration
let S be Language;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
let phi0 be 0wff string of S;
identify I -TruthEval phi0 with I -AtomicEval phi0;
compatibility
I -TruthEval phi0 = I -AtomicEval phi0
by Lm51;
identify I -AtomicEval phi0 with I -TruthEval phi0;
compatibility
I -AtomicEval phi0 = I -TruthEval phi0
;
end;

registration
let S be Language;
cluster non literal ofAtomicFormula Element of AllSymbolsOf S;
existence
not for b1 being ofAtomicFormula Element of S holds b1 is literal
proof end;
end;

Lm52: 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 *)
proof end;

theorem :: FOMODEL2:25
for S being Language
for U being non empty set
for p being FinSequence
for u being Element of U
for l2 being literal Element of S
for I being b1,b2 -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
proof end;

definition
let X be set ;
let S be Language;
let s be Element of S;
attr s is X -occurring means :DefOccur: :: FOMODEL2:def 38
s in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ X);
end;

:: deftheorem DefOccur defines -occurring FOMODEL2:def 38 :
for X being set
for S being Language
for s being Element of S holds
( s is X -occurring iff s in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ X) );

definition
let S be Language;
let s be Element of S;
let X be set ;
attr X is s -containing means :: FOMODEL2:def 39
s in SymbolsOf (((AllSymbolsOf S) *) \ ({{}} /\ X));
end;

:: deftheorem defines -containing FOMODEL2:def 39 :
for S being Language
for s being Element of S
for X being set holds
( X is s -containing iff s in SymbolsOf (((AllSymbolsOf S) *) \ ({{}} /\ X)) );

notation
let X be set ;
let S be Language;
let s be Element of S;
antonym X -absent s for X -occurring ;
end;

notation
let S be Language;
let s be Element of S;
let X be set ;
antonym s -free X for s -containing ;
end;

registration
let X be finite set ;
let S be Language;
cluster literal non operational non relational termal own ofAtomicFormula X -absent Element of AllSymbolsOf S;
existence
not for b1 being literal Element of S holds b1 is X -occurring
proof end;
end;

Lm53: for S being Language
for w being string of S st w is termal holds
(rng w) /\ (LettersOf S) <> {}
proof end;

registration
let S be Language;
let t be termal string of S;
cluster (rng t) /\ (LettersOf S) -> non empty set ;
coherence
for b1 being set st b1 = (rng t) /\ (LettersOf S) holds
not b1 is empty
by Lm53;
end;

Lm54: for S being Language
for w being string of S st w is wff holds
(rng w) /\ (LettersOf S) <> {}
proof end;

registration
let S be Language;
let phi be wff string of S;
cluster (rng phi) /\ (LettersOf S) -> non empty set ;
coherence
for b1 being set st b1 = (rng phi) /\ (LettersOf S) holds
not b1 is empty
by Lm54;
end;

registration
let B be set ;
let S be Language;
let A be Subset of B;
cluster A -occurring -> B -occurring Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is A -occurring holds
b1 is B -occurring
proof end;
end;

registration
let A, B be set ;
let S be Language;
cluster A null B -absent -> A /\ B -absent Element of AllSymbolsOf S;
coherence
for b1 being Element of S st not b1 is A null B -occurring holds
not b1 is A /\ B -occurring
;
end;

registration
let F be finite set ;
let A be set ;
let S be Language;
cluster F -absent A -absent -> F -absent A \/ F -absent Element of AllSymbolsOf S;
coherence
for b1 being F -absent Element of S st not b1 is A -occurring holds
not b1 is A \/ F -occurring
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster (OwnSymbolsOf S) \ (dom I) -> empty set ;
coherence
for b1 being set st b1 = (OwnSymbolsOf S) \ (dom I) holds
b1 is empty
proof end;
end;

theorem :: FOMODEL2:26
for S being Language
for U being non empty set
for l being literal Element of S
for I being b1,b2 -interpreter-like Function ex u being Element of U st
( u = (I . l) . {} & (l,u) ReassignIn I = I )
proof end;

definition
let S be Language;
let X be set ;
attr X is S -covering means :: FOMODEL2:def 40
for phi being wff string of S holds
( phi in X or xnot phi in X );
end;

:: deftheorem defines -covering FOMODEL2:def 40 :
for S being Language
for X being set holds
( X is S -covering iff for phi being wff string of S holds
( phi in X or xnot phi in X ) );

registration
let S be Language;
cluster S -mincover -> S -covering set ;
coherence
for b1 being set st b1 is S -mincover holds
b1 is S -covering
proof end;
end;

registration
let U be non empty set ;
let S be Language;
let phi be non 0wff wff non exal string of S;
let I be Element of U -InterpretersOf S;
cluster (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) -> empty set ;
coherence
for b1 being set st b1 = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds
b1 is empty
proof end;
end;

definition
let S be Language;
func ExFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}}) equals :: FOMODEL2:def 41
{ phi where phi is string of S : ( phi is wff & phi is exal ) } ;
coherence
{ phi where phi is string of S : ( phi is wff & phi is exal ) } is Subset of (((AllSymbolsOf S) *) \ {{}})
proof end;
end;

:: deftheorem defines ExFormulasOf FOMODEL2:def 41 :
for S being Language holds ExFormulasOf S = { phi where phi is string of S : ( phi is wff & phi is exal ) } ;

registration
let S be Language;
cluster ExFormulasOf S -> non empty set ;
coherence
for b1 being set st b1 = ExFormulasOf S holds
not b1 is empty
proof end;
end;

registration
let S be Language;
cluster -> wff exal Element of ExFormulasOf S;
coherence
for b1 being Element of ExFormulasOf S holds
( b1 is exal & b1 is wff )
proof end;
end;

registration
let S be Language;
cluster -> wff Element of ExFormulasOf S;
coherence
for b1 being Element of ExFormulasOf S holds b1 is wff
;
end;

registration
let S be Language;
cluster -> exal Element of ExFormulasOf S;
coherence
for b1 being Element of ExFormulasOf S holds b1 is exal
;
end;

registration
let S be Language;
cluster (ExFormulasOf S) \ (AllFormulasOf S) -> empty set ;
coherence
for b1 being set st b1 = (ExFormulasOf S) \ (AllFormulasOf S) holds
b1 is empty
proof end;
end;

registration
let U be non empty set ;
let S1 be Language;
let S2 be S1 -extending Language;
cluster Relation-like Function-like S2,U -interpreter-like -> S1,U -interpreter-like set ;
coherence
for b1 being Function st b1 is S2,U -interpreter-like holds
b1 is S1,U -interpreter-like
proof end;
end;

registration
let U be non empty set ;
let S1 be Language;
let S2 be S1 -extending Language;
let I be S2,U -interpreter-like Function;
cluster I | (OwnSymbolsOf S1) -> S1,U -interpreter-like Function;
coherence
for b1 being Function st b1 = I | (OwnSymbolsOf S1) holds
b1 is S1,U -interpreter-like
;
end;

registration
let U be non empty set ;
let S1 be Language;
let S2 be S1 -extending Language;
let I1 be Element of U -InterpretersOf S1;
let I2 be S2,U -interpreter-like Function;
cluster I2 +* I1 -> S2,U -interpreter-like ;
coherence
I2 +* I1 is S2,U -interpreter-like
proof end;
end;

definition
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X be set ;
attr X is I -satisfied means :DefSat: :: FOMODEL2:def 42
for phi being wff string of S st phi in X holds
I -TruthEval phi = 1;
end;

:: deftheorem DefSat defines -satisfied FOMODEL2:def 42 :
for U being non empty set
for S being Language
for I being Element of U -InterpretersOf S
for X being set holds
( X is I -satisfied iff for phi being wff string of S st phi in X holds
I -TruthEval phi = 1 );

definition
let S be Language;
let U be non empty set ;
let X be set ;
let I be Element of U -InterpretersOf S;
attr I is X -satisfying means :DefSat2: :: FOMODEL2:def 43
X is I -satisfied ;
end;

:: deftheorem DefSat2 defines -satisfying FOMODEL2:def 43 :
for S being Language
for U being non empty set
for X being set
for I being Element of U -InterpretersOf S holds
( I is X -satisfying iff X is I -satisfied );

registration
let U be non empty set ;
let S be Language;
let e be empty set ;
let I be Element of U -InterpretersOf S;
cluster e null I -> I -satisfied ;
coherence
e null I is I -satisfied
proof end;
end;

registration
let X be set ;
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
cluster I -satisfied Element of bool X;
existence
ex b1 being Subset of X st b1 is I -satisfied
proof end;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
cluster I -satisfied set ;
existence
ex b1 being set st b1 is I -satisfied
proof end;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X be I -satisfied set ;
cluster -> I -satisfied Element of bool X;
coherence
for b1 being Subset of X holds b1 is I -satisfied
proof end;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X, Y be I -satisfied set ;
cluster X \/ Y -> I -satisfied ;
coherence
X \/ Y is I -satisfied
proof end;
end;

registration
let U be non empty set ;
let S be Language;
let I be Element of U -InterpretersOf S;
let X be I -satisfied set ;
cluster I null X -> X -satisfying Element of U -InterpretersOf S;
coherence
for b1 being Element of U -InterpretersOf S st b1 = I null X holds
b1 is X -satisfying
by DefSat2;
end;

definition
let S be Language;
let X be set ;
attr X is S -correct means :SeqCorr: :: FOMODEL2:def 44
for U being non empty set
for I being Element of U -InterpretersOf S
for x being b2 -satisfied set
for phi being wff string of S st [x,phi] in X holds
I -TruthEval phi = 1;
end;

:: deftheorem SeqCorr defines -correct FOMODEL2:def 44 :
for S being Language
for X being set holds
( X is S -correct iff for U being non empty set
for I being Element of U -InterpretersOf S
for x being b4 -satisfied set
for phi being wff string of S st [x,phi] in X holds
I -TruthEval phi = 1 );

registration
let S be Language;
cluster {} null S -> S -correct ;
coherence
{} null S is S -correct
proof end;
end;

registration
let S be Language;
let X be set ;
cluster S -correct Element of bool X;
existence
ex b1 being Subset of X st b1 is S -correct
proof end;
end;

theorem :: FOMODEL2:27
for S being Language
for U being non empty set
for phi being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval phi = 1 iff {phi} is I -satisfied )
proof end;

theorem :: FOMODEL2:28
for S being Language
for s being Element of S
for w being string of S holds
( s is {w} -occurring iff s in rng w )
proof end;

registration
let U be non empty set ;
let S be Language;
let phi1, phi2 be wff string of S;
let I be Element of U -InterpretersOf S;
cluster (I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) -> empty set ;
coherence
for b1 being set st b1 = (I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) holds
b1 is empty
proof end;
end;

registration
let S be Language;
let phi be wff string of S;
let U be non empty set ;
let I be Element of U -InterpretersOf S;
cluster (I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) -> empty set ;
coherence
for b1 being set st b1 = (I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) holds
b1 is empty
proof end;
end;

definition
let X be set ;
let S be Language;
let phi be wff string of S;
attr phi is X -implied means :: FOMODEL2:def 45
for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1;
end;

:: deftheorem defines -implied FOMODEL2:def 45 :
for X being set
for S being Language
for phi being wff string of S holds
( phi is X -implied iff for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1 );