:: First order languages: syntax, part two; semantics
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2021 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 (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: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 b₁ being set st b₁ is Function of (|.(ar s).| -tuples_on U),BOOLEAN ) & ( not s is relational implies ex b₁ being set st b₁ is Function of (|.(ar s).| -tuples_on U),U ) )

proof end;

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

coherence
for b₁ being Interpreter of s,U holds b₁ is U -valued by Def2;

end;

registration

let S be Language;

cluster literal -> own for Element of AllSymbolsOf S;

coherence
for b₁ being Element of S st b₁ is literal holds
b₁ 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 b₁ being Function st
for s being own Element of S holds b₁ . 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 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 :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 ;

cluster Relation-like Function-like S,U -interpreter-like -> Function-yielding for set ;

coherence
for b₁ being Function st b₁ is S,U -interpreter-like holds
b₁ 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 b₁ being Interpreter of s,U holds not b₁ 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 ;

cluster Relation-like Function-like S,U -interpreter-like for 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 for 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 V171() for 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

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 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 for FinSequence of E;

coherence
for b₁ being FinSequence of E st b₁ = h * p holds
b₁ is n -element ;

end;

Lm3: 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 |.(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;

Lm4: 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 -> sequence of (Funcs ((AllTermsOf S),U)) means :Def7: :: 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 sequence of (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 sequence of (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 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 b₁,b₂ -interpreter-like Function
for b₅ being sequence of (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)____ ) ) );

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

Lm6: 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 :Def8: :: 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 Def8 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 :Def9: :: 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 Def9 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 );

::############### 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 +* ((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 :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 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 for Function;

coherence
for b₁ being Function st b₁ = I === holds
b₁ is I -extension ;

cluster I -extension -> Function-like for set ;

coherence
for b₁ being set st b₁ is I -extension holds
b₁ is Function-like ;

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

::###### 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 | (OwnSymbolsOf S) -> PFuncs ((U *),(U \/ BOOLEAN)) -valued for 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 for 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 for 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 for set ;

coherence
for b₁ being set st b₁ = U -InterpretersOf S holds
not b₁ 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 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 :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 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 Def14 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 :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 b₁ 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 [:(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 :Def16: :: 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 Def16 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 :Def17: :: 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 Def17 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 ) );

::# 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 ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN);

func NorIterator g -> PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN means :Def18: :: 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 Def18 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 -> sequence of (PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],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 b₁ being sequence of (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 sequence of (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 Def19 defines -TruthEval FOMODEL2:def 20 :
for S being Language
for U being non empty set
for b₃ being sequence of (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 :Def20: :: 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 Def20 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 );

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 (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),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 (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;

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 (((AllSymbolsOf S) *) \ {{}}) 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 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 Def22 defines -formulasOfMaxDepth FOMODEL2:def 23 :
for S being Language
for m being natural Number
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) );

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 ((AllSymbolsOf S) *) \ {{}};

coherence
for b₁ being string of S st b₁ is 0 -wff holds
b₁ is 0wff

proof end;

cluster 0wff -> 0 -wff for 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 for Element of ((AllSymbolsOf S) *) \ {{}};

coherence
for b₁ being string of S st b₁ is m -wff holds
b₁ is wff ;
let n be Nat;

cluster m + (0 * n) -wff -> m + n -wff for 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 natural Number ;

cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like m -wff for 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 natural Number ;

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 omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like wff for 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 :Def25: :: 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 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 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 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 (U -InterpretersOf S),(PFuncs ((((AllSymbolsOf S) *) \ {{}}),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 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 Def27 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) );

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

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 ([:(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 } ;

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

proof end;

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

proof end;

theorem Th9: :: 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 for 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 for 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 :Def30: :: 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 Def30 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 ) ) );

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

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 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 for 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 :Def31: :: FOMODEL2:def 32
(S -firstChar) . 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 (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 for 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 omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like m1 -wff wff exal for 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 for Element of ((AllSymbolsOf S) *) \ {{}};

coherence
for b₁ being string of S st b₁ is exal holds
not b₁ is 0wff ;

end;

registration

let S be Language;
let m1 be non zero Nat;

cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like non 0wff m1 -wff wff exal for 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 omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like non 0wff wff exal for Element of ((AllSymbolsOf S) *) \ {{}};

existence
not for b₁ being wff exal string of S holds b₁ 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 b₁ being Nat st b₁ = Depth phi holds
not b₁ 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 (S -firstChar) . w -> non relational for Element of S;

coherence
for b₁ being Element of S st b₁ = (S -firstChar) . w holds
not b₁ 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 b₁ being set st b₁ = S -formulasOfMaxDepth m holds
b₁ is S -prefix by Lm24;

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 for Element of AllFormulasOf S;

coherence
for b₁ being Element of AllFormulasOf S holds b₁ 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 b₁ being set st b₁ = AllFormulasOf S holds
b₁ 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)) = [:(U -InterpretersOf S),(m -NorFormulasOf S):] 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)) = [:(U -InterpretersOf S),(m -ExFormulasOf S):] by Lm19;

Lm26: 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 for number ;

coherence
for b₁ being number st b₁ = (ar (TheEqSymbOf S)) + 2 holds
b₁ is zero

proof end;

cluster |.(ar (TheEqSymbOf S)).| - 2 -> zero for number ;

coherence
for b₁ being number st b₁ = |.(ar (TheEqSymbOf S)).| - 2 holds
b₁ 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 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 for 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 for 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 for Element of S;

coherence
for b₁ being Element of S st b₁ = (S -firstChar) . w holds
b₁ 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 b₁ being Element of m -NorFormulasOf S holds not b₁ 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

proof end;

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

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 for Element of m -ExFormulasOf S;

coherence
for b₁ being Element of m -ExFormulasOf S holds b₁ 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

proof end;

registration

let S be Language;

cluster non literal for 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 for 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 for 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 for 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;

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

proof end;

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

proof end;

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 ((AllSymbolsOf S) *) \ {{}};

coherence
for b₁ being string of S st not b₁ is m -wff holds
b₁ is m -nonwff ;

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 for 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 for 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 for string of S;

coherence
for b₁ being string of S st b₁ = <*l*> ^ phi holds
b₁ 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 ;

cluster -> OwnSymbolsOf S -defined for 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 V171() S,U -interpreter-like for 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 for 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;

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 [:(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;

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 [:(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;

Lm37: for S being Language
for U being non empty set
for phi1, phi2 being wff string of S
for I being Element of U -InterpretersOf S holds
( I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = TRUE iff ( I -TruthEval phi1 = FALSE & I -TruthEval phi2 = FALSE ) )

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 for 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 for 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 for 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 :: 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 ((<*(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 Lm27, Lm29;

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 Lm35, Lm37;

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 :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 = (<*((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 Def34 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 for 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 for 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 Lm28, Lm30;

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 omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like non 0wff m1 -wff wff non exal for 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 for set ;

coherence
for b₁ being set st b₁ = tail phi holds
b₁ 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 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 for 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 for set ;

coherence
for b₁ being set st b₁ = ((S -firstChar) . phi) \+\ (TheNorSymbOf S) holds
b₁ 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 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 for 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 for string of S;

coherence
for b₁ being string of S st b₁ = tail phi holds
b₁ 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 ((S -formulasOfMaxDepth m),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;

cluster non literal ofAtomicFormula for Element of AllSymbolsOf S;

existence
not for b₁ being ofAtomicFormula Element of S holds b₁ is literal

proof end;

end;

Lm41: 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 :Def37: :: FOMODEL2:def 38
s in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ 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 ((((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 for Element of AllSymbolsOf S;

existence
ex b₁ being literal Element of S st b₁ is X -absent

proof end;

end;

Lm42: 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 for set ;

coherence
for b₁ being set st b₁ = (rng t) /\ (LettersOf S) holds
not b₁ is empty by Lm42;

end;

Lm43: 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 for set ;

coherence
for b₁ being set st b₁ = (rng phi) /\ (LettersOf S) holds
not b₁ is empty by Lm43;

end;

registration

let B be set ;
let S be Language;
let A be Subset of B;

cluster A -occurring -> B -occurring for 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 for Element of AllSymbolsOf S;

coherence
for b₁ being Element of S st b₁ is A null B -absent holds
b₁ 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 b₁ being F -absent Element of S st b₁ is A -absent holds
b₁ 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 (OwnSymbolsOf S) \ (dom I) -> empty for 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 for set ;

coherence
for b₁ being set st b₁ is S -mincover holds
b₁ 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 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 for 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 for 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 for Element of ExFormulasOf S;

coherence
for b₁ being Element of ExFormulasOf S holds b₁ is wff ;

end;

registration

let S be Language;

cluster -> exal for 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 for 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 for 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 for 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 :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 b₁ being set st b₁ = e null I holds
b₁ 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 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 for 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 for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ 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 b₁ being Element of U -InterpretersOf S st b₁ = I null X holds
b₁ 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 b₂ -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 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 for set ;

coherence
for b₁ being set st b₁ = {} null S holds
b₁ is S -correct ;

end;

registration

let S be Language;
let X be set ;

cluster S -correct for 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 ) 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 ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) -> empty for 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 for 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 );

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;