:: 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 b₁ being set st b₁ is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ) & ( not s is relational implies ex b₁ being set st b₁ is Function of ((abs (ar s)) -tuples_on U),U ) )

proof end;

consistency
for b₁ 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 b₄ being set holds
( ( s is relational implies ( b₄ is Interpreter of s,U iff b₄ is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ) ) & ( not s is relational implies ( b₄ is Interpreter of s,U iff b₄ 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 b₁ being Interpreter of s,U holds b₁ 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 b₁ being Interpreter of s,U holds b₁ is U -valued by DefInterpreter1;

end;

registration

let S be Language;
cluster literal -> own Element of AllSymbolsOf S;
coherence
for b₁ being Element of S st b₁ is literal holds
b₁ 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 b₁ being Function st
for s being own Element of S holds b₁ . 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 b₃ being Function holds
( b₃ is Interpreter of S,U iff for s being own Element of S holds b₃ . 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 b₁ being Function st b₁ is S,U -interpreter-like holds
b₁ 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 b₁ being Interpreter of s,U holds not b₁ 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 b₁ being Function st b₁ 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 b₁ being Function of X,(Funcs (Y,Z)) holds b₁ 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 b₁ being Function of X,(Funcs (Y,Z)) st b₁ 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 b₁ being Function st
( dom b₁ = dom f & ( for x being set st x in dom f holds
b₁ . x = g * (f . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for x being set st x in dom f holds
b₁ . x = g * (f . x) ) & dom b₂ = dom f & ( for x being set st x in dom f holds
b₂ . x = g * (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ^^^ FOMODEL2:def 6 :
for f being Function-yielding Function
for g, b₃ being Function holds
( b₃ = ^^^g,f__ iff ( dom b₃ = dom f & ( for x being set st x in dom f holds
b₃ . 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 b₁ being Function st
( dom b₁ = (dom f) /\ (dom g) & ( for x being set st x in dom b₁ holds
b₁ . x = (f . x) . (g . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f) /\ (dom g) & ( for x being set st x in dom b₁ holds
b₁ . x = (f . x) . (g . x) ) & dom b₂ = (dom f) /\ (dom g) & ( for x being set st x in dom b₂ holds
b₂ . x = (f . x) . (g . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines ^^^ FOMODEL2:def 7 :
for f being Function-yielding Function
for g, b₃ being Function holds
( b₃ = ^^^f,g__ iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being set st x in dom b₃ holds
b₃ . 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 b₁ being Function st b₁ is X -valued holds
b₁ 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 b₁ being FinSequence st b₁ = h * p holds
b₁ 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 b₁ being FinSequence of E st b₁ = h * p holds
b₁ is n -element ;

end;

Lm15: for U being non empty set
for S being Language
for I being b₂,b₁ -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 b₁,b₂ -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 b₁ being Function of NAT,(Funcs ((AllTermsOf S),U)) st
( b₁ . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b₁ . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b₁ . mm),(S -subTerms)____ ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT,(Funcs ((AllTermsOf S),U)) st b₁ . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b₁ . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b₁ . mm),(S -subTerms)____ ) & b₂ . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b₂ . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b₂ . mm),(S -subTerms)____ ) holds
b₁ = b₂

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 b₁,b₂ -interpreter-like Function
for b₅ being Function of NAT,(Funcs ((AllTermsOf S),U)) holds
( b₅ = (I,u) -TermEval iff ( b₅ . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b₅ . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b₅ . mm),(S -subTerms)____ ) ) );

Lm21: for S being Language
for U being non empty set
for u being Element of U
for I being b₁,b₂ -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 b₁,b₂ -interpreter-like Function
for u1, u2 being Element of U
for m being Nat
for t being b₆ -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 b₁ being Element of U st
for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b₁ = (((I,u1) -TermEval) . (mm + 1)) . t

proof end;

uniqueness
for b₁, b₂ being Element of U st ( for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b₁ = (((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
b₂ = (((I,u1) -TermEval) . (mm + 1)) . t ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefTermEval2 defines -TermEval FOMODEL2:def 9 :
for S being Language
for U being non empty set
for I being b₁,b₂ -interpreter-like Function
for t being Element of AllTermsOf S
for b₅ being Element of U holds
( b₅ = I -TermEval t iff for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
b₅ = (((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 b₁ being Function of (AllTermsOf S),U st
for t being Element of AllTermsOf S holds b₁ . t = I -TermEval t

proof end;

uniqueness
for b₁, b₂ being Function of (AllTermsOf S),U st ( for t being Element of AllTermsOf S holds b₁ . t = I -TermEval t ) & ( for t being Element of AllTermsOf S holds b₂ . t = I -TermEval t ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefTermEval3 defines -TermEval FOMODEL2:def 10 :
for S being Language
for U being non empty set
for I being b₁,b₂ -interpreter-like Function
for b₄ being Function of (AllTermsOf S),U holds
( b₄ = I -TermEval iff for t being Element of AllTermsOf S holds b₄ . 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 b₁,b₂ -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 b₁,b₂ -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 b₁ being Function st b₁ = I === holds
b₁ is I -extension by DefExtension;
cluster I -extension -> Function-like set ;
coherence
for b₁ being set st b₁ is I -extension holds
b₁ 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 b₁ being Function st b₁ 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 b₁,b₂ -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 b₁ being Function st b₁ = I | (OwnSymbolsOf S) holds
b₁ is PFuncs ((U *),(U \/ BOOLEAN)) -valued

proof end;

cluster I | (OwnSymbolsOf S) -> S,U -interpreter-like Function;
coherence
for b₁ being Function st b₁ = I | (OwnSymbolsOf S) holds
b₁ 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 b₁ being OwnSymbolsOf S -defined Relation st b₁ = I | (OwnSymbolsOf S) holds
b₁ 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 b₁ being Element of U -InterpretersOf S holds b₁ 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 b₁ 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 b₁ . (I,phi) = I -AtomicEval phi

proof end;

uniqueness
for b₁, b₂ 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 b₁ . (I,phi) = I -AtomicEval phi ) & ( for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b₂ . (I,phi) = I -AtomicEval phi ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefTruth6 defines -TruthEval FOMODEL2:def 15 :
for S being Language
for U being non empty set
for b₃ being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN holds
( b₃ = S -TruthEval U iff for I being Element of U -InterpretersOf S
for phi being Element of AtomicFormulasOf S holds b₃ . (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 b₁ 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 b₁ 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 b₁ 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 b₁ holds
b₁ . (x,y) = g -ExFunctor (x,y) ) )

proof end;

uniqueness
for b₁, b₂ 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 b₁ 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 b₁ holds
b₁ . (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 b₂ 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 b₂ holds
b₂ . (x,y) = g -ExFunctor (x,y) ) holds
b₁ = b₂

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 b₄ being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds
( b₄ = ExIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b₄ 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 b₄ holds
b₄ . (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 b₁ 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 b₁ 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 b₁ 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 b₁ holds
b₁ . (x,y) = g -NorFunctor (x,y) ) )

proof end;

uniqueness
for b₁, b₂ 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 b₁ 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 b₁ holds
b₁ . (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 b₂ 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 b₂ holds
b₂ . (x,y) = g -NorFunctor (x,y) ) holds
b₁ = b₂

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 b₄ being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds
( b₄ = NorIterator g iff ( ( for x being Element of U -InterpretersOf S
for y being Element of ((AllSymbolsOf S) *) \ {{}} holds
( [x,y] in dom b₄ 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 b₄ holds
b₄ . (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 b₁ being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) st
( b₁ . 0 = S -TruthEval U & ( for mm being Element of NAT holds b₁ . (mm + 1) = ((ExIterator (b₁ . mm)) +* (NorIterator (b₁ . mm))) +* (b₁ . mm) ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT,(PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) st b₁ . 0 = S -TruthEval U & ( for mm being Element of NAT holds b₁ . (mm + 1) = ((ExIterator (b₁ . mm)) +* (NorIterator (b₁ . mm))) +* (b₁ . mm) ) & b₂ . 0 = S -TruthEval U & ( for mm being Element of NAT holds b₂ . (mm + 1) = ((ExIterator (b₂ . mm)) +* (NorIterator (b₂ . mm))) +* (b₂ . mm) ) holds
b₁ = b₂

proof end;

end;

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

theorem Th2: :: FOMODEL2:2

for S being Language
for U being non empty set
for I being b₁,b₂ -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 b₁ being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st
for mm being Element of NAT st m = mm holds
b₁ = ((S,U) -TruthEval) . mm

proof end;

uniqueness
for b₁, b₂ being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st ( for mm being Element of NAT st m = mm holds
b₁ = ((S,U) -TruthEval) . mm ) & ( for mm being Element of NAT st m = mm holds
b₂ = ((S,U) -TruthEval) . mm ) holds
b₁ = b₂

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 b₄ being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) holds
( b₄ = (S,U) -TruthEval m iff for mm being Element of NAT st m = mm holds
b₄ = ((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 b₁ 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
b₁ = dom ((I,mm) -TruthEval)

proof end;

uniqueness
for b₁, b₂ 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
b₁ = 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
b₂ = dom ((I,mm) -TruthEval) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefFormula1 defines -formulasOfMaxDepth FOMODEL2:def 23 :
for S being Language
for m being Nat
for b₃ being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b₃ = 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
b₃ = 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 b₁ being string of S st b₁ is 0 -wff holds
b₁ is 0wff

proof end;

cluster 0wff -> 0 -wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b₁ being string of S st b₁ is 0wff holds
b₁ is 0 -wff

proof end;

let m be Nat;
cluster m -wff -> wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b₁ being string of S st b₁ is m -wff holds
b₁ is wff by DefWff2;
let n be Nat;
cluster m + (0 * n) -wff -> m + n -wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b₁ being string of S st b₁ is m + (0 * n) -wff holds
b₁ 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 b₁ being string of S st b₁ 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 b₁ being string of S st b₁ 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 b₁ being Element of BOOLEAN st
for m being Nat st w is m -wff holds
b₁ = ((I,m) -TruthEval) . w

proof end;

uniqueness
for b₁, b₂ being Element of BOOLEAN st ( for m being Nat st w is m -wff holds
b₁ = ((I,m) -TruthEval) . w ) & ( for m being Nat st w is m -wff holds
b₂ = ((I,m) -TruthEval) . w ) holds
b₁ = b₂

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 b₅ being Element of BOOLEAN holds
( b₅ = I -TruthEval w iff for m being Nat st w is m -wff holds
b₅ = ((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 b₂,b₃ -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 b₃,b₄ -interpreter-like Function
for t being b₁ -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 b₁ being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b₁ = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds b₁ = dom ((I,m) -TruthEval) )

proof end;

end;

:: deftheorem DefFormulas defines -formulasOfMaxDepth FOMODEL2:def 28 :
for S being Language
for m being Nat
for b₃ being Subset of (((AllSymbolsOf S) *) \ {{}}) holds
( b₃ = S -formulasOfMaxDepth m iff for U being non empty set
for I being Element of U -InterpretersOf S holds b₃ = 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 b₁ being set st b₁ = AtomicFormulasOf S holds
b₁ is S -prefix by Th10;

end;

registration

let S be Language;
cluster S -formulasOfMaxDepth 0 -> S -prefix set ;
coherence
for b₁ being set st b₁ = S -formulasOfMaxDepth 0 holds
b₁ 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 b₁ being Nat st
( phi is b₁ -wff & ( for n being Nat st phi is n -wff holds
b₁ <= n ) )

proof end;

uniqueness
for b₁, b₂ being Nat st phi is b₁ -wff & ( for n being Nat st phi is n -wff holds
b₁ <= n ) & phi is b₂ -wff & ( for n being Nat st phi is n -wff holds
b₂ <= n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefDepth defines Depth FOMODEL2:def 31 :
for S being Language
for phi being wff string of S
for b₃ being Nat holds
( b₃ = Depth phi iff ( phi is b₃ -wff & ( for n being Nat st phi is n -wff holds
b₃ <= 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 b₁ -wff string of S holds not w = <*v*> ^ phi ) holds
ex phi1, phi2 being b₁ -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 b₁ being string of S st b₁ = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b₁ 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 b₁ being string of S st b₁ = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
b₁ 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 b₁ being string of S st b₁ = <*v*> ^ phi holds
b₁ 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 b₁ being string of S st b₁ = <*l*> ^ phi holds
b₁ 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 b₁ being string of S st b₁ = <*s*> ^ w holds
not b₁ 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 b₁ being string of S st b₁ = (<*s*> ^ w1) ^ w2 holds
not b₁ is 0wff

proof end;

end;

registration

let S be Language;
cluster TheNorSymbOf S -> non relational Element of S;
coherence
for b₁ being Element of S st b₁ = TheNorSymbOf S holds
not b₁ 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 b₁ being string of S st b₁ = <*(TheNorSymbOf S)*> ^ w holds
not b₁ 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 b₁ being string of S st b₁ = <*l*> ^ w holds
not b₁ 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 b₁ being string of S st b₁ = <*l*> ^ w holds
b₁ 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 b₁ being m1 -wff string of S st b₁ is exal

proof end;

end;

registration

let S be Language;
cluster exal -> non 0wff Element of ((AllSymbolsOf S) *) \ {{}};
coherence
for b₁ being string of S st b₁ is exal holds
not b₁ 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 b₁ being m1 -wff exal string of S holds b₁ 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 b₁ being wff exal string of S holds b₁ 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 b₁ being Nat st b₁ = Depth phi holds
not b₁ 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 b₁ being Element of S st b₁ = (S -firstChar) . w holds
not b₁ 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 b₁ being set st b₁ = S -formulasOfMaxDepth m holds
b₁ 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 b₁ being Element of AllFormulasOf S holds b₁ 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 b₁ being set st b₁ = AllFormulasOf S holds
b₁ 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 b₁ being number st b₁ = (ar (TheEqSymbOf S)) + 2 holds
b₁ is empty

proof end;

cluster (abs (ar (TheEqSymbOf S))) - 2 -> zero number ;
coherence
for b₁ being number st b₁ = (abs (ar (TheEqSymbOf S))) - 2 holds
b₁ 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 b₁,b₂ -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 b₁,b₂ -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 b₁ being set st b₁ = m -ExFormulasOf S holds
not b₁ is empty

proof end;

end;

registration

let S be Language;
let m be Nat;
cluster m -NorFormulasOf S -> non empty set ;
coherence
for b₁ being set st b₁ = m -NorFormulasOf S holds
not b₁ 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 b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ is literal by DefExal;

end;

registration

let S be Language;
let m be Nat;
cluster -> non exal Element of m -NorFormulasOf S;
coherence
for b₁ being Element of m -NorFormulasOf S holds not b₁ 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 b₁ being Element of m -ExFormulasOf S holds b₁ 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 b₁ being Element of S holds b₁ 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 b₁ being string of S st b₁ = <*s*> ^ w holds
not b₁ 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 b₁ being string of S st b₁ = (<*s*> ^ w1) ^ w2 holds
not b₁ is exal

proof end;

end;

registration

let S be Language;
cluster TheNorSymbOf S -> non literal Element of S;
coherence
for b₁ being Element of S st b₁ = TheNorSymbOf S holds
not b₁ 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 b₁ being string of S st not b₁ is m -wff holds
not b₁ 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 b₁ being string of S st b₁ = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
not b₁ 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 b₁ being string of S st b₁ = <*l*> ^ phi holds
not b₁ 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 b₁ being string of S st b₁ = <*l*> ^ phi holds
b₁ 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 b₁ being Element of U -InterpretersOf S holds b₁ 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 b₁ being Element of U -InterpretersOf S st b₁ 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 b₁ being OwnSymbolsOf S -defined Element of U -InterpretersOf S holds b₁ 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 b₁ being string of S st b₁ = xnot phi holds
b₁ 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 b₁ being string of S st b₁ = xnot phi holds
b₁ is wff ;

end;

registration

let S be Language;
cluster TheEqSymbOf S -> non own Element of S;
coherence
for b₁ being Element of S st b₁ = TheEqSymbOf S holds
not b₁ 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 b₂,b₃ -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 b₁,b₂ -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 S₁[ 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 b₁ being set ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b₁ = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) & ( phi is 0wff implies ex b₁ being set st b₁ = [phi,{}] ) )

proof end;

uniqueness
for b₁, b₂ being set holds
( ( not phi is 0wff & ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b₁ = [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 & b₂ = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) implies b₁ = b₂ ) & ( phi is 0wff & b₁ = [phi,{}] & b₂ = [phi,{}] implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being set holds verum ;

end;

:: deftheorem DefSub1 defines SubWffsOf FOMODEL2:def 35 :
for S being Language
for phi being wff string of S
for b₃ being set holds
( ( not phi is 0wff implies ( b₃ = SubWffsOf phi iff ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & b₃ = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) ) & ( phi is 0wff implies ( b₃ = SubWffsOf phi iff b₃ = [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 b₁ being set st b₁ = (S -formulasOfMaxDepth m) \ (AllFormulasOf S) holds
b₁ is empty

proof end;

end;

registration

let S be Language;
cluster (AtomicFormulasOf S) \ (AllFormulasOf S) -> empty set ;
coherence
for b₁ being set st b₁ = (AtomicFormulasOf S) \ (AllFormulasOf S) holds
b₁ 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 b₁ being non 0wff m1 -wff string of S holds b₁ 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 b₁ being set st b₁ = tail phi holds
b₁ 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 b₁ -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 b₁ being string of S st b₁ = tail phi holds
b₁ 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 b₁ being set st b₁ = ((S -firstChar) . phi) \+\ (TheNorSymbOf S) holds
b₁ 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 b₁ -wff string of S & tail phi is b₁ -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 b₁ being string of S st b₁ = head phi holds
b₁ 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 b₁ being string of S st b₁ = tail phi holds
b₁ 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 b₁ being ofAtomicFormula Element of S holds b₁ is literal

proof end;

end;

Lm52: for X being set
for S being Language
for U being non empty set
for I1, I2 being b₂,b₃ -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 b₁,b₂ -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 b₁ being literal Element of S holds b₁ 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 b₁ being set st b₁ = (rng t) /\ (LettersOf S) holds
not b₁ 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 b₁ being set st b₁ = (rng phi) /\ (LettersOf S) holds
not b₁ 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 b₁ being Element of S st b₁ is A -occurring holds
b₁ 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 b₁ being Element of S st not b₁ is A null B -occurring holds
not b₁ 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 b₁ being F -absent Element of S st not b₁ is A -occurring holds
not b₁ 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 b₁ being set st b₁ = (OwnSymbolsOf S) \ (dom I) holds
b₁ 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 b₁,b₂ -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 b₁ being set st b₁ is S -mincover holds
b₁ 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 b₁ being set st b₁ = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds
b₁ 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 b₁ being set st b₁ = ExFormulasOf S holds
not b₁ is empty

proof end;

end;

registration

let S be Language;
cluster -> wff exal Element of ExFormulasOf S;
coherence
for b₁ being Element of ExFormulasOf S holds
( b₁ is exal & b₁ is wff )

proof end;

end;

registration

let S be Language;
cluster -> wff Element of ExFormulasOf S;
coherence
for b₁ being Element of ExFormulasOf S holds b₁ is wff ;

end;

registration

let S be Language;
cluster -> exal Element of ExFormulasOf S;
coherence
for b₁ being Element of ExFormulasOf S holds b₁ is exal ;

end;

registration

let S be Language;
cluster (ExFormulasOf S) \ (AllFormulasOf S) -> empty set ;
coherence
for b₁ being set st b₁ = (ExFormulasOf S) \ (AllFormulasOf S) holds
b₁ 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 b₁ being Function st b₁ is S2,U -interpreter-like holds
b₁ 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 b₁ being Function st b₁ = I | (OwnSymbolsOf S1) holds
b₁ 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 b₁ being Subset of X st b₁ 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 b₁ being set st b₁ 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 b₁ being Subset of X holds b₁ 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 b₁ being Element of U -InterpretersOf S st b₁ = I null X holds
b₁ 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 b₂ -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 b₄ -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 b₁ being Subset of X st b₁ 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 b₁ being set st b₁ = (I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) holds
b₁ 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 b₁ being set st b₁ = (I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) holds
b₁ 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 );