:: by Marco B. Caminati

::

:: Received December 29, 2010

:: Copyright (c) 2010-2013 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;
:: original: TheNorSymbOf

redefine func TheNorSymbOf S -> Element of S;

coherence

TheNorSymbOf S is Element of S ;

definition

let U be non empty set ;

chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U)) is Function of (2 -tuples_on U),BOOLEAN ;

end;
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));

chi (((U -concatenation) .: (id (1 -tuples_on U))),(2 -tuples_on U)) is Function of (2 -tuples_on U),BOOLEAN ;

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

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;
:: original: id

redefine func id X -> Equivalence_Relation of X;

coherence

id X is Equivalence_Relation of X by EQREL_1:3;

definition

let S be Language;

let U be non empty set ;

let s be ofAtomicFormula Element of S;

( ( s is relational implies ex b_{1} being set st b_{1} is Function of (|.(ar s).| -tuples_on U),BOOLEAN ) & ( not s is relational implies ex b_{1} being set st b_{1} is Function of (|.(ar s).| -tuples_on U),U ) )

for b_{1} being set holds verum
;

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

( ( s is relational implies ex b

proof end;

consistency for b

:: 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_{4} being set holds

( ( s is relational implies ( b_{4} is Interpreter of s,U iff b_{4} is Function of (|.(ar s).| -tuples_on U),BOOLEAN ) ) & ( not s is relational implies ( b_{4} is Interpreter of s,U iff b_{4} is Function of (|.(ar s).| -tuples_on U),U ) ) );

for S being Language

for U being non empty set

for s being ofAtomicFormula Element of S

for b

( ( s is relational implies ( b

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_{1} being Interpreter of s,U holds b_{1} is Function of (|.(ar s).| -tuples_on U),(U \/ BOOLEAN)

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

proof end;

registration

let S be Language;

let U be non empty set ;

let s be termal Element of S;

coherence

for b_{1} being Interpreter of s,U holds b_{1} is U -valued
by Def2;

end;
let U be non empty set ;

let s be termal Element of S;

coherence

for b

registration
end;

definition

let S be Language;

let U be non empty set ;

ex b_{1} being Function st

for s being own Element of S holds b_{1} . s is Interpreter of s,U

end;
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 for s being own Element of S holds it . s is Interpreter of s,U;

ex b

for s being own Element of S holds b

proof end;

:: deftheorem Def3 defines Interpreter FOMODEL2:def 3 :

for S being Language

for U being non empty set

for b_{3} being Function holds

( b_{3} is Interpreter of S,U iff for s being own Element of S holds b_{3} . s is Interpreter of s,U );

for S being Language

for U being non empty set

for b

( b

definition

let S be Language;

let U be non empty set ;

let f be Function;

end;
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 );

( f is Interpreter of S,U & f is Function-yielding );

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

for S being Language

for U being non empty set

for f being Function holds

( f is S,U -interpreter-like iff ( f is Interpreter of S,U & f is Function-yielding ) );

registration

let S be Language;

let U be non empty set ;

coherence

for b_{1} being Function st b_{1} is S,U -interpreter-like holds

b_{1} is Function-yielding
;

end;
let U be non empty set ;

coherence

for b

b

registration

let S be Language;

let U be non empty set ;

let s be own Element of S;

coherence

for b_{1} being Interpreter of s,U holds not b_{1} is empty
;

end;
let U be non empty set ;

let s be own Element of S;

coherence

for b

Lm1: for S being Language

for U being non empty set

for f being Interpreter of S,U holds OwnSymbolsOf S c= dom f

proof end;

Lm2: for S being Language

for U being non empty set

for f being Function st f is S,U -interpreter-like holds

OwnSymbolsOf S c= dom f

by Lm1;

registration

let S be Language;

let U be non empty set ;

existence

ex b_{1} being Function st b_{1} is S,U -interpreter-like

end;
let U be non empty set ;

existence

ex b

proof 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

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

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;

coherence

I +* (x .--> f) is S,U -interpreter-like

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

coherence

I +* (x .--> f) is S,U -interpreter-like

proof end;

definition
end;

:: deftheorem defines ReassignIn FOMODEL2:def 5 :

for f being Function

for x, y being set holds (x,y) ReassignIn f = f +* (x .--> ({} .--> y));

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;

coherence

(x,u) ReassignIn I is S,U -interpreter-like

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

coherence

(x,u) ReassignIn I is S,U -interpreter-like

proof end;

::###############################################################

::###############################################################

::###############################################################

::###############################################################

::###############################################################

registration
end;

registration

let Y be set ;

let X, Z be non empty set ;

coherence

for b_{1} being Function of X,(Funcs (Y,Z)) holds b_{1} is Function-yielding
;

end;
let X, Z be non empty set ;

coherence

for b

registration

let X, Y, Z be non empty set ;

ex b_{1} being Function of X,(Funcs (Y,Z)) st b_{1} is Function-yielding

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

proof end;

definition

let f be Function-yielding Function;

let g be Function;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom f holds

b_{1} . x = g * (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom f holds

b_{1} . x = g * (f . x) ) & dom b_{2} = dom f & ( for x being set st x in dom f holds

b_{2} . x = g * (f . x) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom f & ( for x being set st x in dom f holds

it . x = g * (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines ^^^ FOMODEL2:def 6 :

for f being Function-yielding Function

for g, b_{3} being Function holds

( b_{3} = ^^^g,f__ iff ( dom b_{3} = dom f & ( for x being set st x in dom f holds

b_{3} . x = g * (f . x) ) ) );

for f being Function-yielding Function

for g, b

( b

b

definition
end;

canceled;

registration
end;

registration

let E, D be non empty set ;

let p be D -valued FinSequence;

let h be Function of D,E;

coherence

for b_{1} being FinSequence st b_{1} = h * p holds

b_{1} is len p -element

end;
let p be D -valued FinSequence;

let h be Function of D,E;

coherence

for b

b

proof end;

registration

let X, Y be non empty set ;

let f be Function of X,Y;

let p be X -valued FinSequence;

coherence

f * p is FinSequence-like ;

end;
let f be Function of X,Y;

let p be X -valued FinSequence;

coherence

f * p is FinSequence-like ;

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;

coherence

for b_{1} being FinSequence of E st b_{1} = h * p holds

b_{1} is n -element
;

end;
let n be Nat;

let p be D -valued n -element FinSequence;

let h be Function of D,E;

coherence

for b

b

Lm3: for U being non empty set

for S being Language

for I being b

for t being termal string of S holds |.(ar t).| -tuples_on U = dom (I . ((S -firstChar) . t))

by FUNCT_2:def 1;

Lm4: for S being Language

for U being non empty set

for I being b

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;

ex b_{1} being sequence of (Funcs ((AllTermsOf S),U)) st

( b_{1} . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b_{1} . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b_{1} . mm),(S -subTerms)____ ) )

for b_{1}, b_{2} being sequence of (Funcs ((AllTermsOf S),U)) st b_{1} . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b_{1} . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b_{1} . mm),(S -subTerms)____ ) & b_{2} . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b_{2} . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b_{2} . mm),(S -subTerms)____ ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds it . (mm + 1) = ^^^(I * (S -firstChar)),^^^(it . mm),(S -subTerms)____ ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines -TermEval FOMODEL2:def 7 :

for S being Language

for U being non empty set

for u being Element of U

for I being b_{1},b_{2} -interpreter-like Function

for b_{5} being sequence of (Funcs ((AllTermsOf S),U)) holds

( b_{5} = (I,u) -TermEval iff ( b_{5} . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds b_{5} . (mm + 1) = ^^^(I * (S -firstChar)),^^^(b_{5} . mm),(S -subTerms)____ ) ) );

for S being Language

for U being non empty set

for u being Element of U

for I being b

for b

( b

Lm5: for S being Language

for U being non empty set

for u being Element of U

for I being b

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

for u1, u2 being Element of U

for m being Nat

for t being b

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;

ex b_{1} 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_{1} = (((I,u1) -TermEval) . (mm + 1)) . t

for b_{1}, b_{2} 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_{1} = (((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_{2} = (((I,u1) -TermEval) . (mm + 1)) . t ) holds

b_{1} = b_{2}

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

ex b

for u1 being Element of U

for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds

b

proof end;

uniqueness for b

for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds

b

for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds

b

b

proof end;

:: deftheorem Def8 defines -TermEval FOMODEL2:def 8 :

for S being Language

for U being non empty set

for I being b_{1},b_{2} -interpreter-like Function

for t being Element of AllTermsOf S

for b_{5} being Element of U holds

( b_{5} = I -TermEval t iff for u1 being Element of U

for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds

b_{5} = (((I,u1) -TermEval) . (mm + 1)) . t );

for S being Language

for U being non empty set

for I being b

for t being Element of AllTermsOf S

for b

( b

for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds

b

definition

let S be Language;

let U be non empty set ;

let I be S,U -interpreter-like Function;

ex b_{1} being Function of (AllTermsOf S),U st

for t being Element of AllTermsOf S holds b_{1} . t = I -TermEval t

for b_{1}, b_{2} being Function of (AllTermsOf S),U st ( for t being Element of AllTermsOf S holds b_{1} . t = I -TermEval t ) & ( for t being Element of AllTermsOf S holds b_{2} . t = I -TermEval t ) holds

b_{1} = b_{2}

end;
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 for t being Element of AllTermsOf S holds it . t = I -TermEval t;

ex b

for t being Element of AllTermsOf S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines -TermEval FOMODEL2:def 9 :

for S being Language

for U being non empty set

for I being b_{1},b_{2} -interpreter-like Function

for b_{4} being Function of (AllTermsOf S),U holds

( b_{4} = I -TermEval iff for t being Element of AllTermsOf S holds b_{4} . t = I -TermEval t );

for S being Language

for U being non empty set

for I being b

for b

( b

::############### Semantics of 0wff formulas (propositions) ############

::#########################################################################

::#########################################################################

definition

let S be Language;

let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter)) is Function ;

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter)) is Function ;

:: deftheorem defines === FOMODEL2:def 10 :

for S being Language

for U being non empty set

for I being b_{1},b_{2} -interpreter-like Function holds I === = I +* ((TheEqSymbOf S) .--> (U -deltaInterpreter));

for S being Language

for U being non empty set

for I being b

definition
end;

:: deftheorem Def11 defines -extension FOMODEL2:def 11 :

for S being Language

for U being non empty set

for I being b_{1},b_{2} -interpreter-like Function

for x being set holds

( x is I -extension iff x = I === );

for S being Language

for U being non empty set

for I being b

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;

coherence

for b_{1} being Function st b_{1} = I === holds

b_{1} is I -extension
;

coherence

for b_{1} being set st b_{1} is I -extension holds

b_{1} is Function-like
;

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

for b

b

coherence

for b

b

registration

let S be Language;

let U be non empty set ;

let I be S,U -interpreter-like Function;

existence

ex b_{1} being Function st b_{1} is I -extension

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

existence

ex b

proof end;

registration

let S be Language;

let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

I === is S,U -interpreter-like

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

I === is S,U -interpreter-like

proof 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

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

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;

((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) is set ;

end;
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));

((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi)) is set ;

:: deftheorem defines -AtomicEval FOMODEL2:def 12 :

for S being Language

for U being non empty set

for I being b_{1},b_{2} -interpreter-like Function

for phi being 0wff string of S holds I -AtomicEval phi = ((I ===) . ((S -firstChar) . phi)) . ((I -TermEval) * (SubTerms phi));

for S being Language

for U being non empty set

for I being b

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

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

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

coherence

for b_{1} being Function st b_{1} = I | (OwnSymbolsOf S) holds

b_{1} is PFuncs ((U *),(U \/ BOOLEAN)) -valued

for b_{1} being Function st b_{1} = I | (OwnSymbolsOf S) holds

b_{1} is S,U -interpreter-like

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let S be Language;

let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

for b_{1} being OwnSymbolsOf S -defined Relation st b_{1} = I | (OwnSymbolsOf S) holds

b_{1} is total

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

for b

b

proof end;

definition

let S be Language;

let U be non empty set ;

{ f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like } is set ;

end;
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 } ;

{ f where f is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) : f is S,U -interpreter-like } is set ;

:: deftheorem defines -InterpretersOf FOMODEL2:def 13 :

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

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)))))

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

registration

let S be Language;

let U be non empty set ;

coherence

for b_{1} being set st b_{1} = U -InterpretersOf S holds

not b_{1} is empty

end;
let U be non empty set ;

coherence

for b

not b

proof end;

registration

let S be Language;

let U be non empty set ;

coherence

for b_{1} being Element of U -InterpretersOf S holds b_{1} is S,U -interpreter-like

end;
let U be non empty set ;

coherence

for b

proof end;

definition

let S be Language;

let U be non empty set ;

ex b_{1} 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_{1} . (I,phi) = I -AtomicEval phi

for b_{1}, b_{2} 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_{1} . (I,phi) = I -AtomicEval phi ) & ( for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds b_{2} . (I,phi) = I -AtomicEval phi ) holds

b_{1} = b_{2}

end;
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 for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds it . (I,phi) = I -AtomicEval phi;

ex b

for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds b

proof end;

uniqueness for b

for phi being Element of AtomicFormulasOf S holds b

for phi being Element of AtomicFormulasOf S holds b

b

proof end;

:: deftheorem Def14 defines -TruthEval FOMODEL2:def 14 :

for S being Language

for U being non empty set

for b_{3} being Function of [:(U -InterpretersOf S),(AtomicFormulasOf S):],BOOLEAN holds

( b_{3} = S -TruthEval U iff for I being Element of U -InterpretersOf S

for phi being Element of AtomicFormulasOf S holds b_{3} . (I,phi) = I -AtomicEval phi );

for S being Language

for U being non empty set

for b

( b

for phi being Element of AtomicFormulasOf S holds b

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

( ( 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_{1} being Element of BOOLEAN holds verum
;

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

( ( 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

:: deftheorem Def15 defines -ExFunctor FOMODEL2:def 15 :

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

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

ex b_{1} 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_{1} 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_{1} holds

b_{1} . (x,y) = g -ExFunctor (x,y) ) )

for b_{1}, b_{2} 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_{1} 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_{1} holds

b_{1} . (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_{2} 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_{2} holds

b_{2} . (x,y) = g -ExFunctor (x,y) ) holds

b_{1} = b_{2}

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

ex b

( ( for x being Element of U -InterpretersOf S

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

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

b

proof end;

uniqueness for b

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

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

b

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

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

b

b

proof end;

:: deftheorem Def16 defines ExIterator FOMODEL2:def 16 :

for S being Language

for U being non empty set

for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)

for b_{4} being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds

( b_{4} = ExIterator g iff ( ( for x being Element of U -InterpretersOf S

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b_{4} 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_{4} holds

b_{4} . (x,y) = g -ExFunctor (x,y) ) ) );

for S being Language

for U being non empty set

for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)

for b

( b

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

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

b

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

( ( 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_{1} being Element of BOOLEAN holds verum
;

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

( ( 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

:: deftheorem Def17 defines -NorFunctor FOMODEL2:def 17 :

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

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.

::# 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);

ex b_{1} 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_{1} 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_{1} holds

b_{1} . (x,y) = g -NorFunctor (x,y) ) )

for b_{1}, b_{2} 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_{1} 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_{1} holds

b_{1} . (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_{2} 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_{2} holds

b_{2} . (x,y) = g -NorFunctor (x,y) ) holds

b_{1} = b_{2}

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

ex b

( ( for x being Element of U -InterpretersOf S

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

( 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

b

proof end;

uniqueness for b

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

( 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

b

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

( 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

b

b

proof end;

:: deftheorem Def18 defines NorIterator FOMODEL2:def 18 :

for S being Language

for U being non empty set

for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)

for b_{4} being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN holds

( b_{4} = NorIterator g iff ( ( for x being Element of U -InterpretersOf S

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b_{4} 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_{4} holds

b_{4} . (x,y) = g -NorFunctor (x,y) ) ) );

for S being Language

for U being non empty set

for g being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)

for b

( b

for y being Element of ((AllSymbolsOf S) *) \ {{}} holds

( [x,y] in dom b

( 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

b

definition

let S be Language;

let U be non empty set ;

ex b_{1} being sequence of (PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) st

( b_{1} . 0 = S -TruthEval U & ( for mm being Element of NAT holds b_{1} . (mm + 1) = ((ExIterator (b_{1} . mm)) +* (NorIterator (b_{1} . mm))) +* (b_{1} . mm) ) )

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

b_{1} = b_{2}

end;
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 ( it . 0 = S -TruthEval U & ( for mm being Element of NAT holds it . (mm + 1) = ((ExIterator (it . mm)) +* (NorIterator (it . mm))) +* (it . mm) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def19 defines -TruthEval FOMODEL2:def 19 :

for S being Language

for U being non empty set

for b_{3} being sequence of (PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN)) holds

( b_{3} = (S,U) -TruthEval iff ( b_{3} . 0 = S -TruthEval U & ( for mm being Element of NAT holds b_{3} . (mm + 1) = ((ExIterator (b_{3} . mm)) +* (NorIterator (b_{3} . mm))) +* (b_{3} . mm) ) ) );

for S being Language

for U being non empty set

for b

( b

theorem Th2: :: FOMODEL2:2

for S being Language

for U being non empty set

for I being b_{1},b_{2} -interpreter-like Function holds I | (OwnSymbolsOf S) in U -InterpretersOf S

for U being non empty set

for I being b

proof end;

definition

let S be Language;

let m be Nat;

let U be non empty set ;

ex b_{1} being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st

for mm being Element of NAT st m = mm holds

b_{1} = ((S,U) -TruthEval) . mm

for b_{1}, b_{2} being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) st ( for mm being Element of NAT st m = mm holds

b_{1} = ((S,U) -TruthEval) . mm ) & ( for mm being Element of NAT st m = mm holds

b_{2} = ((S,U) -TruthEval) . mm ) holds

b_{1} = b_{2}

end;
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 for mm being Element of NAT st m = mm holds

it = ((S,U) -TruthEval) . mm;

ex b

for mm being Element of NAT st m = mm holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def20 defines -TruthEval FOMODEL2:def 20 :

for S being Language

for m being Nat

for U being non empty set

for b_{4} being Element of PFuncs ([:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) holds

( b_{4} = (S,U) -TruthEval m iff for mm being Element of NAT st m = mm holds

b_{4} = ((S,U) -TruthEval) . mm );

for S being Language

for m being Nat

for U being non empty set

for b

( b

b

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;

(curry ((S,U) -TruthEval m)) . I is Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)

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

(curry ((S,U) -TruthEval m)) . I is Element of PFuncs ((((AllSymbolsOf S) *) \ {{}}),BOOLEAN)

proof end;

:: deftheorem defines -TruthEval FOMODEL2:def 21 :

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;

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

ex b_{1} 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_{1} = dom ((I,mm) -TruthEval)

for b_{1}, b_{2} 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_{1} = 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_{2} = dom ((I,mm) -TruthEval) ) holds

b_{1} = b_{2}

end;
let m be Nat;

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

ex b

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

proof end;

uniqueness for b

for I being Element of U -InterpretersOf S

for mm being Element of NAT st m = mm holds

b

for I being Element of U -InterpretersOf S

for mm being Element of NAT st m = mm holds

b

b

proof end;

:: deftheorem Def22 defines -formulasOfMaxDepth FOMODEL2:def 22 :

for S being Language

for m being Nat

for b_{3} being Subset of (((AllSymbolsOf S) *) \ {{}}) holds

( b_{3} = 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_{3} = dom ((I,mm) -TruthEval) );

for S being Language

for m being Nat

for b

( b

for I being Element of U -InterpretersOf S

for mm being Element of NAT st m = mm holds

b

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;

:: deftheorem Def23 defines -wff FOMODEL2:def 23 :

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

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

:: deftheorem Def24 defines wff FOMODEL2:def 24 :

for S being Language

for w being string of S holds

( w is wff iff ex m being Nat st w is m -wff );

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;

coherence

for b_{1} being string of S st b_{1} is 0 -wff holds

b_{1} is 0wff

for b_{1} being string of S st b_{1} is 0wff holds

b_{1} is 0 -wff

coherence

for b_{1} being string of S st b_{1} is m -wff holds

b_{1} is wff
;

let n be Nat;

coherence

for b_{1} being string of S st b_{1} is m + (0 * n) -wff holds

b_{1} is m + n -wff

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

let m be Nat;coherence

for b

b

let n be Nat;

coherence

for b

b

proof end;

registration

let S be Language;

let m be Nat;

ex b_{1} being string of S st b_{1} is m -wff

end;
let m be Nat;

cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like V210() m -wff for Element of ((AllSymbolsOf S) *) \ {{}};

existence ex b

proof end;

registration
end;

registration

let S be Language;

ex b_{1} being string of S st b_{1} is wff

end;
cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like V210() wff for Element of ((AllSymbolsOf S) *) \ {{}};

existence ex b

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

ex b_{1} being Element of BOOLEAN st

for m being Nat st w is m -wff holds

b_{1} = ((I,m) -TruthEval) . w

for b_{1}, b_{2} being Element of BOOLEAN st ( for m being Nat st w is m -wff holds

b_{1} = ((I,m) -TruthEval) . w ) & ( for m being Nat st w is m -wff holds

b_{2} = ((I,m) -TruthEval) . w ) holds

b_{1} = b_{2}

end;
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 for m being Nat st w is m -wff holds

it = ((I,m) -TruthEval) . w;

ex b

for m being Nat st w is m -wff holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def25 defines -TruthEval FOMODEL2:def 25 :

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_{5} being Element of BOOLEAN holds

( b_{5} = I -TruthEval w iff for m being Nat st w is m -wff holds

b_{5} = ((I,m) -TruthEval) . w );

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

( b

b

definition

let S be Language;

{ w where w is string of S : ex m being Nat st w is m -wff } is set ;

end;
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 } ;

{ w where w is string of S : ex m being Nat st w is m -wff } is set ;

:: deftheorem defines AllFormulasOf FOMODEL2:def 26 :

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

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

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_{2},b_{3} -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)) . {} ) )

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

( (((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

theorem :: FOMODEL2:5

theorem :: FOMODEL2:6

theorem :: FOMODEL2:7

definition

let S be Language;

let m be Nat;

for b_{1} being Subset of (((AllSymbolsOf S) *) \ {{}}) holds

( b_{1} = S -formulasOfMaxDepth m iff for U being non empty set

for I being Element of U -InterpretersOf S holds b_{1} = dom ((I,m) -TruthEval) )

end;
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 U being non empty set

for I being Element of U -InterpretersOf S holds it = dom ((I,m) -TruthEval);

for b

( b

for I being Element of U -InterpretersOf S holds b

proof end;

:: deftheorem Def27 defines -formulasOfMaxDepth FOMODEL2:def 27 :

for S being Language

for m being Nat

for b_{3} being Subset of (((AllSymbolsOf S) *) \ {{}}) holds

( b_{3} = S -formulasOfMaxDepth m iff for U being non empty set

for I being Element of U -InterpretersOf S holds b_{3} = dom ((I,m) -TruthEval) );

for S being Language

for m being Nat

for b

( b

for I being Element of U -InterpretersOf S holds b

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) )

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;

{ (<*v*> ^ phi) where v is Element of LettersOf S, phi is Element of S -formulasOfMaxDepth m : verum } is set ;

{ ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } is set ;

end;
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 } ;

{ (<*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 } ;

{ ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1, phi2 is Element of S -formulasOfMaxDepth m : verum } is set ;

:: deftheorem defines -ExFormulasOf FOMODEL2:def 28 :

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

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 29 :

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

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)

for S being Language holds S -formulasOfMaxDepth (m + 1) = ((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m)

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = AtomicFormulasOf S holds

b_{1} is S -prefix
by Th10;

end;
coherence

for b

b

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = S -formulasOfMaxDepth 0 holds

b_{1} is S -prefix

end;
coherence

for b

b

proof end;

definition

let S be Language;

let phi be wff string of S;

ex b_{1} being Nat st

( phi is b_{1} -wff & ( for n being Nat st phi is n -wff holds

b_{1} <= n ) )

for b_{1}, b_{2} being Nat st phi is b_{1} -wff & ( for n being Nat st phi is n -wff holds

b_{1} <= n ) & phi is b_{2} -wff & ( for n being Nat st phi is n -wff holds

b_{2} <= n ) holds

b_{1} = b_{2}

end;
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 ( phi is it -wff & ( for n being Nat st phi is n -wff holds

it <= n ) );

ex b

( phi is b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def30 defines Depth FOMODEL2:def 30 :

for S being Language

for phi being wff string of S

for b_{3} being Nat holds

( b_{3} = Depth phi iff ( phi is b_{3} -wff & ( for n being Nat st phi is n -wff holds

b_{3} <= n ) ) );

for S being Language

for phi being wff string of S

for b

( b

b

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

ex phi1, phi2 being b

proof end;

registration

let S be Language;

let m be Nat;

let phi1, phi2 be m -wff string of S;

coherence

for b_{1} being string of S st b_{1} = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds

b_{1} is m + 1 -wff

end;
let m be Nat;

let phi1, phi2 be m -wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let phi1, phi2 be wff string of S;

coherence

for b_{1} being string of S st b_{1} = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds

b_{1} is wff

end;
let phi1, phi2 be wff string of S;

coherence

for b

b

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

coherence

for b_{1} being string of S st b_{1} = <*v*> ^ phi holds

b_{1} is m + 1 -wff

end;
let m be Nat;

let phi be m -wff string of S;

let v be literal Element of S;

coherence

for b

b

proof end;

registration

let S be Language;

let l be literal Element of S;

let phi be wff string of S;

coherence

for b_{1} being string of S st b_{1} = <*l*> ^ phi holds

b_{1} is wff

end;
let l be literal Element of S;

let phi be wff string of S;

coherence

for b

b

proof end;

registration

let S be Language;

let w be string of S;

let s be non relational Element of S;

coherence

for b_{1} being string of S st b_{1} = <*s*> ^ w holds

not b_{1} is 0wff

end;
let w be string of S;

let s be non relational Element of S;

coherence

for b

not b

proof end;

registration

let S be Language;

let w1, w2 be string of S;

let s be non relational Element of S;

coherence

for b_{1} being string of S st b_{1} = (<*s*> ^ w1) ^ w2 holds

not b_{1} is 0wff

end;
let w1, w2 be string of S;

let s be non relational Element of S;

coherence

for b

not b

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of S st b_{1} = TheNorSymbOf S holds

not b_{1} is relational
;

end;
coherence

for b

not b

registration

let S be Language;

let w be string of S;

coherence

for b_{1} being string of S st b_{1} = <*(TheNorSymbOf S)*> ^ w holds

not b_{1} is 0wff
;

end;
let w be string of S;

coherence

for b

not b

registration

let S be Language;

let l be literal Element of S;

let w be string of S;

coherence

for b_{1} being string of S st b_{1} = <*l*> ^ w holds

not b_{1} is 0wff
;

end;
let l be literal Element of S;

let w be string of S;

coherence

for b

not b

:: deftheorem Def31 defines exal FOMODEL2:def 31 :

for S being Language

for w being string of S holds

( w is exal iff (S -firstChar) . w is literal );

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;

coherence

for b_{1} being string of S st b_{1} = <*l*> ^ w holds

b_{1} is exal

end;
let w be string of S;

let l be literal Element of S;

coherence

for b

b

proof end;

registration

let S be Language;

let m1 be non zero Nat;

ex b_{1} being m1 -wff string of S st b_{1} is exal

end;
let m1 be non zero Nat;

cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like V210() m1 -wff wff exal for Element of ((AllSymbolsOf S) *) \ {{}};

existence ex b

proof end;

registration
end;

registration

let S be Language;

let m1 be non zero Nat;

not for b_{1} being m1 -wff exal string of S holds b_{1} is 0wff

end;
let m1 be non zero Nat;

cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like V210() non 0wff m1 -wff wff exal for Element of ((AllSymbolsOf S) *) \ {{}};

existence not for b

proof end;

registration

let S be Language;

not for b_{1} being wff exal string of S holds b_{1} is 0wff

end;
cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like V210() non 0wff wff exal for Element of ((AllSymbolsOf S) *) \ {{}};

existence not for b

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

coherence

for b_{1} being Nat st b_{1} = Depth phi holds

not b_{1} is zero
by Lm22;

end;
let phi be non 0wff wff string of S;

coherence

for b

not b

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;

coherence

for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

not b_{1} is relational

end;
let w be non 0wff wff string of S;

coherence

for b

not b

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

coherence

for b_{1} being set st b_{1} = S -formulasOfMaxDepth m holds

b_{1} is S -prefix
by Lm24;

end;
let m be Nat;

coherence

for b

b

definition

let S be Language;

:: original: AllFormulasOf

redefine func AllFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}});

coherence

AllFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})

end;
:: original: AllFormulasOf

redefine func AllFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}});

coherence

AllFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of AllFormulasOf S holds b_{1} is wff

end;
coherence

for b

proof end;

Lm25: for S being Language holds AllFormulasOf S is S -prefix

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = AllFormulasOf S holds

b_{1} is S -prefix
by Lm25;

end;
coherence

for b

b

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;

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;

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;
:: original: TheEqSymbOf

redefine func TheEqSymbOf S -> Element of S;

coherence

TheEqSymbOf S is Element of S ;

registration

let S be Language;

coherence

for b_{1} being number st b_{1} = (ar (TheEqSymbOf S)) + 2 holds

b_{1} is zero

for b_{1} being number st b_{1} = |.(ar (TheEqSymbOf S)).| - 2 holds

b_{1} is zero

end;
coherence

for b

b

proof end;

coherence for b

b

proof 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_{1},b_{2} -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)) ) )

for U being non empty set

for phi being 0wff string of S

for I being b

( ( (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_{1},b_{2} -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) )

for U being non empty set

for I being b

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;

coherence

for b_{1} being set st b_{1} = m -ExFormulasOf S holds

not b_{1} is empty

end;
let m be Nat;

coherence

for b

not b

proof end;

registration

let S be Language;

let m be Nat;

coherence

for b_{1} being set st b_{1} = m -NorFormulasOf S holds

not b_{1} is empty

end;
let m be Nat;

coherence

for b

not b

proof 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) *) \ {{}})

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

registration

let S be Language;

let w be exal string of S;

coherence

for b_{1} being Element of S st b_{1} = (S -firstChar) . w holds

b_{1} is literal
by Def31;

end;
let w be exal string of S;

coherence

for b

b

registration

let S be Language;

let m be Nat;

coherence

for b_{1} being Element of m -NorFormulasOf S holds not b_{1} is exal

end;
let m be Nat;

coherence

for b

proof end;

Lm27: for m being Nat

for S being Language

for phi being wff string of S st Depth phi = m + 1 & phi is exal holds

phi in m -ExFormulasOf S

by Def30;

Lm28: for S being Language

for l being literal Element of S

for phi1 being wff string of S holds Depth (<*l*> ^ phi1) > Depth phi1

by Def30;

definition

let S be Language;

let m be Nat;

:: original: -ExFormulasOf

redefine func m -ExFormulasOf S -> Subset of (((AllSymbolsOf S) *) \ {{}});

coherence

m -ExFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}})

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

registration

let S be Language;

let m be Nat;

coherence

for b_{1} being Element of m -ExFormulasOf S holds b_{1} is exal

end;
let m be Nat;

coherence

for b

proof end;

Lm29: for m being Nat

for S being Language

for phi being wff string of S st Depth phi = m + 1 & not phi is exal holds

phi in m -NorFormulasOf S

by Def30;

registration
end;

registration

let S be Language;

let w be string of S;

let s be non literal Element of S;

coherence

for b_{1} being string of S st b_{1} = <*s*> ^ w holds

not b_{1} is exal

end;
let w be string of S;

let s be non literal Element of S;

coherence

for b

not b

proof end;

registration

let S be Language;

let w1, w2 be string of S;

let s be non literal Element of S;

coherence

for b_{1} being string of S st b_{1} = (<*s*> ^ w1) ^ w2 holds

not b_{1} is exal

end;
let w1, w2 be string of S;

let s be non literal Element of S;

coherence

for b

not b

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of S st b_{1} = TheNorSymbOf S holds

not b_{1} is literal
;

end;
coherence

for b

not b

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 )

by Def30;

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

by Def30;

registration

let m be Nat;

let S be Language;

coherence

for b_{1} being string of S st not b_{1} is m -wff holds

b_{1} is m -nonwff
;

end;
let S be Language;

coherence

for b

b

registration

let S be Language;

let phi1, phi2 be wff string of S;

for b_{1} being string of S st b_{1} = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds

not b_{1} is max ((Depth phi1),(Depth phi2)) -wff

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

not b

proof end;

registration

let S be Language;

let phi be wff string of S;

let l be literal Element of S;

coherence

for b_{1} being string of S st b_{1} = <*l*> ^ phi holds

not b_{1} is Depth phi -wff

end;
let phi be wff string of S;

let l be literal Element of S;

coherence

for b

not b

proof end;

registration

let S be Language;

let phi be wff string of S;

let l be literal Element of S;

coherence

for b_{1} being string of S st b_{1} = <*l*> ^ phi holds

b_{1} is 1 + (Depth phi) -wff

end;
let phi be wff string of S;

let l be literal Element of S;

coherence

for b

b

proof end;

Lm32: for S being Language

for U being non empty set

for I being Relation st I in U -InterpretersOf S holds

dom I = OwnSymbolsOf S

proof end;

registration

let S be Language;

let U be non empty set ;

coherence

for b_{1} being Element of U -InterpretersOf S holds b_{1} is OwnSymbolsOf S -defined

end;
let U be non empty set ;

coherence

for b

proof end;

registration

let S be Language;

let U be non empty set ;

ex b_{1} being Element of U -InterpretersOf S st b_{1} is OwnSymbolsOf S -defined

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

proof end;

registration

let S be Language;

let U be non empty set ;

for b_{1} being OwnSymbolsOf S -defined Element of U -InterpretersOf S holds b_{1} is total

end;
let U be non empty set ;

cluster OwnSymbolsOf S -defined -> OwnSymbolsOf S -defined total for Element of U -InterpretersOf S;

coherence for b

proof 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

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

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

:: deftheorem defines xnot FOMODEL2:def 32 :

for S being Language

for w being string of S holds xnot w = (<*(TheNorSymbOf S)*> ^ w) ^ w;

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;

coherence

for b_{1} being string of S st b_{1} = xnot phi holds

b_{1} is m + 1 -wff
;

end;
let m be Nat;

let phi be m -wff string of S;

coherence

for b

b

registration

let S be Language;

let phi be wff string of S;

coherence

for b_{1} being string of S st b_{1} = xnot phi holds

b_{1} is wff
;

end;
let phi be wff string of S;

coherence

for b

b

registration

let S be Language;

coherence

for b_{1} being Element of S st b_{1} = TheEqSymbOf S holds

not b_{1} is own

end;
coherence

for b

not b

proof end;

:: deftheorem defines -mincover FOMODEL2:def 33 :

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

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

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;

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_{2},b_{3} -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m)

for S being Language

for U being non empty set

for u being Element of U

for I being b

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_{1},b_{2} -interpreter-like Function holds (I -TermEval) . t = (I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t))

for U being non empty set

for t being termal string of S

for I being b

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_{1}[ 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 );

( ( not phi is 0wff implies ex b_{1} being set ex phi1 being wff string of S ex p being FinSequence st

( p is AllSymbolsOf S -valued & b_{1} = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) & ( phi is 0wff implies ex b_{1} being set st b_{1} = [phi,{}] ) )

for b_{1}, b_{2} 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_{1} = [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_{2} = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) implies b_{1} = b_{2} ) & ( phi is 0wff & b_{1} = [phi,{}] & b_{2} = [phi,{}] implies b_{1} = b_{2} ) )

for b_{1} being set holds verum
;

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

( 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 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,{}];

( ( not phi is 0wff implies ex b

( p is AllSymbolsOf S -valued & b

proof end;

uniqueness for b

( ( not phi is 0wff & ex phi1 being wff string of S ex p being FinSequence st

( p is AllSymbolsOf S -valued & b

( p is AllSymbolsOf S -valued & b

proof end;

consistency for b

:: deftheorem Def34 defines SubWffsOf FOMODEL2:def 34 :

for S being Language

for phi being wff string of S

for b_{3} being set holds

( ( not phi is 0wff implies ( b_{3} = SubWffsOf phi iff ex phi1 being wff string of S ex p being FinSequence st

( p is AllSymbolsOf S -valued & b_{3} = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) ) ) & ( phi is 0wff implies ( b_{3} = SubWffsOf phi iff b_{3} = [phi,{}] ) ) );

for S being Language

for phi being wff string of S

for b

( ( not phi is 0wff implies ( b

( p is AllSymbolsOf S -valued & b

definition

let S be Language;

let phi be wff string of S;

set IT = SubWffsOf phi;

set SS = AllSymbolsOf S;

set F = S -firstChar ;

coherence

(SubWffsOf phi) `1 is wff string of S

(SubWffsOf phi) `2 is Element of (AllSymbolsOf S) *

end;
let phi be wff string of S;

set IT = SubWffsOf phi;

set SS = AllSymbolsOf S;

set F = S -firstChar ;

coherence

(SubWffsOf phi) `1 is wff string of S

proof end;

coherence (SubWffsOf phi) `2 is Element of (AllSymbolsOf S) *

proof end;

:: deftheorem defines head FOMODEL2:def 35 :

for S being Language

for phi being wff string of S holds head phi = (SubWffsOf phi) `1 ;

for S being Language

for phi being wff string of S holds head phi = (SubWffsOf phi) `1 ;

:: deftheorem defines tail FOMODEL2:def 36 :

for S being Language

for phi being wff string of S holds tail phi = (SubWffsOf phi) `2 ;

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;

coherence

for b_{1} being set st b_{1} = (S -formulasOfMaxDepth m) \ (AllFormulasOf S) holds

b_{1} is empty

end;
let m be Nat;

coherence

for b

b

proof end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = (AtomicFormulasOf S) \ (AllFormulasOf S) holds

b_{1} is empty

end;
coherence

for b

b

proof end;

theorem :: FOMODEL2:22

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 ) )

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;

not for b_{1} being non 0wff m1 -wff string of S holds b_{1} is exal

end;
let m1 be non zero Nat;

cluster non empty Relation-like omega -defined Function-like non zero finite FinSequence-like FinSubsequence-like V210() non 0wff m1 -wff wff non exal for Element of ((AllSymbolsOf S) *) \ {{}};

existence not for b

proof end;

registration

let S be Language;

let phi be wff exal string of S;

coherence

for b_{1} being set st b_{1} = tail phi holds

b_{1} is empty

end;
let phi be wff exal string of S;

coherence

for b

b

proof 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

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

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

registration

let S be Language;

let phi be non 0wff wff non exal string of S;

coherence

for b_{1} being string of S st b_{1} = tail phi holds

b_{1} is wff
;

end;
let phi be non 0wff wff non exal string of S;

coherence

for b

b

registration
end;

registration

let S be Language;

let phi be non 0wff wff non exal string of S;

coherence

for b_{1} being set st b_{1} = ((S -firstChar) . phi) \+\ (TheNorSymbOf S) holds

b_{1} is empty

end;
let phi be non 0wff wff non exal string of S;

coherence

for b

b

proof 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

proof end;

registration

let m be Nat;

let S be Language;

let phi be m + 1 -wff string of S;

coherence

for b_{1} being string of S st b_{1} = head phi holds

b_{1} is m -wff

end;
let S be Language;

let phi be m + 1 -wff string of S;

coherence

for b

b

proof end;

registration

let m be Nat;

let S be Language;

let phi be non 0wff m + 1 -wff non exal string of S;

coherence

for b_{1} being string of S st b_{1} = tail phi holds

b_{1} is m -wff
by Lm39;

end;
let S be Language;

let phi be non 0wff m + 1 -wff non exal string of S;

coherence

for b

b

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)

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;

compatibility

I -TruthEval phi0 = I -AtomicEval phi0 by Lm40;

compatibility

I -AtomicEval phi0 = I -TruthEval phi0 ;

end;
let U be non empty set ;

let I be Element of U -InterpretersOf S;

let phi0 be 0wff string of S;

compatibility

I -TruthEval phi0 = I -AtomicEval phi0 by Lm40;

compatibility

I -AtomicEval phi0 = I -TruthEval phi0 ;

registration

let S be Language;

existence

not for b_{1} being ofAtomicFormula Element of S holds b_{1} is literal

end;
existence

not for b

proof end;

Lm41: for X being set

for S being Language

for U being non empty set

for I1, I2 being b

(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_{1},b_{2} -interpreter-like Function st not l2 in rng p holds

(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p

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

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

end;
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);

s in SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ X);

:: deftheorem Def37 defines -occurring FOMODEL2:def 37 :

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

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 ;

end;
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));

s in SymbolsOf (((AllSymbolsOf S) *) \ ({{}} /\ X));

:: deftheorem defines -containing FOMODEL2:def 38 :

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

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

notation
end;

registration

let X be finite set ;

let S be Language;

ex b_{1} being literal Element of S st b_{1} is X -absent

end;
let S be Language;

cluster literal non operational non relational termal own ofAtomicFormula X -absent for Element of AllSymbolsOf S;

existence ex b

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

coherence

for b_{1} being set st b_{1} = (rng t) /\ (LettersOf S) holds

not b_{1} is empty
by Lm42;

end;
let t be termal string of S;

coherence

for b

not b

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;

coherence

for b_{1} being set st b_{1} = (rng phi) /\ (LettersOf S) holds

not b_{1} is empty
by Lm43;

end;
let phi be wff string of S;

coherence

for b

not b

registration

let B be set ;

let S be Language;

let A be Subset of B;

coherence

for b_{1} being Element of S st b_{1} is A -occurring holds

b_{1} is B -occurring

end;
let S be Language;

let A be Subset of B;

coherence

for b

b

proof end;

registration

let A, B be set ;

let S be Language;

coherence

for b_{1} being Element of S st b_{1} is A null B -absent holds

b_{1} is A /\ B -absent
;

end;
let S be Language;

coherence

for b

b

registration

let F be finite set ;

let A be set ;

let S be Language;

coherence

for b_{1} being F -absent Element of S st b_{1} is A -absent holds

b_{1} is A \/ F -absent

end;
let A be set ;

let S be Language;

coherence

for b

b

proof end;

registration

let S be Language;

let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

for b_{1} being set st b_{1} = (OwnSymbolsOf S) \ (dom I) holds

b_{1} is empty

end;
let U be non empty set ;

let I be S,U -interpreter-like Function;

coherence

for b

b

proof 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_{1},b_{2} -interpreter-like Function ex u being Element of U st

( u = (I . l) . {} & (l,u) ReassignIn I = I )

for U being non empty set

for l being literal Element of S

for I being b

( u = (I . l) . {} & (l,u) ReassignIn I = I )

proof end;

:: deftheorem defines -covering FOMODEL2:def 39 :

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

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;

coherence

for b_{1} being set st b_{1} is S -mincover holds

b_{1} is S -covering
;

end;
coherence

for b

b

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;

for b_{1} being set st b_{1} = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds

b_{1} is empty

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

b

proof end;

definition

let S be Language;

{ phi where phi is string of S : ( phi is wff & phi is exal ) } is Subset of (((AllSymbolsOf S) *) \ {{}})

end;
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 ) } ;

{ phi where phi is string of S : ( phi is wff & phi is exal ) } is Subset of (((AllSymbolsOf S) *) \ {{}})

proof end;

:: deftheorem defines ExFormulasOf FOMODEL2:def 40 :

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

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;

coherence

for b_{1} being set st b_{1} = ExFormulasOf S holds

not b_{1} is empty

end;
coherence

for b

not b

proof end;

registration

let S be Language;

coherence

for b_{1} being Element of ExFormulasOf S holds

( b_{1} is exal & b_{1} is wff )

end;
coherence

for b

( b

proof end;

registration
end;

registration
end;

registration

let S be Language;

coherence

for b_{1} being set st b_{1} = (ExFormulasOf S) \ (AllFormulasOf S) holds

b_{1} is empty

end;
coherence

for b

b

proof end;

registration

let U be non empty set ;

let S1 be Language;

let S2 be S1 -extending Language;

coherence

for b_{1} being Function st b_{1} is S2,U -interpreter-like holds

b_{1} is S1,U -interpreter-like

end;
let S1 be Language;

let S2 be S1 -extending Language;

coherence

for b

b

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

coherence

for b_{1} being Function st b_{1} = I | (OwnSymbolsOf S1) holds

b_{1} is S1,U -interpreter-like
;

end;
let S1 be Language;

let S2 be S1 -extending Language;

let I be S2,U -interpreter-like Function;

coherence

for b

b

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;

coherence

I2 +* I1 is S2,U -interpreter-like

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

coherence

I2 +* I1 is S2,U -interpreter-like

proof end;

definition

let U be non empty set ;

let S be Language;

let I be Element of U -InterpretersOf S;

let X be set ;

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

for phi being wff string of S st phi in X holds

I -TruthEval phi = 1;

:: deftheorem Def41 defines -satisfied FOMODEL2:def 41 :

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

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

:: deftheorem defines -satisfying FOMODEL2:def 42 :

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

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;

coherence

for b_{1} being set st b_{1} = e null I holds

b_{1} is I -satisfied
;

end;
let S be Language;

let e be empty set ;

let I be Element of U -InterpretersOf S;

coherence

for b

b

registration

let X be set ;

let U be non empty set ;

let S be Language;

let I be Element of U -InterpretersOf S;

existence

ex b_{1} being Subset of X st b_{1} is I -satisfied

end;
let U be non empty set ;

let S be Language;

let I be Element of U -InterpretersOf S;

existence

ex b

proof end;

registration

let U be non empty set ;

let S be Language;

let I be Element of U -InterpretersOf S;

existence

ex b_{1} being set st b_{1} is I -satisfied

end;
let S be Language;

let I be Element of U -InterpretersOf S;

existence

ex b

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

coherence

for b_{1} being Subset of X holds b_{1} is I -satisfied
by Def41;

end;
let S be Language;

let I be Element of U -InterpretersOf S;

let X be I -satisfied set ;

coherence

for b

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 ;

coherence

X \/ Y is I -satisfied

end;
let S be Language;

let I be Element of U -InterpretersOf S;

let X, Y be I -satisfied set ;

coherence

X \/ Y is I -satisfied

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

coherence

for b_{1} being Element of U -InterpretersOf S st b_{1} = I null X holds

b_{1} is X -satisfying
;

end;
let S be Language;

let I be Element of U -InterpretersOf S;

let X be I -satisfied set ;

coherence

for b

b

definition

let S be Language;

let X be set ;

end;
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_{2} -satisfied set

for phi being wff string of S st [x,phi] in X holds

I -TruthEval phi = 1;

for U being non empty set

for I being Element of U -InterpretersOf S

for x being b

for phi being wff string of S st [x,phi] in X holds

I -TruthEval phi = 1;

:: deftheorem defines -correct FOMODEL2:def 43 :

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_{4} -satisfied set

for phi being wff string of S st [x,phi] in X holds

I -TruthEval phi = 1 );

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

for phi being wff string of S st [x,phi] in X holds

I -TruthEval phi = 1 );

registration
end;

registration

let S be Language;

let X be set ;

existence

ex b_{1} being Subset of X st b_{1} is S -correct

end;
let X be set ;

existence

ex b

proof 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 )

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;

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;

for b_{1} being set st b_{1} = (I -TruthEval ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2)) holds

b_{1} is empty

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

b

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

coherence

for b_{1} being set st b_{1} = (I -TruthEval (xnot phi)) \+\ ('not' (I -TruthEval phi)) holds

b_{1} is empty

end;
let phi be wff string of S;

let U be non empty set ;

let I be Element of U -InterpretersOf S;

coherence

for b

b

proof end;

definition

let X be set ;

let S be Language;

let phi be wff string of S;

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

for U being non empty set

for I being Element of U -InterpretersOf S st X is I -satisfied holds

I -TruthEval phi = 1;

:: deftheorem defines -implied FOMODEL2:def 44 :

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

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;

coherence

(head (<*l*> ^ phi)) \+\ phi is empty

end;
let l be literal Element of S;

let phi be wff string of S;

coherence

(head (<*l*> ^ phi)) \+\ phi is empty

proof end;

::###############################################################

::###############################################################

::# Interpreter of a Language.