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

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 (),BOOLEAN equals :: FOMODEL2:def 1
chi ((() .: (id ())),());
coherence
chi ((() .: (id ())),()) is Function of (),BOOLEAN
;
end;

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

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:3;
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 :Def2: :: FOMODEL2:def 2
it is Function of (|.(ar s).| -tuples_on U),BOOLEAN if s is relational
otherwise it is Function of (|.(ar s).| -tuples_on U),U;
existence
( ( s is relational implies ex b1 being set st b1 is Function of (|.(ar s).| -tuples_on U),BOOLEAN ) & ( not s is relational implies ex b1 being set st b1 is Function of (|.(ar s).| -tuples_on U),U ) )
proof end;
consistency
for b1 being set holds verum
;
end;

:: deftheorem Def2 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 (|.(ar s).| -tuples_on U),BOOLEAN ) ) & ( not s is relational implies ( b4 is Interpreter of s,U iff b4 is Function of (|.(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 (|.(ar s).| -tuples_on U),();
coherence
for b1 being Interpreter of s,U holds b1 is Function of (|.(ar s).| -tuples_on U),()
proof end;
end;

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

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

::###############################################################
::###############################################################
::###############################################################
::# Interpreter of a Language.
definition
let S be Language;
let U be non empty set ;
mode Interpreter of S,U -> Function means :Def3: :: 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 Def3 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 :Def4: :: FOMODEL2:def 4
( f is Interpreter of S,U & f is Function-yielding );
end;

:: deftheorem Def4 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 ;
coherence
for b1 being Function st b1 is S,U -interpreter-like holds
b1 is Function-yielding
;
end;

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

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

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

by Lm1;

registration
let S be Language;
let U be non empty 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 .--> ());
coherence
f +* (x .--> ()) 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 .--> ());

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 for 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 V171() for 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
end;

:: deftheorem FOMODEL2:def 7 :
canceled;

registration
let f be Function-yielding Function;
let g be empty Function;
cluster ^^^f,g__ -> empty ;
coherence
^^^f,g__ is empty
;
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 for 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;
coherence ;
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 for FinSequence of E;
coherence
for b1 being FinSequence of E st b1 = h * p holds
b1 is n -element
;
end;

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 |.(ar t).| -tuples_on U = dom (I . (() . t))

by FUNCT_2:def 1;

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

Lm4: for S being Language
for U being non empty set
for I being b1,b2 -interpreter-like Function
for xx being Function of (),U holds
( ^^^(I * ()),^^^xx,()____ is Element of Funcs ((),U) & AllTermsOf S c= dom (I * ()) )

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 -> sequence of (Funcs ((),U)) means :Def7: :: FOMODEL2:def 8
( it . 0 = () --> u & ( for mm being Element of NAT holds it . (mm + 1) = ^^^(I * ()),^^^(it . mm),()____ ) );
existence
ex b1 being sequence of (Funcs ((),U)) st
( b1 . 0 = () --> u & ( for mm being Element of NAT holds b1 . (mm + 1) = ^^^(I * ()),^^^(b1 . mm),()____ ) )
proof end;
uniqueness
for b1, b2 being sequence of (Funcs ((),U)) st b1 . 0 = () --> u & ( for mm being Element of NAT holds b1 . (mm + 1) = ^^^(I * ()),^^^(b1 . mm),()____ ) & b2 . 0 = () --> u & ( for mm being Element of NAT holds b2 . (mm + 1) = ^^^(I * ()),^^^(b2 . mm),()____ ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 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 sequence of (Funcs ((),U)) holds
( b5 = (I,u) -TermEval iff ( b5 . 0 = () --> u & ( for mm being Element of NAT holds b5 . (mm + 1) = ^^^(I * ()),^^^(b5 . mm),()____ ) ) );

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 . (() . t)) . ((((I,u) -TermEval) . mm) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (mm + 1)) . t = (I . (() . t)) . {} ) )

proof end;

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

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 :Def8: :: FOMODEL2:def 9
for u1 being Element of U
for mm being Element of NAT st t in () . 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 () . 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 () . mm holds
b1 = (((I,u1) -TermEval) . (mm + 1)) . t ) & ( for u1 being Element of U
for mm being Element of NAT st t in () . mm holds
b2 = (((I,u1) -TermEval) . (mm + 1)) . t ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 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 () . 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 (),U means :Def9: :: FOMODEL2:def 10
for t being Element of AllTermsOf S holds it . t = I -TermEval t;
existence
ex b1 being Function of (),U st
for t being Element of AllTermsOf S holds b1 . t = I -TermEval t
proof end;
uniqueness
for b1, b2 being Function of (),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 Def9 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 (),U holds
( b4 = I -TermEval iff for t being Element of AllTermsOf S holds b4 . t = I -TermEval t );

::############### Semantics of 0wff formulas (propositions) ############
::#########################################################################
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 +* (() .--> );
coherence
I +* (() .--> ) 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 +* (() .--> );

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 :Def11: :: FOMODEL2:def 12
x = I === ;
end;

:: deftheorem Def11 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 for Function;
coherence
for b1 being Function st b1 = I === holds
b1 is I -extension
;
coherence
for b1 being set st b1 is I -extension holds
b1 is Function-like
;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
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 ===) . (() . phi)) . (() * (SubTerms phi));
coherence
((I ===) . (() . phi)) . (() * (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 ===) . (() . phi)) . (() * (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;

::###### Semantics of formulas (evaluation of any wff string) ##########
::######################################################################
registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster I | () -> PFuncs ((U *),()) -valued for Function;
coherence
for b1 being Function st b1 = I | () holds
b1 is PFuncs ((U *),()) -valued
proof end;
cluster I | () -> S,U -interpreter-like for Function;
coherence
for b1 being Function st b1 = I | () 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;
coherence
for b1 being OwnSymbolsOf S -defined Relation st b1 = I | () 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 ((),(PFuncs ((U *),()))) : f is S,U -interpreter-like } ;
coherence
{ f where f is Element of Funcs ((),(PFuncs ((U *),()))) : 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 ((),(PFuncs ((U *),()))) : 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 ((),(PFuncs ((U *),()))));
coherence
U -InterpretersOf S is Subset of (Funcs ((),(PFuncs ((U *),()))))
proof end;
end;

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

registration
let S be Language;
let U be non empty set ;
cluster -> S,U -interpreter-like for 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 [:(),():],BOOLEAN means :Def14: :: 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 [:(),():],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 [:(),():],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 Def14 defines -TruthEval FOMODEL2:def 15 :
for S being Language
for U being non empty set
for b3 being Function of [:(),():],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 [:(),((() *) \ ):],BOOLEAN;
let phi be Element of (() *) \ ;
func f -ExFunctor (I,phi) -> Element of BOOLEAN equals :Def15: :: 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 Def15 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 [:(),((() *) \ ):],BOOLEAN
for phi being Element of (() *) \ 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 ([:(),((() *) \ ):],BOOLEAN);
func ExIterator g -> PartFunc of [:(),((() *) \ ):],BOOLEAN means :Def16: :: FOMODEL2:def 17
( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ 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 (() *) \ st [x,y] in dom it holds
it . (x,y) = g -ExFunctor (x,y) ) );
existence
ex b1 being PartFunc of [:(),((() *) \ ):],BOOLEAN st
( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ 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 (() *) \ st [x,y] in dom b1 holds
b1 . (x,y) = g -ExFunctor (x,y) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(),((() *) \ ):],BOOLEAN st ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ 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 (() *) \ 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 (() *) \ 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 (() *) \ st [x,y] in dom b2 holds
b2 . (x,y) = g -ExFunctor (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines ExIterator FOMODEL2:def 17 :
for S being Language
for U being non empty set
for g being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN)
for b4 being PartFunc of [:(),((() *) \ ):],BOOLEAN holds
( b4 = ExIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ 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 (() *) \ 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 [:(),((() *) \ ):],BOOLEAN;
let I be Element of U -InterpretersOf S;
let phi be Element of (() *) \ ;
func f -NorFunctor (I,phi) -> Element of BOOLEAN equals :Def17: :: FOMODEL2:def 18
TRUE if ex w1, w2 being Element of (() *) \ st
( [I,w1] in dom f & f . (I,w1) = FALSE & f . (I,w2) = FALSE & phi = (<*()*> ^ w1) ^ w2 )
otherwise FALSE ;
coherence
( ( ex w1, w2 being Element of (() *) \ st
( [I,w1] in dom f & f . (I,w1) = FALSE & f . (I,w2) = FALSE & phi = (<*()*> ^ w1) ^ w2 ) implies TRUE is Element of BOOLEAN ) & ( ( for w1, w2 being Element of (() *) \ holds
( not [I,w1] in dom f or not f . (I,w1) = FALSE or not f . (I,w2) = FALSE or not phi = (<*()*> ^ w1) ^ w2 ) ) implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
end;

:: deftheorem Def17 defines -NorFunctor FOMODEL2:def 18 :
for S being Language
for U being non empty set
for f being PartFunc of [:(),((() *) \ ):],BOOLEAN
for I being Element of U -InterpretersOf S
for phi being Element of (() *) \ holds
( ( ex w1, w2 being Element of (() *) \ st
( [I,w1] in dom f & f . (I,w1) = FALSE & f . (I,w2) = FALSE & phi = (<*()*> ^ w1) ^ w2 ) implies f -NorFunctor (I,phi) = TRUE ) & ( ( for w1, w2 being Element of (() *) \ holds
( not [I,w1] in dom f or not f . (I,w1) = FALSE or not f . (I,w2) = FALSE or not phi = (<*()*> ^ w1) ^ w2 ) ) implies f -NorFunctor (I,phi) = FALSE ) );

::# The inelegant specification [I,w1] in dom f above is needed because
::# of a general problem with the . functor Despite the ideal policy of
::# separating the definition of well-formedness and truth value respectively
::# in NorIterator and -NorFunctor, one is obliged to repeat the specification
::# because the . functor adopts {} as return value for indefinite arguments
::# (see FUNCT_1:def 2) Sadly, {} is also the set conventionally chosen to
::# represent FALSE (and many other things), so we cannot resolve ambiguity
::# between a meaningless argument and a false argument, and are forced to
::# add the statement about the argument effectively belonging to the domain.
::# An alternative could have been to recode truth values in e.g. 1=true,
::# 2=false, but that could have been too much of a breakthrough. Thus in
::# general, when one has to choose an arbitrary convention to represent
::# things, I feel it would be better to avoid functions with 0={} in their
::# ranges; sadly this does not happen in many cases (see eg the chi functor),
::# probably because of the load of intuitive, symbolic, representative
::# imagery that 0 and emptiness symbols convey.
definition
let S be Language;
let U be non empty set ;
let g be Element of PFuncs ([:(),((() *) \ ):],BOOLEAN);
func NorIterator g -> PartFunc of [:(),((() *) \ ):],BOOLEAN means :Def18: :: FOMODEL2:def 19
( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom it iff ex phi1, phi2 being Element of (() *) \ st
( y = (<*()*> ^ 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 (() *) \ st [x,y] in dom it holds
it . (x,y) = g -NorFunctor (x,y) ) );
existence
ex b1 being PartFunc of [:(),((() *) \ ):],BOOLEAN st
( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom b1 iff ex phi1, phi2 being Element of (() *) \ st
( y = (<*()*> ^ 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 (() *) \ st [x,y] in dom b1 holds
b1 . (x,y) = g -NorFunctor (x,y) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(),((() *) \ ):],BOOLEAN st ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom b1 iff ex phi1, phi2 being Element of (() *) \ st
( y = (<*()*> ^ 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 (() *) \ 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 (() *) \ holds
( [x,y] in dom b2 iff ex phi1, phi2 being Element of (() *) \ st
( y = (<*()*> ^ 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 (() *) \ st [x,y] in dom b2 holds
b2 . (x,y) = g -NorFunctor (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines NorIterator FOMODEL2:def 19 :
for S being Language
for U being non empty set
for g being Element of PFuncs ([:(),((() *) \ ):],BOOLEAN)
for b4 being PartFunc of [:(),((() *) \ ):],BOOLEAN holds
( b4 = NorIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of (() *) \ holds
( [x,y] in dom b4 iff ex phi1, phi2 being Element of (() *) \ st
( y = (<*()*> ^ 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 (() *) \ 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 -> sequence of (PFuncs ([:(),((() *) \ ):],BOOLEAN)) means :Def19: :: 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 sequence of (PFuncs ([:(),((() *) \ ):],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 sequence of (PFuncs ([:(),((() *) \ ):],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 Def19 defines -TruthEval FOMODEL2:def 20 :
for S being Language
for U being non empty set
for b3 being sequence of (PFuncs ([:(),((() *) \ ):],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 | () 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 ([:(),((() *) \ ):],BOOLEAN) means :Def20: :: 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 ([:(),((() *) \ ):],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 ([:(),((() *) \ ):],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 Def20 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 ([:(),((() *) \ ):],BOOLEAN) holds
( b4 = (S,U) -TruthEval m iff for mm being Element of NAT st m = mm holds
b4 = ((S,U) -TruthEval) . mm );

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 )

proof end;

Lm8: for X, Y, Z, x being set holds
( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) )

proof end;

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)

proof end;

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 (),(PFuncs (((() *) \ ),BOOLEAN))

proof end;

Lm11: for m being Nat
for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (),(PFuncs (((() *) \ ),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 (((() *) \ ),BOOLEAN) equals :: FOMODEL2:def 22
(curry ((S,U) -TruthEval m)) . I;
coherence
(curry ((S,U) -TruthEval m)) . I is Element of PFuncs (((() *) \ ),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;

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

proof end;

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)

proof end;

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)

by Lm13;

definition
let S be Language;
let m be natural Number ;
func S -formulasOfMaxDepth m -> Subset of ((() *) \ ) means :Def22: :: 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 ((() *) \ ) 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 ((() *) \ ) 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 Def22 defines -formulasOfMaxDepth FOMODEL2:def 23 :
for S being Language
for m being natural Number
for b3 being Subset of ((() *) \ ) 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) );

Lm15: for m, n being Nat
for S being Language holds S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n)

proof end;

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

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

:: deftheorem Def23 defines -wff FOMODEL2:def 24 :
for S being Language
for m being natural Number
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 :Def24: :: FOMODEL2:def 25
ex m being Nat st w is m -wff ;
end;

:: deftheorem Def24 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 for Element of (() *) \ ;
coherence
for b1 being string of S st b1 is 0 -wff holds
b1 is 0wff
proof end;
cluster 0wff -> 0 -wff for Element of (() *) \ ;
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 for Element of (() *) \ ;
coherence
for b1 being string of S st b1 is m -wff holds
b1 is wff
;
let n be Nat;
cluster m + (0 * n) -wff -> m + n -wff for Element of (() *) \ ;
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 natural Number ;
existence
ex b1 being string of S st b1 is m -wff
proof end;
end;

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

registration
let S be Language;
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 :Def25: :: 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 Def25 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 . (() . t)) . ((((I,u) -TermEval) . m) * ()) & ( t is 0 -termal implies (((I,u) -TermEval) . (m + 1)) . t = (I . (() . 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 Lm6;

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 (),(PFuncs (((() *) \ ),BOOLEAN)) by Lm11;

theorem :: FOMODEL2:6
for X, Y, Z, x being set holds
( x in (X \/ Y) \/ Z iff ( x in X or x in Y or x in Z ) ) by Lm8;

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

definition
let S be Language;
let m be Nat;
redefine func S -formulasOfMaxDepth m means :Def27: :: 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 ((() *) \ ) 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 Def27 defines -formulasOfMaxDepth FOMODEL2:def 28 :
for S being Language
for m being Nat
for b3 being Subset of ((() *) \ ) 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) );

Lm17: for m being Nat
for S being Language
for U being non empty set holds curry ((S,U) -TruthEval m) is Function of (),(Funcs ((),BOOLEAN))

proof end;

theorem Th8: :: FOMODEL2:8
for m being Nat
for S being Language
for U being non empty set holds
( (S,U) -TruthEval m in Funcs ([:(),():],BOOLEAN) & ((S,U) -TruthEval) . m in Funcs ([:(),():],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
{ ((<*()*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } ;
coherence
{ ((<*()*> ^ 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 = { ((<*()*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } ;

Lm18: for m being Nat
for S being Language
for U being non empty set holds dom (NorIterator ((S,U) -TruthEval m)) = [:(),():]

proof end;

Lm19: for m being Nat
for S being Language
for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(),():]

proof end;

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

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

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

registration
let S be Language;
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 :Def30: :: 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 Def30 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 ) ) );

Lm20: for m being Nat
for S being Language
for phi being wff string of S st phi in () \ () holds
ex n being Nat st
( phi is n + 1 -wff & not phi is n -wff & n + 1 <= m )

proof end;

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 = (<*()*> ^ phi1) ^ phi2

proof end;

registration
let S be Language;
let m be Nat;
let phi1, phi2 be m -wff string of S;
cluster (<*()*> ^ phi1) ^ phi2 -> m + 1 -wff for string of S;
coherence
for b1 being string of S st b1 = (<*()*> ^ 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 (<*()*> ^ phi1) ^ phi2 -> wff for string of S;
coherence
for b1 being string of S st b1 = (<*()*> ^ 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 for 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 for 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 for 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 for 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 for 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 <*()*> ^ w -> non 0wff for string of S;
coherence
for b1 being string of S st b1 = <*()*> ^ 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 for 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 :Def31: :: FOMODEL2:def 32
() . w is literal ;
end;

:: deftheorem Def31 defines exal FOMODEL2:def 32 :
for S being Language
for w being string of S holds
( w is exal iff () . 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 for 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;
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 for Element of (() *) \ ;
coherence
for b1 being string of S st b1 is exal holds
not b1 is 0wff
;
end;

registration
let S be Language;
let m1 be non zero Nat;
existence
not for b1 being m1 -wff exal string of S holds b1 is 0wff
proof end;
end;

registration
let S be Language;
existence
not for b1 being wff exal string of S holds b1 is 0wff
proof end;
end;

Lm22: 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 for Nat;
coherence
for b1 being Nat st b1 = Depth phi holds
not b1 is zero
by Lm22;
end;

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

proof end;

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

Lm24: 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 for set ;
coherence
for b1 being set st b1 = S -formulasOfMaxDepth m holds
b1 is S -prefix
by Lm24;
end;

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

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

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

registration
let S be Language;
cluster AllFormulasOf S -> S -prefix for set ;
coherence
for b1 being set st b1 = AllFormulasOf S holds
b1 is S -prefix
by Lm25;
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)) = [:(),():] by Lm18;

theorem :: FOMODEL2:12
for m being Nat
for S being Language
for U being non empty set holds dom (ExIterator ((S,U) -TruthEval m)) = [:(),():] by Lm19;

Lm26: for U being non empty set holds " {1} = () .: (id ())
proof end;

theorem Th13: :: FOMODEL2:13
for U being non empty set holds " {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 ()) + 2 -> zero for number ;
coherence
for b1 being number st b1 = (ar ()) + 2 holds
b1 is zero
proof end;
cluster |.(ar ()).| - 2 -> zero for number ;
coherence
for b1 being number st b1 = |.(ar ()).| - 2 holds
b1 is zero
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
( ( () . phi <> TheEqSymbOf S implies I -AtomicEval phi = (I . (() . phi)) . (() * (SubTerms phi)) ) & ( () . phi = TheEqSymbOf S implies I -AtomicEval phi = . (() * (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 () . phi = TheEqSymbOf S holds
( I -AtomicEval phi = 1 iff () . ((SubTerms phi) . 1) = () . ((SubTerms phi) . 2) )
proof end;

registration
let S be Language;
let m be Nat;
cluster m -ExFormulasOf S -> non empty for 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 for 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 ((() *) \ );
coherence
m -NorFormulasOf S is Subset of ((() *) \ )
proof end;
end;

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

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

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

by Def30;

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

by Def30;

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

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

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

by Def30;

registration
let S be Language;
cluster non literal for 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 for 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 for 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 for 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;

Lm30: for S being Language
for phi1, phi2 being wff string of S holds
( Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi2 )

by Def30;

Lm31: for S being Language
for phi1, phi2 being wff string of S holds Depth ((<*()*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1

by Def30;

notation
let S be Language;
let m be natural Number ;
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 for Element of (() *) \ ;
coherence
for b1 being string of S st not b1 is m -wff holds
b1 is m -nonwff
;
end;

registration
let S be Language;
let phi1, phi2 be wff string of S;
cluster (<*()*> ^ phi1) ^ phi2 -> max ((Depth phi1),(Depth phi2)) -nonwff for string of S;
coherence
for b1 being string of S st b1 = (<*()*> ^ 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 for 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 for string of S;
coherence
for b1 being string of S st b1 = <*l*> ^ phi holds
b1 is 1 + (Depth phi) -wff
proof end;
end;

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

proof end;

registration
let S be Language;
let U be non empty set ;
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 ;
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 ;
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;

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]

proof end;

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 [:(),((() *) \ ):],BOOLEAN st dom f = [:(),():] & 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;

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 )

proof end;

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 [:(),((() *) \ ):],BOOLEAN st dom f = [:(),():] & phi1 is m -wff holds
( f -NorFunctor (I,((<*()*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )

proof end;

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 ((<*()*> ^ 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
(<*()*> ^ w) ^ w;
coherence
(<*()*> ^ 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 = (<*()*> ^ 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 for 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 for 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 for 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 :: FOMODEL2:def 34
for phi being wff string of S holds
( phi in X iff not xnot phi in X );
end;

:: deftheorem 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 ((<*()*> ^ phi1) ^ phi2) = 1 + (max ((Depth phi1),(Depth phi2))) & Depth (<*l*> ^ phi1) = (Depth phi1) + 1 ) by Def30;

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 ;

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 ((<*()*> ^ phi1) ^ phi2) = TRUE implies ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) ) & ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE implies I -TruthEval ((<*()*> ^ phi1) ^ phi2) = TRUE ) ) by ;

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)) | (() . m) = () | (() . 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 () . t = (I . (() . 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 = () . 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 = (<*(() . phi)*> ^ phi1) ^ p );
func SubWffsOf phi -> set means :Def34: :: FOMODEL2:def 35
ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & it = [phi1,p] & phi = (<*(() . 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 = (<*(() . 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 = (<*(() . phi)*> ^ phi1) ^ p ) & ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b2 = [phi1,p] & phi = (<*(() . 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 Def34 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 = (<*(() . 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 () * equals :: FOMODEL2:def 37
(SubWffsOf phi) `2 ;
coherence
(SubWffsOf phi) `2 is Element of () *
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 () \ () -> empty for set ;
coherence
for b1 being set st b1 = () \ () holds
b1 is empty
proof end;
end;

registration
let S be Language;
cluster () \ () -> empty for set ;
coherence
for b1 being set st b1 = () \ () 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 ((<*()*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi2 ) by ;

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 = () . phi & phi2 = head phi & p2 = tail phi ) )
proof end;

registration
let S be Language;
let m1 be non zero Nat;
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 for set ;
coherence
for b1 being set st b1 = tail phi holds
b1 is empty
proof end;
end;

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

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 for 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
proof end;
end;

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

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 )

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 for 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 for string of S;
coherence
for b1 being string of S st b1 = tail phi holds
b1 is m -wff
by Lm39;
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 ((),BOOLEAN)
proof end;

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

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 Lm40;
identify I -AtomicEval phi0 with I -TruthEval phi0;
compatibility
I -AtomicEval phi0 = I -TruthEval phi0
;
end;

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

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
() | (X *) = () | (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 = () . p
proof end;

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

:: deftheorem Def37 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 (((() *) \ ) /\ 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 ((() *) \ ());
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 ((() *) \ ()) );

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;
existence
ex b1 being literal Element of S st b1 is X -absent
proof end;
end;

Lm42: for S being Language
for w being string of S st w is termal holds
(rng w) /\ () <> {}

proof end;

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

Lm43: for S being Language
for w being string of S st w is wff holds
(rng w) /\ () <> {}

proof end;

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

registration
let B be set ;
let S be Language;
let A be Subset of B;
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 for Element of AllSymbolsOf S;
coherence
for b1 being Element of S st b1 is A null B -absent holds
b1 is A /\ B -absent
;
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 for Element of AllSymbolsOf S;
coherence
for b1 being F -absent Element of S st b1 is A -absent holds
b1 is A \/ F -absent
proof end;
end;

registration
let S be Language;
let U be non empty set ;
let I be S,U -interpreter-like Function;
cluster () \ (dom I) -> empty for set ;
coherence
for b1 being set st b1 = () \ (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 for set ;
coherence
for b1 being set st b1 is S -mincover holds
b1 is S -covering
;
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 for 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 ((() *) \ ) 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 ((() *) \ )
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 for 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 for 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 for Element of ExFormulasOf S;
coherence
for b1 being Element of ExFormulasOf S holds b1 is wff
;
end;

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

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

registration
let U be non empty set ;
let S1 be Language;
let S2 be S1 -extending Language;
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 | () -> S1,U -interpreter-like for Function;
coherence
for b1 being Function st b1 = I | () 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 :Def41: :: FOMODEL2:def 42
for phi being wff string of S st phi in X holds
I -TruthEval phi = 1;
end;

:: deftheorem Def41 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 :: FOMODEL2:def 43
X is I -satisfied ;
end;

:: deftheorem 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 for set ;
coherence
for b1 being set st b1 = e null I holds
b1 is I -satisfied
;
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 for 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 for 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 for Element of bool X;
coherence
for b1 being Subset of X holds b1 is I -satisfied
by Def41;
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 for Element of U -InterpretersOf S;
coherence
for b1 being Element of U -InterpretersOf S st b1 = I null X holds
b1 is X -satisfying
;
end;

definition
let S be Language;
let X be set ;
attr X is S -correct means :: 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 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 for set ;
coherence
for b1 being set st b1 = {} null S holds
b1 is S -correct
;
end;

registration
let S be Language;
let X be set ;
cluster S -correct for 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 ) by FOMODEL0:45;

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 ((<*()*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) -> empty for set ;
coherence
for b1 being set st b1 = (I -TruthEval ((<*()*> ^ 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 for 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 );

registration
let S be Language;
let l be literal Element of S;
let phi be wff string of S;
cluster (head (<*l*> ^ phi)) \+\ phi -> empty ;
coherence
(head (<*l*> ^ phi)) \+\ phi is empty
proof end;
end;