:: First order languages: syntax, part two; semantics
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1,
FUNCT_2, FINSEQ_1, FUNCT_1, ARYTM_3, XCMPLX_0, CARD_1, MONOID_0,
ORDINAL1, ARYTM_1, XXREAL_0, ORDINAL4, PARTFUN1, FINSEQ_2, EQREL_1,
COMPLEX1, FUNCT_3, MCART_1, FUNCT_4, FUNCOP_1, MARGREL1, XBOOLEAN,
RFINSEQ, FUNCT_5, FINSET_1, FOMODEL0, FOMODEL1, FOMODEL2;
notations TARSKI, XTUPLE_0, XFAMILY, XBOOLEAN, MARGREL1, MONOID_0, XBOOLE_0,
ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
BINOP_1, RFUNCT_3, FUNCOP_1, FUNCT_4, MCART_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, INT_2, FINSEQ_1, EQREL_1, FINSEQ_2, RELSET_1,
RFINSEQ, FINSEQOP, FUNCT_5, FINSET_1, FOMODEL0, FOMODEL1, BVFUNC_1;
constructors TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, NAT_1, NUMBERS, INT_1,
ARYTM_3, FINSEQ_1, XCMPLX_0, FUNCT_1, MONOID_0, XXREAL_0, RELAT_2,
RFINSEQ, FUNCT_2, FUNCT_4, FUNCT_7, FUNCOP_1, FINSEQ_2, EQREL_1,
COMPLEX1, RELSET_1, MCART_1, PARTFUN1, FINSEQOP, MATRIX_1, FUNCT_3,
SETFAM_1, PRE_POLY, FINSET_1, BINOP_1, FUNCT_5, RFUNCT_3, STRUCT_0,
XTUPLE_0, FOMODEL0, FOMODEL1, XFAMILY, BVFUNC_1;
registrations ORDINAL1, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, INT_1, FINSEQ_1,
XREAL_0, FUNCT_2, FINSEQ_2, SUBSET_1, FUNCOP_1, RELSET_1, FUNCT_4,
PARTFUN1, FINSEQ_6, CARD_1, XBOOLE_0, SETFAM_1, MARGREL1, FINSET_1,
RAMSEY_1, XBOOLEAN, FOMODEL0, FOMODEL1, XTUPLE_0;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TARSKI;
equalities TARSKI, FINSEQ_1, XBOOLE_0, FUNCOP_1, XBOOLEAN, BINOP_1, FOMODEL0,
FOMODEL1;
expansions TARSKI, XBOOLE_0, BINOP_1, FOMODEL0, FOMODEL1;
theorems TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, RELAT_1, XBOOLE_1, ZFMISC_1,
FUNCT_2, XXREAL_0, NAT_1, ORDINAL1, EQREL_1, PARTFUN1, FINSEQ_2, XREAL_1,
MCART_1, FUNCT_4, FUNCOP_1, FUNCT_5, FUNCT_6, FINSEQ_6, RELSET_1,
GRFUNC_1, FOMODEL0, FOMODEL1, DOMAIN_1, ABSVALUE, FUNCT_7, CARD_1;
schemes NAT_1, FUNCT_1, FUNCT_2, CLASSES1, RECDEF_1, DOMAIN_1, BINOP_1,
FRAENKEL;
begin
reserve k,m,n for Nat, kk,mm,nn for Element of NAT, A,B,X,Y,Z,x,y,z for set,
S, S1, S2 for Language, s for (Element of S), w,w1,w2 for (string of S),
U,U1,U2 for non empty set, f,g for Function, p,p1,p2 for FinSequence;
definition
let S;
redefine func TheNorSymbOf S -> Element of S; :: redefines TheNorSymbOf (FOMODEL1, definition)
coherence;
end;
definition
let U be non empty set;
func U-deltaInterpreter -> Function of (2-tuples_on U), BOOLEAN equals
chi((U-concatenation) .: (id (1-tuples_on U)), 2-tuples_on U);
coherence;
end;
definition
let X be set;
redefine func id X -> Equivalence_Relation of X; :: redefines id (RELAT_1, definition)
coherence by EQREL_1:3;
end;
definition
let S be Language; let U be non empty set;
let s be ofAtomicFormula Element of S;
mode Interpreter of s, U -> set means :Def2:
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
proof
thus s is relational implies ex IT being set st IT is
Function of |.ar s.|-tuples_on U, BOOLEAN
proof
assume s is relational;
take the Function of |.ar s.|-tuples_on U, BOOLEAN; thus thesis;
end;
assume not s is relational;
take the Function of |.ar s.|-tuples_on U, U; thus thesis;
end;
consistency;
end;
definition
let S,U; let s be ofAtomicFormula Element of S;
redefine mode Interpreter of s,U -> :: redefines Interpreter (FOMODEL2, definition)
Function of |.ar s.|-tuples_on U, U\/BOOLEAN;
coherence
proof
let f be Interpreter of s,U;
set n=|.ar s.|, D=n-tuples_on U, C=U\/BOOLEAN;
D c= D\/{}; then reconsider DD=D as Subset of D;
reconsider C1=BOOLEAN,C2=U as Subset of C by XBOOLE_1:7;
per cases;
suppose s is relational; then
reconsider ff=f as Function of DD, C1 by Def2;
[: DD, C1 :] c= [:D,C:]; then
reconsider fff=ff as Relation of D,C by XBOOLE_1:1; fff is Function of D,C;
hence thesis;
end;
suppose not s is relational; then
reconsider ff=f as Function of DD, C2 by Def2;
[: DD, C2 :] c= [:D,C:]; then
reconsider fff=ff as Relation of D,C by XBOOLE_1:1; fff is Function of D,C;
hence thesis;
end;
end;
end;
registration
let S,U; let s be termal Element of S;
cluster -> U-valued for Interpreter of s,U;
coherence by Def2;
end;
registration
let S be Language;
cluster literal -> own for Element of S;
coherence;
end;
::###############################################################
::###############################################################
::###############################################################
::# Interpreter of a Language.
definition
let S, U;
mode Interpreter of S, U -> Function means :Def3:
for s being own Element of S holds it.s is Interpreter of s, U;
existence
proof
set O=OwnSymbolsOf S;
defpred P[object,object] means ex s being own Element of S st $1=s &
$2 is Interpreter of s,U;
A1: for x being object st x in O ex y being object st P[x,y]
proof
let x be object; assume x in O; then
reconsider s=x as own Element of S by FOMODEL1:def 19;
take y=the Interpreter of s, U; take s;
thus x=s & y is Interpreter of s, U;
end;
consider f being Function such that A2: dom f = O &
for s being object st s in O holds P[s,f.s] from CLASSES1:sch 1(A1); take f;
thus for s being own Element of S holds f.s is Interpreter of s,U
proof
let s be own Element of S;
consider s1 being own Element of S such that
A3: s=s1 & f.s is Interpreter of s1,U by A2, FOMODEL1:def 19;
thus f.s is Interpreter of s,U by A3;
end;
end;
end;
definition
let S, U, f;
attr f is (S,U)-interpreter-like means :Def4:
f is Interpreter of S,U & f is Function-yielding;
end;
registration
let S; let U be non empty set;
cluster (S,U)-interpreter-like -> Function-yielding for Function;
coherence;
end;
registration
let S,U; let s be own Element of S;
cluster -> non empty for Interpreter of s,U;
coherence;
end;
Lm1: for f being Interpreter of S,U holds OwnSymbolsOf S c= dom f
proof
set SS=AllSymbolsOf S, A=AtomicFormulaSymbolsOf S, O=OwnSymbolsOf S;
let f be Interpreter of S,U;
let x be object; assume x in O; then
reconsider s=x as own Element of S by FOMODEL1:def 19;
f.s is non empty by Def3; hence x in dom f by FUNCT_1:def 2;
end;
Lm2: f is (S,U)-interpreter-like implies OwnSymbolsOf S c= dom f
by Lm1;
registration
let S be Language;
let U be non empty set;
cluster (S,U)-interpreter-like for Function;
existence
proof
set O=OwnSymbolsOf S, SS=AllSymbolsOf S;
set I = the Interpreter of S,U; reconsider f=I|O as Function;
A1: dom f= O /\ dom I by RELAT_1:61 .= O by XBOOLE_1:28, Lm1;
take f; A2: for s being own Element of S holds
f.s is Interpreter of s,U & f.s is Function
proof
let s be own Element of S;
A3: f.s=I.s by FUNCT_1:47, A1, FOMODEL1:def 19;
hence f.s is Interpreter of s,U by Def3;
thus f.s is Function by A3, Def3;
end;
then reconsider ff=f as Interpreter of S,U by Def3;
now
let x be object; assume x in dom f; then reconsider
s=x as own Element of S by A1, FOMODEL1:def 19; ff.s is Function by A2;
hence ff.x is Function;
end;
hence thesis by FUNCOP_1:def 6;
end;
end;
definition
let S,U;
let I be (S,U)-interpreter-like Function;
let s be own Element of S;
redefine func I.s -> Interpreter of s,U; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider I as Interpreter of S,U by Def4;
I.s is Interpreter of s,U by Def3; hence thesis;
end;
end;
registration
let S be Language, U be non empty set;
let I be (S,U)-interpreter-like Function;
let x be own Element of S, f be Interpreter of x, U;
cluster I +* (x .--> f) -> (S,U)-interpreter-like;
coherence
proof
set g=x .--> f, O=OwnSymbolsOf S, h=I +* g;
O c= dom I & dom I c= dom I \/ dom g by Lm2, XBOOLE_1:7;
then
A1: O c= dom I \/ dom g;
reconsider I as Interpreter of S,U by Def4;
now
let s be own Element of S;
A2: s in O by FOMODEL1:def 19;
per cases;
suppose
A3: s in dom g; then
A4: h.s = g.s by FUNCT_4:def 1, A2, A1
.= f by FUNCOP_1:7, A3;
thus h.s is Interpreter of s,U by A4, A3, TARSKI:def 1;
end;
suppose not s in dom g; then h.s=I.s by FUNCT_4:def 1, A1, A2;
hence h.s is Interpreter of s,U by Def3;
end;
end;
then h is Interpreter of S,U & h is Function-yielding by Def3;
hence thesis;
end;
end;
definition
let f,x,y;
func (x,y) ReassignIn f -> Function equals
f +* (x .--> ({} .--> y));
coherence;
end;
registration
let S be Language,U be non empty set,I be (S,U)-interpreter-like Function;
let x be literal Element of S, u be Element of U;
cluster (x,u) ReassignIn I -> (S,U)-interpreter-like;
coherence
proof
set h=(x,u) ReassignIn I, n=|.ar x.|;
n=0 & {{}}=0-tuples_on U by FOMODEL0:10;
then reconsider f={{}} --> u as Function of n-tuples_on U,U;
reconsider ff=f as Interpreter of x,U by Def2;
h=I +* (x .--> ff); hence thesis;
end;
end;
::###############################################################
::###############################################################
::###############################################################
registration
let S be Language;
cluster (AllSymbolsOf S) -> non empty;
coherence;
end;
registration
let Y be set;
let X,Z be non empty set;
cluster -> Function-yielding for Function of X, Funcs(Y,Z);
coherence;
end;
registration
let X,Y,Z be non empty set;
cluster Function-yielding for Function of X, Funcs(Y,Z);
existence
proof take the Function of X, Funcs(Y,Z); thus thesis; end;
end;
definition
let f be Function-yielding Function, g be Function;
func ^^^ g, f __ -> Function means :Def6:
dom it=dom f & for x st x in dom f holds it.x=g*(f.x);
existence
proof
deffunc F(object)=g*(f.$1);
consider h being Function such that A1: dom h=dom f &
for x being object st x in dom f holds h.x=F(x) from FUNCT_1:sch 3;
take h; thus thesis by
A1;
end;
uniqueness
proof
let IT1,IT2 be Function;
assume A2: dom IT1=dom f & for x st x in dom f holds IT1.x=g*(f.x);
assume A3: dom IT2=dom f & for x st x in dom f holds IT2.x=g*(f.x);
now
let x be object; assume x in dom IT1;
then IT1.x=g*(f.x) & IT2.x=g*(f.x) by A2,A3; hence IT1.x=IT2.x;
end;
hence thesis by A2, A3, FUNCT_1:2;
end;
end;
registration
let f be empty Function, g be Function;
cluster ^^^ g, f __ -> empty;
coherence
proof dom ^^^ g,f __ =dom f by Def6 .= {}; hence thesis; end;
end;
definition
::$CD
end;
registration
let f be Function-yielding Function, g be empty Function;
cluster ^^^ f, g __ -> empty;
coherence;
end;
registration
let E, D be non empty set, p be D-valued FinSequence, h be Function of D,E;
cluster h*p -> (len p)-element for FinSequence;
coherence
proof
reconsider pp=p as FinSequence of D by FOMODEL0:26;
len (h*pp)=len pp by FINSEQ_2:33; hence thesis by CARD_1:def 7;
end;
end;
registration
let X,Y be non empty set;
let f be Function of X,Y; let p be X-valued FinSequence;
cluster f*p -> FinSequence-like;
coherence;
end;
registration
let E, D be non empty set, n be Nat,
p be n-element D-valued FinSequence, h be Function of D,E;
cluster h*p -> n-element for FinSequence of E;
coherence;
end;
Lm3: for U being non empty set, S being Language,
I being (S,U)-interpreter-like Function, t being termal string of S holds
(|.ar t.|)-tuples_on U = dom (I.(S-firstChar.t)) by FUNCT_2:def 1;
theorem for t0 being 0-termal string of S holds t0=<*S-firstChar.t0*>
proof
let t0 be 0-termal string of S;
reconsider e=(S-multiCat).(SubTerms(t0)) as empty set;
t0 = <*S-firstChar.t0*> ^ e by FOMODEL1:def 37 .= <*S-firstChar.t0*>;
hence thesis;
end;
Lm4: for I being (S,U)-interpreter-like Function, 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
let I be (S,U)-interpreter-like Function;
set A=AllTermsOf S,F=S-firstChar, ST=S-subTerms, SS=AllSymbolsOf S,
Z=AtomicTermsOf S, T=S-termsOfMaxDepth;
A1: dom F=SS*\{{}} by FUNCT_2:def 1;
let xx be Function of A,U;
set f=^^^xx,ST__, g=^^^ I*F, f __;
A2: dom f=dom ST by Def6 .= A by FUNCT_2:def 1;
A3: for a being set st a in A holds
(a in dom (I*F) & (a in dom g implies g.a in U))
proof
let a be set; assume A4: a in A; then
reconsider t=a as termal string of S; set n=|.ar t.|;
reconsider ss=F.t as termal Element of S;
reconsider s=ss as own Element of S;
reconsider t1=s as Element of OwnSymbolsOf S by FOMODEL1:def 19;
t1 in OwnSymbolsOf S & OwnSymbolsOf S c= dom I by Lm2;
hence A5: a in dom (I*F) by FUNCT_1:11, A1;
reconsider tt=a as Element of A by A4;
reconsider i=I.s as Interpreter of s,U;
ST.tt = SubTerms(t) by FOMODEL1:def 39;
then reconsider y=ST.tt as n-element FinSequence of A by FINSEQ_1:def 11;
reconsider z=xx*y as n-element FinSequence of U; len z=n by CARD_1:def 7;
then reconsider zz=z as Element of n-tuples_on U by FINSEQ_2:133;
(n-tuples_on U) c= dom (I.t1) by Lm3; then
A6: zz in dom i;
tt in A; then A7: tt in dom ST by FUNCT_2:def 1;
assume a in dom g; then
g.t= ((I*F).t).(f.t) by FOMODEL0:def 4 .= (I.s).(f.t) by A5, FUNCT_1:12 .=
i.zz by Def6, A7;
hence g.a in U by A6, FUNCT_1:102;
end;
then
A8: for a being object st a in A holds a in dom (I*F);
A9: dom g = dom (I*F) /\ A by A2, FOMODEL0:def 4 .= A
by A8, TARSKI:def 3, XBOOLE_1:28; then
for a being object st a in A holds g.a in U by A3;
then g is Function of A,U by FUNCT_2:3, A9;
hence g is Element of Funcs(A,U) by FUNCT_2:8;
thus thesis by A8;
end;
definition
let S; let U be non empty set, 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: it.0=(AllTermsOf S) --> u & for mm holds
it.(mm+1)=^^^ I*(S-firstChar), ^^^ it.mm qua Function, S-subTerms __ __;
existence
proof
set A=AllTermsOf S,F=S-firstChar, ST=S-subTerms, SS=AllSymbolsOf S,
Z=AtomicTermsOf S, T=S-termsOfMaxDepth, fz=A --> u;
defpred P[set,Element of Funcs(A,U),set] means $3=^^^I*F,^^^$2,ST__ __ ;
reconsider fzz=fz as Function of A, U;
reconsider fzzz=fzz as Element of Funcs(A,U) by FUNCT_2:8;
A1: for mm being Nat for x being Element of Funcs(A,U)
ex y being Element of Funcs(A,U) st P[mm,x,y]
proof
let mm be Nat;
let x be Element of Funcs(A,U); reconsider xx=x as Function of A,U;
reconsider yy=^^^I*F, ^^^xx,ST__ __ as Function of A,U by Lm4;
reconsider yyy=yy as Element of Funcs(A,U) by FUNCT_2:8;
take yyy; thus thesis;
end;
consider f being sequence of Funcs(A,U) such that A2:
(f.0=fzzz & for mm being Nat holds
P[mm,f.mm qua Element of Funcs(A,U),f.(mm+1)]) from RECDEF_1:sch 2(A1);
take f; thus thesis by A2;
end;
uniqueness
proof
set A=AllTermsOf S,F=S-firstChar, ST=S-subTerms, SS=AllSymbolsOf S,
Z=AtomicTermsOf S, T=S-termsOfMaxDepth, fz=A --> u;
reconsider fzz=fz as Element of Funcs(A,U) by FUNCT_2:8;
defpred P[set,set,set] means for f being Element of Funcs(A,U) st $2=f holds
$3=^^^I*F,^^^ f, ST __ __;
let IT1, IT2 be sequence of Funcs(A,U);
assume A3: IT1.0=fz & for mm holds IT1.(mm+1)=^^^I*F,^^^IT1.mm, ST__ __;
assume A4: IT2.0=fz & for mm holds IT2.(mm+1)=^^^I*F,^^^IT2.mm, ST__ __;
A5: IT1.0=fzz by A3;
A6: for m holds P[m,IT1.m,IT1.(m+1)]
proof
let m; reconsider mm=m as Element of NAT by ORDINAL1:def 12;
let f be Element of Funcs(A,U); assume IT1.m=f; then
IT1.mm=f; hence thesis by A3;
end;
A7: IT2.0=fzz by A4;
A8: for m holds P[m,IT2.m,IT2.(m+1)]
proof
let m; reconsider mm=m as Element of NAT by ORDINAL1:def 12;
let f be Element of Funcs(A,U); assume IT2.m=f; then IT2.mm=f;
hence thesis by A4;
end;
A9: for m being Nat, x,y1,y2 being Element of Funcs(A,U) st
P[m,x,y1] & P[m,x,y2] holds y1=y2
proof
let m; let x,y1,y2 be Element of Funcs(A,U); assume
for f being Element of Funcs(A,U) st x=f holds y1=^^^I*F,^^^ f, ST __ __;
then A10: y1=^^^I*F,^^^x,ST__ __; assume
for f being Element of Funcs(A,U) st x=f holds y2=^^^I*F,^^^ f, ST __ __;
hence y1=y2 by A10;
end;
IT1=IT2 from NAT_1:sch 14(A5,A6,A7,A8,A9); hence thesis;
end;
end;
Lm5: for u being Element of U, I being (S,U)-interpreter-like Function,
t being termal string of S, 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
let u be Element of U;
let I be (S,U)-interpreter-like Function;
let t be termal string of S; let mm;
set TE=(I,u)-TermEval, F=S-firstChar, ST=S-subTerms, A=AllTermsOf S;
A1: t in A & A c= dom (I*F) by FOMODEL1:def 32, Lm4;
reconsider tt=t as Element of A by FOMODEL1:def 32;
set G=^^^ I*F , ^^^ TE.mm, ST __ __;
A2: dom ST=A by FUNCT_2:def 1;
G is Function of A,U by Lm4; then A3: dom G=A by FUNCT_2:def 1;
A4: (TE.(mm+1)).t = G.t by Def7 .=
((I*F).t).(^^^TE.mm, ST__.t) by A3, A1, FOMODEL0:def 4
.= ((I*F).t).(TE.mm*(ST.tt)) by Def6, A2
.= ((I*F).t).(TE.mm*(SubTerms(t))) by FOMODEL1:def 39
.= (I.(F.t)).(TE.mm*(SubTerms(t))) by A1, FUNCT_1:12; hence
(TE.(mm+1)).t = (I.(F.t)).((TE.mm)*(SubTerms(t)));
assume t is 0-termal; then reconsider tt=t as 0-termal string of S;
reconsider s=F.tt as literal Element of S;
reconsider v=I.s as Interpreter of s, U;
(TE.(mm+1)).t = v.{} by A4; hence thesis;
end;
Lm6: for I being (S,U)-interpreter-like Function, u1,u2 being Element of U
holds for m being Nat holds
for t being m-termal string of S, n being Nat holds
((I,u1)-TermEval.(m+1)).t = ((I,u2)-TermEval.(m+1+n)).t
proof
let I being (S,U)-interpreter-like Function, u1,u2 being Element of U;
set F=S-firstChar, ST=S-subTerms, A=AllTermsOf S, T=S-termsOfMaxDepth;
set U1=(I,u1)-TermEval, U2=(I,u2)-TermEval, SS=AllSymbolsOf S;
defpred P[Nat] means for t being $1-termal string of S, n being Nat holds
(U1.($1+1)).t = (U2.($1+1+n)).t;
A1: P[0]
proof
let t be 0-termal string of S, n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
(U1.(0+1)).t=(I.(S-firstChar.t)).{} by Lm5 .=
(U2.(0+1+nn)).t by Lm5; hence thesis;
end;
A2: for k being Nat st P[k] holds P[k+1]
proof let k be Nat;
assume A3: P[k];
reconsider K=k+1 as Element of NAT;
let t be (k+1)-termal string of S, n be Nat;
reconsider KK=K+n as Element of NAT by ORDINAL1:def 12;
reconsider tt=t as termal string of S;
A4:
(U1.K)*(SubTerms(t))=(U2.(K+n))*(SubTerms(t))
proof
set V=SubTerms(t), l=|.ar t.|;
reconsider VV=V as l-element FinSequence of A by FINSEQ_1:def 11;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
reconsider tx = t as (kk+1)-termal string of S;
SubTerms(tx) is (T.kk)-valued Function;
then reconsider VVV=V as (T.k)-valued Function;
len VV=l by CARD_1:def 7; then A5: dom VVV=Seg l by FINSEQ_1:def 3;
reconsider U1K=U1.K , U2K=U2.KK as Function of A,U;
reconsider p=U1K*VV,q=U2K*VV as l-element FinSequence of U;
len p =l & len q=l by CARD_1:def 7; then
A6: dom p=Seg l & dom q= Seg l by FINSEQ_1:def 3;
for i being object st i in Seg l holds p.i=q.i
proof
let i be object; assume A7: i in Seg l; then
reconsider t1=VVV.i as k-termal string of S by FOMODEL1:def 33, A5,
FUNCT_1:102;
p.i = (U1.K).t1 by A7, A6, FUNCT_1:12 .=
U2K.(VVV.i) by A3 .= q.i by A7, A6, FUNCT_1:12; hence thesis;
end;
hence thesis by A6, FUNCT_1:2;
end;
(U1.(K+1)).tt =
(I.(F.tt)).((U2.KK)*(SubTerms(t))) by Lm5, A4 .= (U2.(KK+1)).tt by Lm5;
hence thesis;
end;
for mm being Nat holds P[mm] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
definition
let S, U; let I be (S,U)-interpreter-like Function;
let t be Element of (AllTermsOf S);
func I-TermEval(t) -> Element of U means :Def8:
for u1 being Element of U, mm st t in S-termsOfMaxDepth.mm holds
it=((I,u1)-TermEval.(mm+1)).t;
existence
proof
set T=S-termsOfMaxDepth, A=AllTermsOf S; consider mm such that
A1: t in T.mm by FOMODEL1:5; set u1=the Element of U;
reconsider t0=t as string of S;
reconsider t1=t0 as mm-termal string of S by A1, FOMODEL1:def 33;
reconsider mmm=mm+1 as Element of NAT;
reconsider f1=(I,u1)-TermEval.mmm as Function of A,U;
reconsider IT=f1.t as Element of U; take IT;
let u2 be Element of U, nn; assume t in T.nn; then
reconsider t2=t0 as nn-termal string of S by FOMODEL1:def 33;
IT=(((I,u2)-TermEval).(mm+1+nn)).t1 by Lm6 .=
(((I,u2)-TermEval).(nn+1+mm)).t2 .= (((I,u2)-TermEval).(nn+1)).t2
by Lm6; hence thesis;
end;
uniqueness
proof
set T=S-termsOfMaxDepth, A=AllTermsOf S;
let IT1, IT2 be Element of U;
assume A2: for u1 being Element of U, mm st t in T.mm holds
IT1=((I,u1)-TermEval.(mm+1)).t;
assume A3: for u2 being Element of U, nn st t in T.nn holds
IT2=((I,u2)-TermEval.(nn+1)).t;
consider mm such that A4: t in T.mm by FOMODEL1:5; set u=the Element of U;
IT1=((I,u)-TermEval.(mm+1)).t by A2,A4 .= IT2 by A3, A4; hence thesis;
end;
end;
definition
let S,U; let I be (S,U)-interpreter-like Function;
func I-TermEval -> Function of AllTermsOf S,U means :Def9:
for t being Element of AllTermsOf S holds it.t=I-TermEval(t);
existence
proof
set A=AllTermsOf S;
deffunc F(Element of A)=I-TermEval($1);
consider f being Function of A,U such that A1:
for t being Element of A holds f.t=F(t) from FUNCT_2:sch 4; take f;
thus thesis by A1;
end;
uniqueness
proof
set A=AllTermsOf S;
let IT1,IT2 be Function of A,U;
assume A2: for t being Element of AllTermsOf S holds IT1.t=I-TermEval(t);
assume A3: for t being Element of AllTermsOf S holds IT2.t=I-TermEval(t);
now
let t be Element of A; thus IT1.t=I-TermEval(t) by A2 .= IT2.t by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
::############### Semantics of 0wff formulas (propositions) ############
::#########################################################################
definition
let S,U; let I be (S,U)-interpreter-like Function;
func I=== -> Function equals
I +* ((TheEqSymbOf S) .--> (U-deltaInterpreter));
coherence;
end;
definition
let S,U; let I be (S,U)-interpreter-like Function; let x be set;
attr x is I-extension means :Def11: x = I===;
end;
registration
let S,U; let I be (S,U)-interpreter-like Function;
cluster I=== -> I-extension for Function;
coherence;
cluster I-extension -> Function-like for set;
coherence ;
end;
registration
let S,U; let I be (S,U)-interpreter-like Function;
cluster I-extension for Function;
existence proof take f=I===; thus thesis; end;
end;
registration
let S,U; let I be (S,U)-interpreter-like Function;
cluster I=== -> (S,U)-interpreter-like;
coherence
proof
set EQ=TheEqSymbOf S, g=EQ .--> (U-deltaInterpreter), O=OwnSymbolsOf S,
A=AtomicFormulaSymbolsOf S;
now
let s be own Element of S; s in O by FOMODEL1:def 19; then
not s in A\O by XBOOLE_0:def 5; then not s in {EQ} by FOMODEL1:9;
then not s in dom g; then
(I===).s = I.s by FUNCT_4:11; hence (I===).s is Interpreter of s,U;
end;
hence I=== is Interpreter of S,U by Def3;
thus thesis;
end;
end;
definition
let S,U; let I be (S,U)-interpreter-like Function;
let f be I-extension Function, s be ofAtomicFormula Element of S;
redefine func f.s -> Interpreter of s,U; :: redefines . (FUNCT_1, definition)
coherence
proof
set a=the adicity of S, EQ=TheEqSymbOf S, d=U-deltaInterpreter, g=EQ .--> d
, n=ar(s), A=AtomicFormulaSymbolsOf S, O=OwnSymbolsOf S;
reconsider sss=s as Element of A by FOMODEL1:def 20;
reconsider EQQ=EQ as ofAtomicFormula Element of S;
ar(EQQ)=-2 by FOMODEL1:def 23; then
A1: |.ar(EQQ).|=-(-2) by ABSVALUE:def 1 .= 2;
A2: f=I=== by Def11;
per cases;
suppose s is own; then reconsider ss=s as own Element of S;
(I===).ss is Interpreter of s,U; hence thesis by Def11;
end;
suppose not s is own;
then not sss in O; then sss in A\O by XBOOLE_0:def 5;
then sss in {EQ} by FOMODEL1:9; then
s=EQ by TARSKI:def 1; then
f.s is Function of |.n.|-tuples_on U, BOOLEAN & s is relational
by A1, A2, FUNCT_7:94; hence thesis by Def2;
end;
end;
end;
definition
let S,U; let I be (S,U)-interpreter-like Function;
let phi be 0wff string of S;
func I-AtomicEval(phi) -> set equals
((I===).(S-firstChar.phi)).((I-TermEval)*(SubTerms(phi)));
coherence;
end;
definition
let S,U; let I be (S,U)-interpreter-like Function;
let phi be 0wff string of S;
redefine func I-AtomicEval(phi) -> Element of BOOLEAN; :: redefines -AtomicEval (FOMODEL2, definition)
coherence
proof
set F=S-firstChar, i=I-TermEval, A=AllTermsOf S;
reconsider s=F.phi as relational Element of S;
set n=|.ar s.|;
reconsider f=(I===).s as Interpreter of s, U;
reconsider ff=f as Function of n-tuples_on U, BOOLEAN by Def2;
reconsider V=SubTerms(phi) as n-element FinSequence of A by FINSEQ_1:def 11;
reconsider iV=i*V as n-element FinSequence of U; len iV=n by CARD_1:def 7;
then reconsider iVV=iV as Element of n-tuples_on U by FINSEQ_2:133;
ff.iVV is Element of BOOLEAN; hence thesis;
end;
end;
::###### Semantics of formulas (evaluation of any wff string) ##########
::######################################################################
registration
let S,U; let I be (S,U)-interpreter-like Function;
cluster I|(OwnSymbolsOf S) -> PFuncs(U*, U\/BOOLEAN)-valued for Function;
coherence
proof
set O=OwnSymbolsOf S, f=I|O, D=dom f, C=U\/BOOLEAN;
now
let y be object; assume y in rng f; then y in f.:D;then
consider x being object such that A1:
x in D & x in D & y=f.x by FUNCT_1:def 6;
x in O by A1; then reconsider s=x as own Element of S by FOMODEL1:def 19;
reconsider n=|.ar s.| as Element of NAT;
reconsider DD=n-tuples_on U as Subset of U* by FINSEQ_2:134; C c= C;
then reconsider CC=C as Subset of C; f.x=I.s by FUNCT_1:49, A1;
then reconsider g=f.x as Function of DD,CC; [:DD,CC:] c= [:U*,C:];
then reconsider gg=g as Relation of U*,C by XBOOLE_1:1;
gg is PartFunc of U*,C; hence y in PFuncs(U*,C) by PARTFUN1:45, A1;
end;
hence thesis by RELAT_1:def 19, TARSKI:def 3;
end;
cluster I|(OwnSymbolsOf S) -> (S,U)-interpreter-like for Function;
coherence
proof
set O=OwnSymbolsOf S, f=I|O, D=dom f, C=U\/BOOLEAN;
now
let s be own Element of S;
f.s=I.s by FOMODEL1:def 19, FUNCT_1:49; hence f.s is Interpreter of s,U;
end;
then f is Interpreter of S,U by Def3;
hence thesis;
end;
end;
registration
let S,U; let I be (S,U)-interpreter-like Function;
cluster I|(OwnSymbolsOf S) -> total for (OwnSymbolsOf S)-defined Relation;
coherence
proof
set O=OwnSymbolsOf S, f=I|O, D=dom f, C=U\/BOOLEAN;
O c= dom f & dom f c= O by Lm2;
hence thesis by PARTFUN1:def 2, XBOOLE_0:def 10;
end;
end;
definition
let S,U;
func U-InterpretersOf S -> set equals
{f where f is Element of Funcs(OwnSymbolsOf S, PFuncs(U*,U\/BOOLEAN)):
f is (S,U)-interpreter-like};
coherence;
end;
definition
let S,U;
redefine func U-InterpretersOf S -> Subset of :: redefines -InterpretersOf (FOMODEL2, definition)
Funcs(OwnSymbolsOf S, PFuncs(U*,U\/BOOLEAN));
coherence
proof
set I=U-InterpretersOf S, O=OwnSymbolsOf S, C= PFuncs(U*,U\/BOOLEAN);
defpred P[Element of Funcs(O,C)] means $1 is (S,U)-interpreter-like;
{f where f is Element of Funcs(O,C): P[f]}
is Subset of Funcs(O,C) from DOMAIN_1:sch 7; hence thesis;
end;
end;
registration
let S,U;
cluster U-InterpretersOf S -> non empty for set;
coherence
proof
set I = the (S,U)-interpreter-like Function;
set O=OwnSymbolsOf S, f=I|O, C=PFuncs(U*, U\/BOOLEAN);
dom f c= O & rng f c= C; then
reconsider ff=f as Relation of O,C by RELSET_1:4;
reconsider fff=ff as Element of Funcs(O,C) by FUNCT_2:8;
ex g being Element of Funcs(O,C) st f=g & g is (S,U)-interpreter-like
proof take fff; thus thesis; end;
then f in U-InterpretersOf S; hence thesis;
end;
end;
registration
let S,U;
cluster -> (S,U)-interpreter-like for Element of U-InterpretersOf S;
coherence
proof
set SUI=U-InterpretersOf S,O=OwnSymbolsOf S, C=PFuncs(U*,U\/BOOLEAN);
let x be Element of SUI; x in SUI;then consider f being Element of
Funcs(O,C) such that A1: x=f & f is (S,U)-interpreter-like;
thus thesis by A1;
end;
end;
definition
let S,U;
func S-TruthEval(U) ->
Function of [: U-InterpretersOf S, AtomicFormulasOf S :],BOOLEAN
means :Def14: for I being Element of U-InterpretersOf S,
phi being Element of AtomicFormulasOf S holds it.(I,phi)=I-AtomicEval(phi);
existence
proof
set II=U-InterpretersOf S, AF=AtomicFormulasOf S;
deffunc F(Element of II, Element of AF)=$1-AtomicEval($2)
qua Element of BOOLEAN;
consider f being Function of [:II,AF:], BOOLEAN such that
A1: for I being Element of II, phi being Element of AF holds
f.(I,phi)=F(I,phi) from BINOP_1:sch 4; take f; thus
for I being Element of II, phi being Element of AF holds
f.(I,phi)=I-AtomicEval(phi)
by A1;
end;
uniqueness
proof
set II=U-InterpretersOf S, AF=AtomicFormulasOf S, B=BOOLEAN;
let IT1,IT2 be Function of [:II,AF:],B;
deffunc F(Element of II, Element of AF)=$1-AtomicEval($2);
assume that A2: for I being Element of II, phi being Element of AF holds
IT1.(I,phi)=F(I,phi) and A3: for I being Element of II,
phi being Element of AF holds IT2.(I,phi)=F(I,phi);
now
let a be Element of II, b be Element of AF;
thus IT1.(a,b)= F(a,b) by A2 .= IT2.(a,b) by A3;
end;
hence IT1=IT2;
end;
end;
definition
let S,U; 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: TRUE if
ex u being Element of U, v being literal Element of S st
(phi.1=v & f.((v,u) ReassignIn I, phi/^1)=TRUE) otherwise FALSE;
coherence; consistency;
end;
definition
let S,U;
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: (for x being Element of U-InterpretersOf S,
y being Element of (AllSymbolsOf S)*\{{}} holds
([x,y] in dom it iff (
ex v being literal Element of S, w being string of S st
[x,w] in dom g & y=<*v*>^w
))) &
(for x being Element of U-InterpretersOf S,
y being Element of (AllSymbolsOf S)*\{{}} st [x,y] in dom it holds
it.(x,y)=g-ExFunctor(x,y));
existence
proof
set SS=AllSymbolsOf S, II=U-InterpretersOf S, Strings=SS*\{{}};
deffunc F(Element of II, Element of Strings)=g-ExFunctor($1,$2);
defpred P[Element of II, Element of Strings] means
ex v being literal Element of S, w being string of S st
[$1,w] in dom g & $2=<*v*>^w;
A1: for x being Element of II, y being Element of Strings st P[x,y] holds
F(x,y) in BOOLEAN;
consider f being PartFunc of [:II, Strings:],BOOLEAN such that A2:
(for x being Element of II, y being Element of Strings holds
([x,y] in dom f iff P[x,y])) &
(for x being Element of II, y being Element of Strings st [x,y] in dom f
holds f.(x,y)=F(x,y)) from BINOP_1:sch 8(A1); take f; thus thesis by A2;
end;
uniqueness
proof
set SS=AllSymbolsOf S,II=U-InterpretersOf S,Strings=SS*\{{}},D=[:II,Strings:];
let IT1, IT2 be PartFunc of D, BOOLEAN;
defpred P[Element of II, Element of Strings] means
ex v being literal Element of S, w being string of S st
[$1,w] in dom g & $2=<*v*>^w;
assume that A3: (for x being Element of II, y being Element of Strings holds
([x,y] in dom IT1 iff P[x,y])) and
A4: (for x being Element of II, y being Element of Strings
st [x,y] in dom IT1 holds IT1.(x,y)=g-ExFunctor(x,y));
assume that A5: (for x being Element of II, y being Element of Strings holds
([x,y] in dom IT2 iff P[x,y])) and
A6: (for x being Element of II, y being Element of Strings
st [x,y] in dom IT2 holds IT2.(x,y)=g-ExFunctor(x,y));
A7: now
let x be object;
assume A8: x in dom IT1; then reconsider xx=x as Element of D;
consider x1,x2 being object such that
A9: x1 in II & x2 in Strings & xx=[x1,x2] by ZFMISC_1:def 2;
reconsider I=x1 as Element of II by A9;
reconsider phi=x2 as Element of Strings by A9;
P[I,phi] by A3,A8,A9;
hence x in dom IT2 by A5, A9;
end;
then
A10: dom IT1 c= dom IT2;
now
let x be object; assume A11: x in dom IT2;
then reconsider xx=x as Element of D;
consider x1,x2 being object such that
A12: x1 in II & x2 in Strings & xx=[x1,x2] by ZFMISC_1:def 2;
reconsider I=x1 as Element of II by A12;
reconsider phi=x2 as Element of Strings by A12;
P[I,phi] by A5,A11,A12;
hence x in dom IT1 by A3, A12;
end; then
A13: dom IT2 c= dom IT1;
now
let x be object; assume A14: x in dom IT1;
then reconsider xx=x as Element of D;
consider x1,x2 being object such that
A15: x1 in II & x2 in Strings & xx=[x1,x2] by ZFMISC_1:def 2;
reconsider I=x1 as Element of II by A15;
reconsider phi=x2 as Element of Strings by A15;
IT1.x = IT1.(I,phi) by A15 .=
g-ExFunctor(I,phi) by A4, A15, A14 .= IT2.(I,phi)
by A6, A15, A14, A7 .= IT2.x by A15;
hence IT1.x = IT2.x;
end;
hence thesis by FUNCT_1:2, A13, A10, XBOOLE_0:def 10;
end;
end;
definition
let S,U;
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:
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; consistency;
end;
::# The inelegant specification [I,w1] in dom f above is needed because
::# of a general problem with the . functor Despite the ideal policy of
::# separating the definition of well-formedness and truth value respectively
::# in NorIterator and -NorFunctor, one is obliged to repeat the specification
::# because the . functor adopts {} as return value for indefinite arguments
::# (see FUNCT_1:def 2) Sadly, {} is also the set conventionally chosen to
::# represent FALSE (and many other things), so we cannot resolve ambiguity
::# between a meaningless argument and a false argument, and are forced to
::# add the statement about the argument effectively belonging to the domain.
::# An alternative could have been to recode truth values in e.g. 1=true,
::# 2=false, but that could have been too much of a breakthrough. Thus in
::# general, when one has to choose an arbitrary convention to represent
::# things, I feel it would be better to avoid functions with 0={} in their
::# ranges; sadly this does not happen in many cases (see eg the chi functor),
::# probably because of the load of intuitive, symbolic, representative
::# imagery that 0 and emptiness symbols convey.
definition
let S,U;
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:
(for x being Element of U-InterpretersOf S,
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,
y being Element of (AllSymbolsOf S)*\{{}} st [x,y] in dom it holds
it.(x,y)=g-NorFunctor(x,y));
existence
proof
set SS=AllSymbolsOf S, II=U-InterpretersOf S, Strings=SS*\{{}};
reconsider g as PartFunc of [: II, Strings :], BOOLEAN;
deffunc F(Element of II, Element of Strings)=g-NorFunctor($1,$2);
defpred P[Element of II, Element of Strings] means
ex phi1, phi2 being Element of (AllSymbolsOf S)*\{{}} st
($2=<*TheNorSymbOf S*>^phi1^phi2 &
[$1,phi1] in dom g & [$1,phi2] in dom g);
A1: for x being Element of II, y being Element of Strings st P[x,y] holds
F(x,y) in BOOLEAN;
consider f being PartFunc of [:II, Strings:],BOOLEAN such that
A2: (for x being Element of II, y being Element of Strings holds
([x,y] in dom f iff P[x,y])) &
(for x being Element of II, y being Element of Strings st [x,y] in dom f
holds f.(x,y)=F(x,y)) from BINOP_1:sch 8(A1); take f; thus thesis by A2;
end;
uniqueness
proof
set SS=AllSymbolsOf S,II=U-InterpretersOf S,Strings=SS*\{{}},D=[:II,Strings:];
deffunc F(Element of II, Element of Strings)=g-NorFunctor($1,$2);
defpred P[Element of II, Element of Strings] means
ex phi1, phi2 being Element of (AllSymbolsOf S)*\{{}} st
($2=<*TheNorSymbOf S*>^phi1^phi2 & [$1,phi1] in dom g & [$1,phi2] in dom g);
let IT1, IT2 be PartFunc of D, BOOLEAN;
assume that A3: (for x being Element of II, y being Element of Strings holds
([x,y] in dom IT1 iff P[x,y])) and
A4: (for x being Element of II, y being Element of Strings
st [x,y] in dom IT1 holds IT1.(x,y)=F(x,y));
assume that A5: (for x being Element of II, y being Element of Strings holds
([x,y] in dom IT2 iff P[x,y])) and
A6: (for x being Element of II, y being Element of Strings
st [x,y] in dom IT2 holds IT2.(x,y)=F(x,y));
A7: now
let x be object;
assume A8: x in dom IT1; then reconsider xx=x as Element of D;
consider x1,x2 being object such that
A9: x1 in II & x2 in Strings & xx=[x1,x2] by ZFMISC_1:def 2;
reconsider I=x1 as Element of II by A9;
reconsider phi=x2 as Element of Strings by A9;
P[I,phi] by A3,A8,A9;
hence x in dom IT2 by A5, A9;
end;
then
A10: dom IT1 c= dom IT2;
now
let x be object;
assume A11: x in dom IT2; then reconsider xx=x as Element of D;
consider x1,x2 being object such that
A12: x1 in II & x2 in Strings & xx=[x1,x2] by ZFMISC_1:def 2;
reconsider I=x1 as Element of II by A12;
reconsider phi=x2 as Element of Strings by A12;
P[I,phi] by A5,A11,A12;
hence x in dom IT1 by A3, A12;
end; then
A13: dom IT2 c= dom IT1;
now
let x be object; assume A14: x in dom IT1;
then reconsider xx=x as Element of D;
consider x1,x2 being object such that
A15: x1 in II & x2 in Strings & xx=[x1,x2] by ZFMISC_1:def 2;
reconsider I=x1 as Element of II by A15;
reconsider phi=x2 as Element of Strings by A15;
IT1.x = IT1.(I,phi) by A15 .=
F(I,phi) by A4, A15, A14 .= IT2.(I,phi)
by A6, A15, A14, A7 .= IT2.x by A15; hence IT1.x = IT2.x;
end;
hence thesis by FUNCT_1:2, A10, XBOOLE_0:def 10, A13;
end;
end;
definition
let S,U;
func (S,U)-TruthEval -> sequence of
PFuncs([:U-InterpretersOf S, (AllSymbolsOf S)*\{{}}:], BOOLEAN) means
:Def19: it.0=S-TruthEval(U) & for mm holds
it.(mm+1)=ExIterator(it.mm) +* NorIterator(it.mm) +* it.mm;
existence
proof
set SS=AllSymbolsOf S, II=U-InterpretersOf S, AF=AtomicFormulasOf S,
Strings=SS*\{{}}, D=[:II, Strings:];
reconsider ii=II as Subset of II by XBOOLE_0:def 10;
reconsider subboolean=BOOLEAN as Subset of BOOLEAN by XBOOLE_0:def 10;
reconsider sub=[: ii, AF :] as Subset of D;
[: sub, subboolean :] c= [: D, BOOLEAN :];
then S-TruthEval(U) is PartFunc of D, BOOLEAN by XBOOLE_1:1; then
reconsider Z=S-TruthEval(U) as Element of PFuncs(D, BOOLEAN) by PARTFUN1:45;
deffunc F(Element of PFuncs(D, BOOLEAN))=ExIterator($1) +*
NorIterator($1) +* $1;
defpred P[set,Element of PFuncs(D,BOOLEAN),set] means $3=F($2);
A1: for n being Nat for x being Element of PFuncs(D, BOOLEAN)
ex y being Element of PFuncs(D, BOOLEAN) st P[n,x,y]
proof
let n be Nat, x be Element of PFuncs(D,BOOLEAN);
reconsider yy=F(x) as Element of PFuncs(D,BOOLEAN) by PARTFUN1:45;
take y=yy; thus thesis;
end;
consider f being sequence of PFuncs(D, BOOLEAN) such that A2: f.0=Z &
for n being Nat holds P[n,
f.n qua Element of PFuncs(D, BOOLEAN)
,f.(n+1)] from RECDEF_1:sch 2(A1); take f;
thus f.0=S-TruthEval(U) by A2; thus
for mm holds f.(mm+1)=ExIterator(f.mm) +* NorIterator(f.mm) +* f.mm
by A2;
end;
uniqueness
proof
set SS=AllSymbolsOf S, II=U-InterpretersOf S, AF=AtomicFormulasOf S,
Strings=SS*\{{}}, D=[:II, Strings:], Z=S-TruthEval(U);
[:II, AF:] c= D & BOOLEAN c= BOOLEAN by ZFMISC_1:96;
then dom Z c= D & rng Z c= BOOLEAN;
then Z is Relation of D, BOOLEAN by RELSET_1:4;
then reconsider ZZ=Z as Element of PFuncs(D, BOOLEAN) by PARTFUN1:45;
deffunc RecFun(set,Element of PFuncs(D,BOOLEAN))=
ExIterator($2) +* NorIterator($2) +* $2;
defpred P[set,set,set] means
for f being Element of PFuncs(D,BOOLEAN) st $2=f holds $3=RecFun($1,f);
let IT1, IT2 be sequence of PFuncs(D, BOOLEAN);
assume A3: IT1.0=Z & for mm holds
IT1.(mm+1)=ExIterator(IT1.mm) +* NorIterator(IT1.mm) +* IT1.mm;
assume A4: IT2.0=Z & for mm holds
IT2.(mm+1)=ExIterator(IT2.mm) +* NorIterator(IT2.mm) +* IT2.mm;
A5: IT1.0=ZZ by A3;
A6: for m holds P[m,IT1.m, IT1.(m+1)]
proof
let m; reconsider mm=m as Element of NAT by ORDINAL1:def 12;
let f being Element of PFuncs(D,BOOLEAN); assume f=IT1.m; then
IT1.(mm+1)=RecFun(m,f) by A3; hence thesis;
end;
A7: IT2.0=ZZ by A4;
A8: for m holds P[m,IT2.m, IT2.(m+1)]
proof
let m; reconsider mm=m as Element of NAT by ORDINAL1:def 12;
let f be Element of PFuncs(D,BOOLEAN); assume f=IT2.m; then
IT2.(mm+1) = RecFun(m,f) by A4; hence thesis;
end;
A9: for n being Nat,x,y1,y2 being Element of PFuncs(D,BOOLEAN) st
P[n,x,y1] & P[n,x,y2] holds y1=y2
proof
let n be Nat, x,y1,y2 be Element of PFuncs(D,BOOLEAN);
assume that A10: P[n,x,y1] and A11: P[n,x,y2];
A12: y2=RecFun(n,x) by A11;
thus thesis by A10, A12;
end;
thus thesis from NAT_1:sch 14(A5,A6,A7,A8,A9);
end;
end;
theorem Th2: for I being (S,U)-interpreter-like Function holds
I|(OwnSymbolsOf S) in U-InterpretersOf S
proof
let I be (S,U)-interpreter-like Function;
set O=OwnSymbolsOf S, C=PFuncs(U*,U\/BOOLEAN);
dom (I|O) c= O & rng (I|O) c= C;
then I|O is Function of O,C by RELSET_1:4; then
I|O is (S,U)-interpreter-like & I|O is Element of Funcs(O,C)
by FUNCT_2:8; hence thesis;
end;
definition
let S be Language, m be Nat, U be non empty set;
func (S,U)-TruthEval m -> Element of
PFuncs([:U-InterpretersOf S, (AllSymbolsOf S)*\{{}}:], BOOLEAN)
means :Def20: for mm st m=mm holds it=(S,U)-TruthEval.mm;
existence
proof
set f=(S,U)-TruthEval;
reconsider nn=m as Element of NAT by ORDINAL1:def 12;
take f.nn; let mm; assume m=mm; hence f.nn=f.mm;
end;
uniqueness
proof
set II=U-InterpretersOf S, SS=AllSymbolsOf S,f=(S,U)-TruthEval;
let IT1,IT2 be Element of PFuncs([:II,SS*\{{}}:],BOOLEAN);
assume that A1:
for mm st m=mm holds IT1=(S,U)-TruthEval.mm and A2:
for mm st m=mm holds IT2=(S,U)-TruthEval.mm;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
thus IT1=f.mm by A1 .= IT2 by A2;
end;
end;
Lm7: for n holds
x in dom (S,U)-TruthEval m implies
(x in dom (S,U)-TruthEval (m+n) &
((S,U)-TruthEval m).x = ((S,U)-TruthEval (m+n)).x)
proof
set f=(S,U)-TruthEval;
defpred P[Nat] means x in dom (S,U)-TruthEval m implies
(x in dom (S,U)-TruthEval (m+$1) &
((S,U)-TruthEval m).x = ((S,U)-TruthEval (m+$1)).x);
A1: P[0];
A2: for n st P[n] holds P[n+1]
proof
let n;
reconsider k=m+n, K=(m+n)+1 as Element of NAT by ORDINAL1:def 12;
assume A3: P[n];
set g=(S,U)-TruthEval m, g0=(S,U)-TruthEval (m+n),
g1=(S,U)-TruthEval ((m+n)+1);
A4: f.k=g0 & f.K=g1 by Def20;
A5: f.K=ExIterator(f.k) +* NorIterator(f.k) +* f.k by Def19; then
dom (f.K)=dom (ExIterator(f.k) +* NorIterator(f.k)) \/ dom (f.k)
by FUNCT_4:def 1; then
A6: dom (f.k) c= dom (f.K) by XBOOLE_1:7; assume
A7: x in dom g; then x in dom (f.k) by A3, Def20; then
A8: x in dom (f.K) by A6;
thus x in dom (S,U)-TruthEval (m+(n+1)) by A4, A7, A3, A6;
x in dom (ExIterator(f.k) +* NorIterator(f.k)) \/ dom (f.k)
by FUNCT_4:def 1, A8, A5;
hence thesis by A3, A4, A7, A5, FUNCT_4:def 1;
end;
thus for n holds P[n] from NAT_1:sch 2(A1,A2);
end;
Lm8: x in X\/Y\/Z iff x in X or x in Y or x in Z
proof
set W=X\/Y\/Z; x in W iff (x in X\/Y) or x in Z
by XBOOLE_0:def 3; hence thesis by XBOOLE_0:def 3;
end;
Lm9:
for m holds
for I1 be Element of U1-InterpretersOf S,
I2 be Element of U2-InterpretersOf S, w being string of S holds
([I1,w] in dom (S,U1)-TruthEval m implies [I2,w] in dom (S,U2)-TruthEval m)
proof
set SS=AllSymbolsOf S, N=TheNorSymbOf S, II1=U1-InterpretersOf S,
II2=U2-InterpretersOf S, AF=AtomicFormulasOf S;
defpred P[Nat] means for I1 be Element of II1, I2 being Element of II2,
w be string of S holds ([I1,w] in dom ((S,U1)-TruthEval $1) implies
[I2,w] in dom ((S,U2)-TruthEval $1));
A1: P[0]
proof
set f1=(S,U1)-TruthEval 0, f2=(S,U2)-TruthEval 0;
reconsider Z=0 as Element of NAT; reconsider g1=((S,U1)-TruthEval).Z as
Element of PFuncs ([:II1,SS*\{{}}:], BOOLEAN); reconsider
g2=((S,U2)-TruthEval).Z as Element of PFuncs ([:II2,SS*\{{}}:], BOOLEAN);
A2: f1=g1 & f2=g2 by Def20;
A3: g1=S-TruthEval(U1) & g2=S-TruthEval(U2) by Def19;
A4: dom f1 = [:II1,AF:] by A2, FUNCT_2:def 1,A3;
A5: dom f2 = [:II2,AF:] by A2, FUNCT_2:def 1,A3;
let I1 be Element of II1, I2 be Element of II2; let w;
assume [I1,w] in dom f1; then I1 in II1 & w in AF by ZFMISC_1:87,A4;
hence [I2,w] in dom f2 by A5, ZFMISC_1:87;
end;
A6: for n st P[n] holds P[n+1]
proof
let n; reconsider nn=n,NN=n+1 as Element of NAT by ORDINAL1:def 12;
assume A7: P[n];
let I1 be Element of II1, I2 be Element of II2;
set f1n=(S,U1)-TruthEval n, f1N=(S,U1)-TruthEval (n+1)
,f2n=(S,U2)-TruthEval n, f2N=(S,U2)-TruthEval (n+1);
A8: dom f1N=dom ExIterator(f1n) \/ dom NorIterator(f1n) \/ dom f1n
proof
reconsider g1N=((S,U1)-TruthEval).NN as Element of PFuncs
([:II1,SS*\{{}}:], BOOLEAN); reconsider
g1n=((S,U1)-TruthEval).nn as Element of PFuncs ([:II1,SS*\{{}}:], BOOLEAN);
A9: f1n=g1n & f1N = g1N by Def20; then
f1N=ExIterator(g1n) +* NorIterator(g1n) +* g1n by Def19; then
dom f1N=dom (ExIterator(g1n) +* NorIterator(g1n)) \/ dom g1n
by FUNCT_4:def 1 .= dom ExIterator(g1n) \/ dom NorIterator(g1n)
\/ dom g1n by FUNCT_4:def 1; hence thesis by A9;
end;
A10: dom f2N=dom ExIterator(f2n) \/ dom NorIterator(f2n) \/ dom f2n
proof
reconsider g2N=((S,U2)-TruthEval).NN as Element of PFuncs
([:II2,SS*\{{}}:], BOOLEAN); reconsider
g2n=((S,U2)-TruthEval).nn as Element of PFuncs ([:II2,SS*\{{}}:], BOOLEAN);
A11: f2n=g2n & f2N = g2N by Def20; then
f2N=ExIterator(g2n) +* NorIterator(g2n) +* g2n by Def19; then
dom f2N=dom (ExIterator(g2n) +* NorIterator(g2n)) \/ dom g2n
by FUNCT_4:def 1 .= dom ExIterator(g2n) \/ dom NorIterator(g2n)
\/ dom g2n by FUNCT_4:def 1; hence thesis by A11;
end;
let w; set x=[I1,w]; assume
A12: x in dom f1N;
per cases by A12, Lm8, A8;
suppose x in dom ExIterator(f1n);
then
consider v being literal Element of S, ww being string of S such that A13:
[I1,ww] in dom f1n & w=<*v*>^ww by Def16;
[I2,ww] in dom f2n & w=<*v*>^ww by A13,A7;
then [I2,w] in dom ExIterator(f2n) by Def16; hence
[I2,w] in dom f2N by Lm8, A10;
end;
suppose x in dom NorIterator(f1n); then
consider phi1, phi2 being string of S such that A14:
(w=<*TheNorSymbOf S*>^phi1^phi2 & [I1,phi1] in dom f1n
& [I1,phi2] in dom f1n) by Def18;
w=<*N*>^phi1^phi2 & [I2,phi1] in dom f2n & [I2,phi2] in dom f2n by A14,A7;
then [I2,w] in dom NorIterator(f2n) by Def18; hence thesis by Lm8,A10;
end;
suppose
x in dom f1n; then [I2,w] in dom f2n by A7; hence thesis by Lm8,A10;
end;
end;
thus for m holds P[m] from NAT_1:sch 2(A1,A6);
end;
Lm10: curry ((S,U)-TruthEval.mm) is Function
of U-InterpretersOf S,PFuncs((AllSymbolsOf S)*\{{}},BOOLEAN)
proof
set II=U-InterpretersOf S, AF=AtomicFormulasOf S, f=(S,U)-TruthEval.mm
, SS=AllSymbolsOf S, F=(S,U)-TruthEval;
reconsider g = curry f as Element of PFuncs(II,PFuncs(SS*\{{}},BOOLEAN))
by FUNCT_6:14; set y = the Element of AF;
reconsider Z=0 as Element of NAT;
dom (S-TruthEval U)=[:II,AF:] by FUNCT_2:def 1; then
A1: dom (F.0)=[:II,AF:] by Def19;
now
let x be object; assume x in II; then [x,y] in dom (F.0) by A1, ZFMISC_1:87;
then [x,y] in dom (S,U)-TruthEval 0 by Def20; then
[x,y] in dom (S,U)-TruthEval (0+mm) by Lm7; then
[x,y] in dom f by Def20; hence x in dom g by FUNCT_5:19;
end;
then II c= dom g & dom g c= II; then
reconsider gg=g as total PartFunc of II,PFuncs(SS*\{{}},BOOLEAN)
by XBOOLE_0:def 10, PARTFUN1:def 2; curry f=gg ; hence thesis;
end;
Lm11: curry ((S,U)-TruthEval m) is Function of
U-InterpretersOf S, PFuncs((AllSymbolsOf S)*\{{}},BOOLEAN)
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set f=(S,U)-TruthEval mm, g=(S,U)-TruthEval.mm;
curry f=curry g by Def20; hence thesis by Lm10;
end;
definition
let S,U,m; let I be Element of U-InterpretersOf S;
func (I,m)-TruthEval -> Element of PFuncs((AllSymbolsOf S)*\{{}},BOOLEAN)
equals (curry ((S,U)-TruthEval m)).I;
coherence
proof
set II=U-InterpretersOf S, SS=AllSymbolsOf S;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
curry ((S,U)-TruthEval mm)= curry ((S,U)-TruthEval.mm) by Def20; then
reconsider f=curry ((S,U)-TruthEval mm) as Function of II, PFuncs(SS*\{{}}
,BOOLEAN) by Lm10;
f.I is Element of PFuncs(SS*\{{}},BOOLEAN); hence thesis;
end;
end;
Lm12: for I being Element of U-InterpretersOf S holds
(I,m)-TruthEval c= (I,m+n)-TruthEval
proof
set UI=U-InterpretersOf S,SS=AllSymbolsOf S;
let I be Element of UI;
set IT1=(I,m)-TruthEval, IT2=(I,m+n)-TruthEval, f=(S,U)-TruthEval m,
g=(S,U)-TruthEval (m+n);
reconsider F=curry f,G=curry g as Function of UI, PFuncs(SS*\{{}},BOOLEAN)
by Lm11;
A1: IT1=F.I & IT2=G.I & dom F=UI by FUNCT_2:def 1;
A2: for x st x in dom IT1 holds (x in dom IT2 & IT1.x=IT2.x)
proof
let x; assume
A3: x in dom IT1; then
A4: [I,x] in dom f by A1, FUNCT_5:31; then
A5: [I,x] in dom g & g.[I,x]=f.[I,x] by Lm7; then
x in dom IT2 & IT2.x=g.(I,x) by FUNCT_5:20; then
IT2.x = f.(I,x) by A4, Lm7 .= IT1.x by A3, FUNCT_5:31, A1;
hence x in dom IT2 & IT1.x=IT2.x by A5, FUNCT_5:20;
end;
(for x being object st x in dom IT1 holds x in dom IT2) &
for x being object st x in dom IT1 holds IT1.x=IT2.x by A2;
hence thesis by GRFUNC_1:2, TARSKI:def 3;
end;
Lm13: for I1 being Element of U1-InterpretersOf S,
I2 being Element of U2-InterpretersOf S holds
dom (I1,m)-TruthEval c= dom (I2,m)-TruthEval
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set II1=U1-InterpretersOf S, II2=U2-InterpretersOf S,
f=(S,U1)-TruthEval.mm, SS=AllSymbolsOf S,
ff1=(S,U1)-TruthEval mm, ff2=(S,U2)-TruthEval mm, g=(S,U2)-TruthEval.mm;
let I1 be Element of II1, I2 be Element of II2;
A1: f=ff1 & g=ff2 by Def20;
set F1=(I1,m)-TruthEval, F2=(I2,m)-TruthEval;
A2: (curry f).I1=F1 & (curry g).I2=F2 by Def20; then
reconsider f1=(curry((S,U1)-TruthEval.mm)).I1,
f2=(curry((S,U2)-TruthEval.mm)).I2 as Element of PFuncs(SS*\{{}},BOOLEAN);
reconsider F=curry f as Function of II1,PFuncs(SS*\{{}},BOOLEAN) by Lm10;
A3: I1 in II1; f is Element of PFuncs ([:II1,SS*\{{}}:], BOOLEAN); then
dom f c= [: II1, SS*\{{}} :] by RELAT_1:def 18; then
A4: uncurry F=f by FUNCT_5:50;
now
let ww be object; assume A5: ww in dom f1; then
reconsider w=ww as Element of SS*\{{}};
I1 in dom F & f1=F.I1 & ww in dom f1 by A3, FUNCT_2:def 1, A5;
then [I1,w] in dom ff1 by A1, A4, FUNCT_5:38;
then [I2,ww] in dom g by A1, Lm9; hence ww in dom f2 by FUNCT_5:20;
end;
hence thesis by A2;
end;
Lm14: for I1 being Element of U1-InterpretersOf S,
I2 being Element of U2-InterpretersOf S holds
dom (I1,mm)-TruthEval = dom (I2,mm)-TruthEval by Lm13;
definition
let S; let m be natural Number;
func S-formulasOfMaxDepth m -> Subset of ((AllSymbolsOf S)*\{{}}) means
:Def22:
for U being non empty set, I being Element of U-InterpretersOf S,
mm being Element of NAT st m=mm holds it=dom (I,mm)-TruthEval;
existence
proof
set SS=AllSymbolsOf S;
set UU =the non empty set, II = the Element of UU-InterpretersOf S;
reconsider nn=m as Element of NAT by ORDINAL1:def 12;
reconsider IT=dom ((II,nn)-TruthEval) as Subset of SS*\{{}};
take IT;
let U; set III=U-InterpretersOf S; let I be Element of III; let mm;
assume m=mm;
hence IT=dom(I,mm)-TruthEval by Lm14;
end;
uniqueness
proof
set SS=AllSymbolsOf S;
let IT1,IT2 be Subset of (SS*\{{}}); assume that
A1:for U being non empty set, I being Element of U-InterpretersOf S,
mm being Element of NAT st m=mm holds IT1=dom (I,mm)-TruthEval and
A2: for U being non empty set, I being Element of U-InterpretersOf S,
mm being Element of NAT st m=mm holds IT2=dom (I,mm)-TruthEval;
set U = the non empty set, I = the Element of U-InterpretersOf S;
reconsider nn=m as Element of NAT by ORDINAL1:def 12;
thus IT1=dom (I,nn)-TruthEval by A1 .= IT2 by A2;
end;
end;
Lm15: S-formulasOfMaxDepth m c= S-formulasOfMaxDepth (m+n)
proof
set U = the non empty set;
set X=S-formulasOfMaxDepth m, Y=S-formulasOfMaxDepth (m+n),
II=U-InterpretersOf S; set I = the Element of II;
reconsider mm=m, NN=m+n as Element of NAT by ORDINAL1:def 12;
set f=(I,mm)-TruthEval, g=(I,NN)-TruthEval;
A1: X=dom f & Y=dom g by Def22;
f c= g by Lm12; hence thesis by GRFUNC_1:2, A1;
end;
Lm16: S-formulasOfMaxDepth 0 = AtomicFormulasOf S
proof
set U = the non empty set, AF=AtomicFormulasOf S, II=U-InterpretersOf S,
I = the Element of II; reconsider z=0 as Element of NAT;
A1: [:II,AF:] = dom (S-TruthEval(U)) by FUNCT_2:def 1 .=
dom ((S,U)-TruthEval.z) by Def19 .=
dom ((S,U)-TruthEval 0) by Def20;
now
let x be object; assume x in AF; then
[I,x] in dom ((S,U)-TruthEval 0) by A1, ZFMISC_1:def 2;
then x in dom (I,z)-TruthEval by FUNCT_5:20;
hence x in S-formulasOfMaxDepth 0 by Def22;
end; then
A2: AF c= S-formulasOfMaxDepth 0;
now
let x be object; assume x in S-formulasOfMaxDepth 0;
then A3: x in dom (I,z)-TruthEval by Def22;
set f=(S,U)-TruthEval z, g=(I,z)-TruthEval;
f=(S,U)-TruthEval.z by Def20; then reconsider gg=curry f as
Function of II, PFuncs((AllSymbolsOf S)*\{{}},BOOLEAN) by Lm10;
dom gg=II by FUNCT_2:def 1; then
[I,x] in [:II, AF:] by A1, A3, FUNCT_5:31;
then ([I,x])`2 in AF by MCART_1:10; hence x in AF;
end;
then S-formulasOfMaxDepth 0 c= AF;
hence thesis by A2;
end;
definition
let S; let m be natural Number; let w;
attr w is m-wff means :Def23: w in S-formulasOfMaxDepth m;
end;
definition
let S,w;
attr w is wff means :Def24: ex m st w is m-wff;
end;
registration
let S;
cluster 0-wff -> 0wff for string of S;
coherence
proof
set AF=AtomicFormulasOf S, Z=S-formulasOfMaxDepth 0;
let w be string of S; assume w is 0-wff; then w in Z; then
w in AF by Lm16; hence thesis;
end;
cluster 0wff -> 0-wff for string of S;
coherence
proof
set AF=AtomicFormulasOf S;
let w be string of S; assume w is 0wff; then w in AF; then
w in S-formulasOfMaxDepth 0 by Lm16; hence thesis;
end;
let m;
cluster m-wff -> wff for string of S;
coherence;
let n;
cluster (m+0*n)-wff -> (m+n)-wff for string of S;
coherence
proof
set X=S-formulasOfMaxDepth m, Y=S-formulasOfMaxDepth (m+n);
A1: X c= Y by Lm15;
let w; assume w is (m+0*n)-wff; then w in X;
hence thesis by A1;
end;
end;
registration
let S; let m be natural Number;
cluster m-wff for string of S;
existence
proof
reconsider m as Nat by TARSKI:1;
set w = the 0wff string of S;
w is (0+0*m)-wff; then w is (0+m)-wff; hence thesis;
end;
end;
registration
let S; let m be natural Number;
cluster S-formulasOfMaxDepth m -> non empty;
coherence
proof
set X=S-formulasOfMaxDepth m, phi = the m-wff string of S;
phi in X by Def23; hence thesis;
end;
end;
registration
let S;
cluster wff for string of S;
existence
proof take the 0-wff string of S; thus thesis; end;
end;
definition
let S,U; let I be Element of U-InterpretersOf S, w be wff string of S;
func I-TruthEval w -> Element of BOOLEAN means :Def25:
for m being Nat st w is m-wff holds it=((I,m)-TruthEval).w;
existence
proof
set IU=U-InterpretersOf S, SS=AllSymbolsOf S, III=I, II=I;
consider n such that A1: w is n-wff by Def24;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
set fn=(III,n)-TruthEval;
reconsider ww=w as n-wff string of S by A1;
A2: S-formulasOfMaxDepth nn=dom ((III,nn)-TruthEval) by Def22;
fn.ww=fn /. ww by A2, Def23, PARTFUN1:def 6; then
reconsider IT=fn.ww as Element of BOOLEAN; take IT;
let m;
set fm=(II,m)-TruthEval, f=(II,m+n)-TruthEval, g=(III,n+m)-TruthEval;
reconsider mm=m,nn=n as Element of NAT by ORDINAL1:def 12;
A3: S-formulasOfMaxDepth m=dom ((II,mm)-TruthEval) &
S-formulasOfMaxDepth nn=dom (III,nn)-TruthEval by Def22;
A4: fm c= f & fn c= g & f=g by Lm12;
assume w is m-wff; then
fm.w=f.w by A4, A3, GRFUNC_1:2;
hence IT=fm.w by A2, Def23, A4, GRFUNC_1:2;
end;
uniqueness
proof
let IT1,IT2 be Element of BOOLEAN;
assume A5: for m being Nat st w is m-wff holds IT1=(I,m)-TruthEval.w;
assume A6: for m being Nat st w is m-wff holds IT2=(I,m)-TruthEval.w;
consider m being Nat such that A7: w is m-wff by Def24;
thus IT1=(I,m)-TruthEval.w by A5, A7 .= IT2 by A6,A7;
end;
end;
definition
let S;
func AllFormulasOf S -> set equals
{w where w is string of S: ex m st w is m-wff};
coherence;
end;
registration
let S;
cluster AllFormulasOf S -> non empty;
coherence
proof
set w = the 0-wff string of S; w in AllFormulasOf S; hence thesis;
end;
end;
reserve u,u1,u2 for Element of U, t for termal string of S,
I for (S,U)-interpreter-like Function,
l, l1, l2 for literal (Element of S), m1, n1 for non zero Nat,
phi0 for 0wff string of S, psi,phi,phi1,phi2 for wff string of S;
theorem Th3:
((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
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
((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)).{})
by Lm5;
hence thesis;
end;
theorem
for t being m-termal string of S holds
((I,u1)-TermEval.(m+1)).t = ((I,u2)-TermEval.(m+1+n)).t by Lm6;
theorem curry ((S,U)-TruthEval m) is Function of
U-InterpretersOf S, PFuncs((AllSymbolsOf S)*\{{}},BOOLEAN) by Lm11;
theorem x in X\/Y\/Z iff x in X or x in Y or x in Z by Lm8;
theorem S-formulasOfMaxDepth 0 = AtomicFormulasOf S by Lm16;
definition
let S,m;
redefine func S-formulasOfMaxDepth m means :Def27: :: redefines -formulasOfMaxDepth (FOMODEL2, definition)
for U being non empty set, I being Element of U-InterpretersOf S
holds it=dom (I,m)-TruthEval;
compatibility
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set SS=AllSymbolsOf S, Phim=S-formulasOfMaxDepth m;
defpred P[set] means for U being non empty set, I being Element of U
-InterpretersOf S holds $1=dom (I,m)-TruthEval;
let x being Subset of (SS*\{{}});
thus x=Phim implies P[x]
proof
assume
A1: x=Phim;
thus for U being non empty set, I being Element of U
-InterpretersOf S holds x=dom (I,m)-TruthEval
proof
let U; set II=U-InterpretersOf S; let I be Element of II;
Phim=dom (I,mm)-TruthEval by Def22; hence x=dom (I,m)-TruthEval by A1;
end;
end;
assume
A2: P[x];
for U being non empty set, I being Element of U-InterpretersOf S, nn
being Element of NAT st m=nn holds x=dom (I,nn)-TruthEval by A2;
hence x=Phim by Def22;
end;
end;
Lm17: curry ((S,U)-TruthEval m) is Function of U-InterpretersOf S, Funcs(S
-formulasOfMaxDepth m, BOOLEAN)
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set Fm=(S,U)-TruthEval m, II=U-InterpretersOf S, SS=AllSymbolsOf S,
Phim=S-formulasOfMaxDepth m;
reconsider f=curry Fm as Function of II, PFuncs(SS*\{{}}, BOOLEAN) by Lm11;
A1: dom f=II by FUNCT_2:def 1;
now
let x be object; assume x in II; then reconsider Ix=x as Element of II;
reconsider g=f.Ix as Element of PFuncs(SS*\{{}}, BOOLEAN);
g is BOOLEAN-valued & g=(Ix,m)-TruthEval; then
g=g & dom g=Phim & rng g c= BOOLEAN by Def27;
hence f.x in Funcs(Phim, BOOLEAN) by FUNCT_2:def 2;
end;
hence thesis by FUNCT_2:3, A1;
end;
theorem Th8: (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
set Fm=(S,U)-TruthEval m,II=U-InterpretersOf S,Phim=S-formulasOfMaxDepth m,
SS=AllSymbolsOf S; reconsider mm=m as Element of NAT by ORDINAL1:def 12;
reconsider Fmm=Fm as PartFunc of [:II, SS*\{{}}:], BOOLEAN;
dom Fm c= [:II,SS*\{{}}:]; then
A1: uncurry curry Fm = Fm by FUNCT_5:50;
reconsider f=curry Fm as Function of II, Funcs(Phim, BOOLEAN) by Lm17;
rng f c= Funcs(Phim, BOOLEAN) & dom f=II by FUNCT_2:def 1;
then Fm=Fm & dom Fm = [:II, Phim:] & rng Fm c= BOOLEAN by A1, FUNCT_5:26;
hence Fm in Funcs([:II, Phim:], BOOLEAN) by FUNCT_2:def 2; then
(S,U)-TruthEval.mm in Funcs([:II,Phim:],BOOLEAN) by Def20; hence thesis;
end;
definition
let S,m;
func m-ExFormulasOf S -> set equals
the set of all <*v*>^phi where v is Element of LettersOf S,
phi is Element of S-formulasOfMaxDepth m;
coherence;
func m-NorFormulasOf S -> set equals the set of all
<*TheNorSymbOf S*>^phi1^phi2 where
phi1 is Element of S-formulasOfMaxDepth m,
phi2 is Element of S-formulasOfMaxDepth m;
coherence;
end;
Lm18: dom NorIterator((S,U)-TruthEval m) =
[:U-InterpretersOf S, m-NorFormulasOf S:]
proof
set mm=m, II=U-InterpretersOf S, SS=AllSymbolsOf S, N=TheNorSymbOf S,
Fm=(S,U)-TruthEval mm, Phim=S-formulasOfMaxDepth mm, IT=NorIterator(Fm);
deffunc F(FinSequence, FinSequence)=<*N*>^$1^$2;
defpred P[] means not contradiction;
set A={F(phi1,phi2) where phi1, phi2 is Element of Phim: P[]}, LH=dom IT,
RH=[:II, A:];
Fm is Element of Funcs([:II, Phim:], BOOLEAN) by Th8; then reconsider
Fmm=Fm as Function of [:II, Phim:], BOOLEAN;
A1: dom Fmm=[:II, Phim:] by FUNCT_2:def 1;
reconsider ITT=IT as PartFunc of [:II,SS*\{{}}:], BOOLEAN;
A2: [:II, SS*\{{}}:]=the set of all [x,y] where x is Element of II,
y is Element of SS*\{{}} by DOMAIN_1:19;
now
let z be object; assume
A3: z in LH; then z in [:II, SS*\{{}}:];
then consider x being Element of II, y being Element of SS*\{{}} such that
A4: z=[x,y] by A2;
consider phi1, phi2 being Element of SS*\{{}} such that
A5: y=<*N*>^phi1^phi2 & [x,phi1] in dom Fm & [x,phi2] in dom Fm
by Def18, A3, A4;
reconsider phi11=phi1, phi22=phi2 as Element of Phim
by ZFMISC_1:87, A5, A1;
set yy=F(phi11, phi22); x in II & yy in A & z=[x,yy] by A4, A5;
hence z in RH by ZFMISC_1:def 2;
end; then
A6: LH c= RH;
now
let z be object; assume z in RH; then consider
xx,yy being object such that
A7: xx in II & yy in A & z=[xx,yy] by ZFMISC_1:def 2;
reconsider x=xx as Element of II by A7;
consider phi1, phi2 being Element of Phim such that
A8: yy=F(phi1, phi2) by A7;
reconsider phi11=phi1, phi22=phi2 as string of S;
<*N*>^phi11^phi22 is string of S; then reconsider y=yy as string of S by A8;
[x,phi1] in dom Fmm & [x,phi2] in dom Fmm by A1; then
[x,y] in LH by A8, Def18; hence z in LH by A7;
end;
then RH c= LH; hence thesis by A6;
end;
Lm19: dom ExIterator((S,U)-TruthEval m)=
[:U-InterpretersOf S, m-ExFormulasOf S:]
proof
set mm=m, II=U-InterpretersOf S, SS=AllSymbolsOf S, N=TheNorSymbOf S,
Fm=(S,U)-TruthEval mm, Phim=S-formulasOfMaxDepth mm, IT=ExIterator(Fm),
L=LettersOf S;
deffunc F(set, FinSequence)=<*$1*>^$2;
defpred P[] means not contradiction;
set A={F(v,phi) where v is Element of L, phi is Element of Phim: P[]},
LH=dom IT, RH=[:II, A:];
Fm is Element of Funcs([:II, Phim:], BOOLEAN) by Th8; then reconsider
Fmm=Fm as Function of [:II, Phim:], BOOLEAN;
A1: dom Fmm=[:II, Phim:] by FUNCT_2:def 1;
reconsider ITT=IT as PartFunc of [:II,SS*\{{}}:], BOOLEAN;
A2: [:II, SS*\{{}}:]=the set of all [x,y] where x is Element of II,
y is Element of SS*\{{}} by DOMAIN_1:19;
now
let z be object; assume
A3: z in LH; then z in [:II, SS*\{{}}:];
then consider x being Element of II, y being Element of SS*\{{}} such that
A4: z=[x,y] by A2;
consider v being literal Element of S, w being string of S such that
A5: [x,w] in dom Fm & y=<*v*>^w by Def16, A3, A4;
reconsider phi=w as Element of Phim by A1, A5, ZFMISC_1:87;
reconsider vv=v as Element of L by FOMODEL1:def 14;
y=<*vv*>^phi by A5; then y in A; hence
z in RH by ZFMISC_1:def 2, A4;
end; then
A6: LH c= RH;
now
let z be object; assume z in RH; then consider
xx,yy being object such that
A7: xx in II & yy in A & z=[xx,yy] by ZFMISC_1:def 2;
reconsider x=xx as Element of II by A7; consider vv being Element of L,
phi being Element of Phim such that
A8: yy=F(vv,phi) by A7;
reconsider v=vv as literal Element of S; reconsider w=phi as string of S;
[x,phi] in dom Fm & yy=<*v*>^w by A8, A1;
hence z in LH by A7, Def16;
end; then
RH c= LH; hence thesis by A6;
end;
theorem Th9: S-formulasOfMaxDepth(m+1) =
m-ExFormulasOf S \/ m-NorFormulasOf S \/ S-formulasOfMaxDepth m
proof
set U=the non empty set, n=m+1, II=U-InterpretersOf S, SS=AllSymbolsOf S,
N=TheNorSymbOf S, I = the Element of II;
reconsider mm=m, nn=n as Element of NAT by ORDINAL1:def 12;
set F=(S,U)-TruthEval, Fn=F.nn, Fc=(curry Fn), Dm=S-formulasOfMaxDepth m,
Dn=S-formulasOfMaxDepth n;
F.mm is Element of PFuncs( [:II, SS*\{{}}:], BOOLEAN ); then
reconsider Fm=F.mm as PartFunc of [:II, SS*\{{}}:], BOOLEAN;
A1: (S,U)-TruthEval n=Fn & (S,U)-TruthEval m=Fm by Def20;
reconsider Fcc=Fc as Function of II, Funcs(Dn, BOOLEAN)
by Lm17, A1;
reconsider fn=Fcc.I as Function of Dn, BOOLEAN;
Fm is Element of Funcs([:II, Dm:], BOOLEAN) by Th8;
then reconsider Fmm=Fm as Function of [:II, Dm:], BOOLEAN;
dom fn=Dn & dom Fcc=II by FUNCT_2:def 1; then
A2: Dn=proj2 (dom Fn/\[:{I}, proj2 dom Fn:]) by FUNCT_5:31;
A3: Fn=ExIterator(F.mm) +* NorIterator(F.mm) +* Fm by Def19;
reconsider Em=ExIterator(F.mm) as PartFunc of [:II, SS*\{{}}:], BOOLEAN;
reconsider dEm=dom Em as Relation of II, SS*\{{}};
reconsider dNm=dom (NorIterator (F.mm)), dFm=dom(Fm) as
Relation of II, SS*\{{}};
A4: dFm = dom Fmm .= [:II, Dm:] by FUNCT_2:def 1;
A5: dom Fn = dom (ExIterator(F.mm) +* NorIterator (F.mm)) \/
dom (Fm) by A3, FUNCT_4:def 1 .= dEm\/dNm\/dFm by FUNCT_4:def 1;
set RNNN = m-NorFormulasOf S, REEE = m-ExFormulasOf S;
(S,U)-TruthEval m=Fm by Def20; then
dNm=[:II, RNNN:] & dEm=[:II, REEE:] by Lm18, Lm19; then
A6: dEm\/dNm\/dFm = [:II, REEE\/RNNN:]\/[:II, Dm:] by A4, ZFMISC_1:97 .=
[:II,REEE\/RNNN\/Dm:] by ZFMISC_1:97;
reconsider sub=[:{I}, REEE\/RNNN\/Dm:] as Subset of
[:II, REEE\/RNNN\/Dm:] by ZFMISC_1:96;
Dn = rng ([:II,REEE\/RNNN\/Dm:] /\ sub )
by A6, A2, A5 .=
REEE\/RNNN\/Dm; hence thesis;
end;
theorem Th10: AtomicFormulasOf S is S-prefix
proof
set AF=AtomicFormulasOf S, SS=AllSymbolsOf S, TT=AllTermsOf S, C=S-multiCat;
now
let p1,q1,p2,q2 be SS-valued FinSequence;
assume p1 in AF; then consider phi1 being string of S such that
A1: p1=phi1 & phi1 is 0wff;
assume p2 in AF; then consider phi2 being string of S such that
A2: p2=phi2 & phi2 is 0wff; consider r1 being relational Element of S,
T1 being |.ar r1.|-element Element of TT* such that
A3: phi1=<*r1*>^(C.T1) by A1;
consider r2 being relational Element of S,
T2 being |.ar r2.|-element Element of TT* such that
A4: phi2=<*r2*>^(C.T2) by A2; assume p1^q1=p2^q2; then
A5: <*r1*>^((C.T1)^q1)=(<*r2*>^(C.T2))^q2 by A1, A2, A3, A4, FINSEQ_1:32 .=
<*r2*>^((C.T2)^q2) by FINSEQ_1:32; then
A6: r1 = (<*r2*>^((C.T2)^q2)).1
by FINSEQ_1:41 .= r2 by FINSEQ_1:41;
set n=|.ar r1.|, nT=n-tuples_on TT;
reconsider T11=T1, T22=T2 as Element of nT by FOMODEL0:16, A6;
reconsider P=C.:(nT) as SS-prefix set;
A7: (SS*\{{}})* c= SS** & TT*c=(SS*\{{}})*; then
T1 in SS** & T2 in SS** & dom C=SS**
by FUNCT_2:def 1; then
A8: C.T11 in P & C.T22 in P by FUNCT_1:def 6;
reconsider T111=T1, T222=T2 as Element of SS**
by A7;
(C.T111)^q1=(C.T222)^q2 by A6, FINSEQ_1:33, A5;
hence p1=p2 & q1=q2 by A1, A2, A8, FOMODEL0:def 19, A3, A4, A6;
end;
then AF is SS-prefix; hence thesis;
end;
registration
let S;
cluster AtomicFormulasOf S -> S-prefix for set;
coherence by Th10;
end;
registration
let S;
cluster S-formulasOfMaxDepth 0 -> S-prefix for set;
coherence
proof
S-formulasOfMaxDepth 0 = AtomicFormulasOf S by Lm16; hence thesis;
end;
end;
definition
let S, phi;
func Depth phi -> Nat means :Def30:
phi is it-wff & for n st phi is n-wff holds it <= n;
existence
proof
defpred P[Nat] means phi is $1-wff; consider m such that
A1: phi is m-wff by Def24;
A2: ex n being Nat st P[n] by A1; consider IT being Nat such that
A3: P[IT] & for n st P[n] holds IT <= n from NAT_1:sch 5(A2); take IT;
thus thesis by A3;
end;
uniqueness
proof
let IT1, IT2 be Nat; assume
A4: phi is IT1-wff & for n st phi is n-wff holds IT1 <= n; assume
A5: phi is IT2-wff & for n st phi is n-wff holds IT2 <= n;
A6: IT2 <= IT1 by A5, A4;
IT1 <= IT2 by A4, A5; hence thesis by A6, XXREAL_0:1;
end;
end;
Lm20: phi in S-formulasOfMaxDepth m \ S-formulasOfMaxDepth 0 implies
ex n st (phi is (n+1)-wff & not phi is n-wff & n+1<=m)
proof
set Phim=S-formulasOfMaxDepth m, Phi0=S-formulasOfMaxDepth 0; assume
B1: phi in Phim \ Phi0; then not phi in Phi0
by XBOOLE_0:def 5; then not phi is 0-wff; then
Depth phi <> 0 by Def30; then consider n such that
A1: Depth phi=n+1 by NAT_1:6; take n; not n+1<=n+0 by XREAL_1:8;
hence phi is (n+1)-wff & not phi is n-wff by Def30, A1;
phi is m-wff by B1;
hence n+1 <= m by A1, Def30;
end;
Lm21: (w is (m+1)-wff & not w is m-wff) implies (
(ex v being literal Element of S,phi being m-wff string of S st w=<*v*>^phi)
or
(ex phi1, phi2 being m-wff string of S st w=<*TheNorSymbOf S*>^phi1^phi2))
proof
set Phim=S-formulasOfMaxDepth m, PhiM=S-formulasOfMaxDepth (m+1),
L=LettersOf S, N=TheNorSymbOf S, EF = m-ExFormulasOf S, NF=m-NorFormulasOf S;
assume w is (m+1)-wff; then w in PhiM; then w in
EF\/NF\/Phim by Th9; then
A1: w in EF or w in NF or w in Phim by Lm8; assume
A2: w is non m-wff; assume
A3: not ex v being literal Element of S,
phi being m-wff string of S st w=<*v*>^phi;
w in EF implies
ex v being literal Element of S,
phi being m-wff string of S st w=<*v*>^phi
proof
assume w in EF; then consider vv being Element of L, phi being Element of Phim
such that
A4: w=<*vv*>^phi;
reconsider phii=phi as m-wff string of S by Def23;
reconsider v=vv as literal Element of S;
take v; take phii; thus thesis by A4;
end;
then consider phi1, phi2 being Element of Phim such that
A5: w=<*N*>^phi1^phi2 by A3, A2, A1;
reconsider phi11=phi1,phi22=phi2 as m-wff string of S by Def23;
take phi11,phi22; thus thesis by A5;
end;
registration
let S, m; let phi1, phi2 be m-wff string of S;
cluster <*TheNorSymbOf S*>^phi1^phi2 -> (m+1)-wff for string of S;
coherence
proof
set N=TheNorSymbOf S, Phim=S-formulasOfMaxDepth m, NF=m-NorFormulasOf S,
PhiM=S-formulasOfMaxDepth (m+1), EF=m-ExFormulasOf S, IT=<*N*>^phi1^phi2;
reconsider phi11=phi1, phi22=phi2 as Element of Phim by Def23;
IT=<*N*>^phi11^phi22; then IT in NF;
then IT in EF\/NF\/Phim by Lm8; then reconsider ITT=IT as
Element of PhiM by Th9; ITT is (m+1)-wff; hence thesis;
end;
end;
registration
let S, phi1, phi2;
cluster <*TheNorSymbOf S*>^phi1^phi2 -> wff for string of S;
coherence
proof
set N=TheNorSymbOf S, IT=<*N*>^phi1^phi2; consider m such that
A1: phi1 is m-wff by Def24; consider n such that
A2: phi2 is n-wff by Def24;
reconsider phi11=phi1 as (m+0*n)-wff string of S by A1;
reconsider phi22=phi2 as (n+0*m)-wff string of S by A2;
reconsider phi111=phi11 as (m+n)-wff string of S;
reconsider phi222=phi22 as (m+n)-wff string of S;
<*N*>^phi111^phi222 is (m+n+1)-wff string of S; hence thesis;
end;
end;
registration
let S, m; let phi be m-wff string of S, v be literal Element of S;
cluster <*v*>^phi -> (m+1)-wff for string of S;
coherence
proof
set L=LettersOf S, Phim=S-formulasOfMaxDepth m, NF=m-NorFormulasOf S,
PhiM=S-formulasOfMaxDepth (m+1), EF=m-ExFormulasOf S, IT=<*v*>^phi;
reconsider vv=v as Element of L by FOMODEL1:def 14; reconsider phii=phi as
Element of Phim by Def23; IT=<*vv*>^phii; then
IT in EF; then IT in EF\/NF\/Phim by Lm8; then reconsider ITT=IT as
Element of PhiM by Th9; ITT is (m+1)-wff; hence thesis;
end;
end;
registration
let S,l,phi;
cluster <*l*>^phi -> wff for string of S;
coherence
proof
consider m such that
A1: phi is m-wff by Def24; reconsider phii=phi as m-wff string of S by A1;
set IT=<*l*>^phii; IT is (m+1)-wff; hence thesis;
end;
end;
registration
let S, w; let s be non relational Element of S;
cluster <*s*>^w -> non 0wff for string of S;
coherence
proof
set FC=S-firstChar, IT=<*s*>^w, SS=AllSymbolsOf S;
FC.IT = IT.1 by FOMODEL0:6 .= s by FINSEQ_1:41;
hence thesis;
end;
end;
registration
let S, w1, w2; let s be non relational Element of S;
cluster <*s*>^w1^w2 -> non 0wff for string of S;
coherence
proof
<*s*>^w1^w2=<*s*>^(w1^w2) by FINSEQ_1:32; hence thesis;
end;
end;
registration
let S;
cluster TheNorSymbOf S -> non relational for Element of S;
coherence;
end;
registration
let S, w;
cluster <*TheNorSymbOf S*>^w -> non 0wff for string of S;
coherence;
end;
registration
let S,l,w;
cluster <*l*>^w -> non 0wff for string of S;
coherence;
end;
definition
let S, w;
attr w is exal means :Def31: S-firstChar.w is literal;
end;
registration
let S,w,l;
cluster <*l*>^w -> exal for string of S;
coherence
proof
set ww=<*l*>^w, F=S-firstChar; F.ww = ww.1 by FOMODEL0:6 .=
l by FINSEQ_1:41; hence thesis;
end;
end;
registration
let S,m1;
cluster exal for m1-wff string of S;
existence
proof
consider m such that
A1: m1=m+1 by NAT_1:6; set phi = the m-wff string of S,
l =the literal Element of S, psi=<*l*>^phi;
reconsider psii=psi as m1-wff string of S by A1;
take psii; thus thesis;
end;
end;
registration
let S;
cluster exal -> non 0wff for string of S;
coherence;
end;
registration
let S,m1;
cluster non 0wff for exal m1-wff string of S;
existence
proof
set l = the literal Element of S; consider m such that
A1: m1=m+1 by NAT_1:6; set phi = the m-wff string of S;
reconsider psi=<*l*>^phi as exal m1-wff string of S by A1; take psi;
thus thesis;
end;
end;
registration
let S;
cluster non 0wff for exal wff string of S;
existence
proof
take the non 0wff exal (the non zero Nat)-wff string of S;
thus thesis;
end;
end;
Lm22: phi is non 0wff implies Depth phi <> 0
proof assume phi is non 0wff; then not phi is 0-wff;
hence Depth phi <> 0 by Def30; end;
registration
let S; let phi be non 0wff wff string of S;
cluster Depth phi -> non zero for Nat;
coherence by Lm22;
end;
Lm23: w is wff & w is non 0wff implies
(w.1 in LettersOf S or w.1=TheNorSymbOf S)
proof
set L=LettersOf S, N=TheNorSymbOf S, SS=AllSymbolsOf S; assume w is wff;
then reconsider ww=w as wff string of S; set n=Depth ww; assume
w is non 0wff; then consider m such that
A1: n=m+1 by NAT_1:6; m+1>m+0 by XREAL_1:8; then
ww is (m+1)-wff & not ww is m-wff by Def30, A1;
then per cases by Lm21;
suppose ex v being literal Element of S, phi being m-wff string of S
st w=<*v*>^phi; then consider v being literal Element of S,
phi being m-wff string of S such that
A2: w=<*v*>^phi; v = w.1 by A2, FINSEQ_1:41;
hence thesis by FOMODEL1:def 14;
end;
suppose ex phi1, phi2 being m-wff string of S st
w=<*N*>^phi1^phi2; then consider phi1, phi2 being
m-wff string of S such that
A3: w=<*N*>^phi1^phi2; w.1=(<*N*>^(phi1^phi2)).1 by A3, FINSEQ_1:32 .=
N by FINSEQ_1:41; hence thesis;
end;
end;
registration
let S; let w be non 0wff wff string of S;
cluster S-firstChar.w -> non relational for Element of S;
coherence
proof
set F=S-firstChar, L=LettersOf S, N=TheNorSymbOf S, SS=AllSymbolsOf S;
per cases by Lm23;
suppose w.1 in L; then reconsider IT=F.w as Element of L by FOMODEL0:6;
IT is non relational; hence thesis;
end;
suppose w.1=N; hence thesis by FOMODEL0:6; end;
end;
end;
Lm24: S-formulasOfMaxDepth m is S-prefix
proof
set SS=AllSymbolsOf S,AF=AtomicFormulasOf S, Nor=TheNorSymbOf S,
Phi0=S-formulasOfMaxDepth 0, F=S-firstChar;
defpred P[Nat] means S-formulasOfMaxDepth $1 is SS-prefix;
A1: P[0];
A2: for n st P[n] holds P[n+1]
proof
let n; assume
A3: P[n];
set N=n+1, PhiN=S-formulasOfMaxDepth N, Phin=S-formulasOfMaxDepth n;
A4: PhiN\Phi0 is SS-prefix
proof
now
let p1,q1,p2,q2 be SS-valued FinSequence; assume
A5: p1 in PhiN \ Phi0; then reconsider
phi1=p1 as N-wff string of S by Def23; consider m1 being Nat such that
A6: phi1 is (m1+1)-wff & not phi1 is m1-wff & m1+1 <= N by Lm20, A5;
assume
A7: p2 in PhiN \ Phi0; then reconsider
phi2=p2 as N-wff string of S by Def23; consider m2 being Nat such that
A8: phi2 is (m2+1)-wff & not phi2 is m2-wff & m2+1 <= N by Lm20, A7;
consider k1 being Nat such that
A9: n=m1+k1 by A6, XREAL_1:8, NAT_1:10; consider k2 being Nat such that
A10: n=m2+k2 by A8, XREAL_1:8, NAT_1:10; assume
A11: p1^q1=p2^q2;
per cases by Lm21, A6;
suppose (ex v1 being literal Element of S, phi11 being m1-wff string of S st
phi1=<*v1*>^phi11); then consider
v1 being literal Element of S, phi11 being m1-wff string of S such that
A12: phi1=<*v1*>^phi11;
per cases by Lm21, A8;
suppose ex v2 being literal Element of S, phi22 being
m2-wff string of S st phi2=<*v2*>^phi22; then consider v2 being
literal Element of S, phi22 being m2-wff string of S such that
A13: phi2=<*v2*>^phi22; <*v2*>^phi22^q2 =
<*v1*>^(phi11^q1) by A13, A11, A12, FINSEQ_1:32; then
A14: <*v2*>^(phi22^q2)=<*v1*>^(phi11^q1) by FINSEQ_1:32; then
A15: (<*v2*>^(phi22^q2)).1 = v1 by FINSEQ_1:41; then
A16: v2=v1 by FINSEQ_1:41;
<*v1*>^(phi22^q2)=<*v1*>^(phi11^q1) by A14, A15, FINSEQ_1:41; then
A17: phi22^q2=phi11^q1 by FINSEQ_1:33; phi11 is (m1+0*k1)-wff &
phi22 is (m2+0*k2)-wff; then phi11 in Phin & phi22 in Phin
by A9, A10, Def23;
hence p1=p2 & q1=q2 by A12, A16, A13, A3, A17, FOMODEL0:def 19;
end;
suppose
ex r2, s2 being m2-wff string of S st phi2=<*Nor*>^r2^s2; then
consider r2, s2 being m2-wff string of S such that
A18: phi2=<*Nor*>^r2^s2; phi1.1 = (phi2^q2).1 by FOMODEL0:28, A11 .=
phi2.1 by FOMODEL0:28 .= (<*Nor*>^(r2^s2)).1 by A18, FINSEQ_1:32 .= Nor
by FINSEQ_1:41;
hence p1=p2 & q1=q2 by A12, FINSEQ_1:41;
end;
end;
suppose ex r1, s1 being m1-wff string of S st phi1=<*Nor*>^r1^s1; then
consider r1, s1 being m1-wff string of S such that
A19: phi1=<*Nor*>^r1^s1;
A20: phi1.1 = (<*Nor*>^(r1^s1)).1 by A19, FINSEQ_1:32
.= Nor by FINSEQ_1:41;
per cases by A8, Lm21;
suppose ex v2 being literal Element of S, phi22 being
m2-wff string of S st phi2=<*v2*>^phi22; then consider v2 being
literal Element of S, phi22 being m2-wff string of S such that
A21: phi2=<*v2*>^phi22;
phi1.1 = (phi2^q2).1 by FOMODEL0:28, A11 .=
(<*v2*>^phi22).1 by FOMODEL0:28, A21 .= v2 by FINSEQ_1:41;
hence p1=p2 & q1=q2 by A20;
end;
suppose ex r2, s2 being m2-wff string of S st phi2=<*Nor*>^r2^s2; then
consider r2, s2 being m2-wff string of S such that
A22: phi2=<*Nor*>^r2^s2; r1 is (m1+0*k1)-wff & r2 is (m2+0*k2)-wff; then
A23: r1 in Phin & r2 in Phin & s1 in Phin & s2 in Phin by A9, A10, Def23;
<*Nor*>^((r1^s1)^q1) = <*Nor*>^(r1^s1)^q1 by FINSEQ_1:32 .=
<*Nor*>^r2^s2^q2 by A19, A22, A11, FINSEQ_1:32.=
<*Nor*>^(r2^s2)^q2 by FINSEQ_1:32 .= <*Nor*>^(r2^s2^q2) by FINSEQ_1:32; then
r1^s1^q1 = r2^s2^q2 by FINSEQ_1:33 .= r2^(s2^q2) by FINSEQ_1:32; then
r1^(s1^q1)=r2^(s2^q2) by FINSEQ_1:32; then
r1=r2 & s1^q1=s2^q2 by A3, FOMODEL0:def 19, A23;
hence p1=p2 & q1=q2 by A19, A22, A3, A23, FOMODEL0:def 19;
end;
end;
end;
hence thesis;
end;
now
let p1,q1,p2,q2 be SS-valued FinSequence; assume
A24: p1 in PhiN & p2 in PhiN & p1^q1=p2^q2; then reconsider
phi1=p1, phi2=p2 as N-wff string of S by Def23;
per cases;
suppose A25: phi1 in Phi0; then phi1 is 0-wff; then
reconsider phi11=phi1 as 0wff string of S;
F.phi11 is relational Element of S; then phi1.1 is relational Element of S
by FOMODEL0:6; then
(phi2^q2).1 is relational Element of S by A24, FOMODEL0:28; then
phi2.1 is relational Element of S by FOMODEL0:28; then F.phi2 is relational
by FOMODEL0:6; then phi2 is 0wff; then phi2 is 0-wff;
then phi2 in Phi0 & phi1 in Phi0 by A25;
hence p1=p2 & q1=q2 by A24, FOMODEL0:def 19;
end;
suppose A26: not phi1 in Phi0; then phi1 is non 0-wff; then
reconsider phi11=phi1 as non 0wff wff string of S;
F.phi2 = phi2.1 by FOMODEL0:6 .= (phi1^q1).1 by A24, FOMODEL0:28 .=
phi1.1 by FOMODEL0:28 .= F.phi11 by FOMODEL0:6; then
phi2 is non 0-wff; then not phi2 in Phi0;
then phi1 in PhiN\Phi0 & phi2 in PhiN\Phi0 by A24, A26, XBOOLE_0:def 5;
hence p1=p2 & q1=q2 by A24, A4; end;
end;
hence thesis by FOMODEL0:def 19;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2); then
S-formulasOfMaxDepth m is SS-prefix; hence thesis;
end;
registration
let S, m;
cluster S-formulasOfMaxDepth m -> S-prefix for set;
coherence by Lm24;
end;
definition
let S;
redefine func AllFormulasOf S -> Subset of (AllSymbolsOf S)*\{{}}; :: redefines AllFormulasOf (FOMODEL2, definition)
coherence
proof
set FF=AllFormulasOf S, SS=AllSymbolsOf S, IT=SS*\{{}};
now
let x be object;
assume x in FF; then consider phi being string of S such that
A1: x=phi & ex m st phi is m-wff; thus x in IT by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let S;
cluster -> wff for Element of AllFormulasOf S;
coherence
proof
set FF=AllFormulasOf S; let x be Element of FF; x in FF; then
consider phi being string of S such that
A1: x=phi & ex m st phi is m-wff; thus thesis by A1;
end;
end;
Lm25: AllFormulasOf S is S-prefix
proof
set FF=AllFormulasOf S, SS=AllSymbolsOf S;
now
let p1,q1,p2,q2 be SS-valued FinSequence; assume
A1: p1 in FF & p2 in FF & p1^q1=p2^q2; then reconsider phi1=p1, phi2=p2 as
wff string of S; consider m1 being Nat such that
A2: phi1 is m1-wff by Def24; consider m2 being Nat such that
A3: phi2 is m2-wff by Def24; set N=m1+m2, PhiN=S-formulasOfMaxDepth N;
phi1 is (m1+0*m2)-wff & phi2 is (m2+0*m1)-wff by A2, A3; then reconsider
phi11=phi1, phi22=phi2 as N-wff string of S; phi11 in PhiN & phi22 in PhiN
by Def23; hence p1=p2 & q1=q2 by A1, FOMODEL0:def 19;
end;
then FF is SS-prefix; hence thesis;
end;
registration
let S;
cluster AllFormulasOf S -> S-prefix for set;
coherence by Lm25;
end;
theorem dom NorIterator((S,U)-TruthEval m) =
[:U-InterpretersOf S, m-NorFormulasOf S:] by Lm18;
theorem dom ExIterator((S,U)-TruthEval m)=
[:U-InterpretersOf S, m-ExFormulasOf S:] by Lm19;
Lm26: (U-deltaInterpreter)"{1}=(U-concatenation).:(id (1-tuples_on U))
proof
set d=U-deltaInterpreter, f=U-concatenation, U1=1-tuples_on U,
U2=2-tuples_on U, A=f.:(id U1), B=U2;
A1: d"{1} = A/\(1+1)-tuples_on U by FOMODEL0:24 .=
f.:(id U1)/\(f.:[:U1,U1:]) by FOMODEL0:22;
reconsider O=f.:(id U1) as Subset of f.:[:U1, U1:] by RELAT_1:123;
O /\ f.:[:U1,U1:]=O null f.:[:U1, U1:] .= O; hence thesis by A1;
end;
theorem Th13: U-deltaInterpreter"{1} =
the set of all <*u,u*> where u is Element of U
proof
set RH=the set of all <*u,u*> where u is Element of U;
set LH=U-deltaInterpreter"{1}, X=(U-concatenation).:(id (1-tuples_on U));
LH=X & X=RH by Lm26, FOMODEL0:38; hence thesis;
end;
definition
let S;
redefine func TheEqSymbOf S -> Element of S; :: redefines TheEqSymbOf (FOMODEL1, definition)
coherence;
end;
registration
let S;
cluster ar(TheEqSymbOf S) + 2 -> zero for number;
coherence
proof set E=TheEqSymbOf S; ar E=-2 by FOMODEL1:def 23; hence thesis; end;
cluster |.ar(TheEqSymbOf S).| - 2 -> zero for number;
coherence
proof
set E=TheEqSymbOf S; A1: |.-2.|=-(-2) by ABSVALUE:def 1 .= 2;
|.ar(E).|=2 by A1, FOMODEL1:def 23; hence thesis;
end;
end;
theorem Th14:
for phi being 0wff string of S, I being (S,U)-interpreter-like Function
holds (S-firstChar.phi <> TheEqSymbOf S implies
I-AtomicEval phi=(I.(S-firstChar.phi)).((I-TermEval)*(SubTerms phi)))
& (S-firstChar.phi=TheEqSymbOf S implies
I-AtomicEval phi = (U-deltaInterpreter).((I-TermEval)*(SubTerms phi)))
proof
let phi be 0wff string of S, I be (S,U)-interpreter-like Function;
set TT=AllTermsOf S, E=TheEqSymbOf S, p=SubTerms phi, F=S-firstChar, r=F.phi,
n=|.ar r.|, AF=AtomicFormulasOf S, d=U-deltaInterpreter, p=SubTerms phi,
V=I-AtomicEval phi, f=(I===).r, UV=I-TermEval, G=I.r;
A1: |.ar E.|-2=0;
thus r<>E implies V=(I.(F.phi)).(UV*p)
proof
assume r <> E; then
not r in dom (E .--> d) by TARSKI:def 1;
hence V=G.(UV*p) by FUNCT_4:11;
end;
assume r=E; then
A2: r in {E} & n=2 by TARSKI:def 1, A1; then r in dom (E .--> d); then f = (E
.--> d).r by FUNCT_4:13 .= d by A2, FUNCOP_1:7;
hence V=d.(UV*p);
end;
theorem for I being (S,U)-interpreter-like Function,
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
let I being (S,U)-interpreter-like Function, phi being 0wff string of S;
set E=TheEqSymbOf S, p=SubTerms phi, F=S-firstChar, s=F.phi, UV=I-TermEval,
V=I-AtomicEval phi,d=U-deltaInterpreter,U2=2-tuples_on U,TT=AllTermsOf S,D=
the set of all <*u,u*> where u is Element of U;
set n=|.ar s.|;
A1: U2=the set of all <*u1,u2*> where u1, u2 is Element of U
by FINSEQ_2:99;
A2: |.ar E.|-2=0; reconsider r=s as relational Element of S; set f=I===.r;
reconsider EE=E as relational Element of S; assume
A3: s=E; then V=d.(UV*p) & n=2 by Th14, A2; then
V=1 iff UV*p in d"{1} by FOMODEL0:25; then
A4: V=1 iff UV*p in D by Th13;
reconsider pp=p as 2-element FinSequence of TT by FINSEQ_1:def 11, A3, A2;
reconsider q=UV*pp as FinSequence of U;
reconsider qq=q as Element of U2 by FOMODEL0:16; qq in U2; then
consider u1, u2 being Element of U such that
A5: qq=<*u1,u2*> by A1; 1<=2 ; then 1<=1 & 1 <= len q
& 1<=2 & 2<=len q by CARD_1:def 7; then 1 in Seg (len q) & 2 in Seg
(len q); then 1 in dom q & 2 in dom q by FINSEQ_1:def 3; then
A7: q.1=UV.(p.1) & q.2=UV.(p.2) by FUNCT_1:12;
q in D implies UV.(p.1)=UV.(p.2)
proof
assume q in D; then consider u being Element of U such that
A8: <*u,u*>=q; q.1=u & q.2=u by A8;
hence thesis by A7;
end;
hence thesis by A4, A7, A5;
end;
registration
let S,m;
cluster m-ExFormulasOf S -> non empty for set;
coherence
proof
set IT=m-ExFormulasOf S, L=LettersOf S, Phim=S-formulasOfMaxDepth m;
set l=the Element of L, phi=the Element of Phim;
set x=<*l*>^phi; x in IT; hence thesis;
end;
end;
registration
let S,m;
cluster m-NorFormulasOf S -> non empty for set;
coherence
proof
set IT=m-NorFormulasOf S, Phim=S-formulasOfMaxDepth m, N=TheNorSymbOf S,
phi1=the Element of Phim, x=<*N*>^phi1^phi1; x in IT; hence thesis;
end;
end;
definition
let S,m;
redefine func m-NorFormulasOf S -> Subset of (AllSymbolsOf S)*\{{}}; :: redefines -NorFormulasOf (FOMODEL2, definition)
coherence
proof
set IT=m-NorFormulasOf S, Phim=S-formulasOfMaxDepth m,
N=TheNorSymbOf S, SS=AllSymbolsOf S;
now
let x be object;assume x in IT;
then ex phi1,phi2 being Element of Phim st x=<*N*>^phi1^phi2;
hence x in SS*\{{}};
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let S; let w be exal string of S;
cluster S-firstChar.w -> literal for Element of S;
coherence by Def31;
end;
registration
let S,m;
cluster -> non exal for Element of m-NorFormulasOf S;
coherence
proof
set IT=m-NorFormulasOf S, Phim=S-formulasOfMaxDepth m, F=S-firstChar,
N=TheNorSymbOf S, SS=AllSymbolsOf S; let x be Element of IT;
x in IT; then consider phi1, phi2 being Element of Phim such that
A1: x=<*N*>^phi1^phi2; reconsider
phi=x as string of S; F.phi=phi.1 by FOMODEL0:6 .=
(<*N*>^(phi1^phi2)).1 by FINSEQ_1:32, A1 .= N by FINSEQ_1:41;
hence thesis;
end;
end;
Lm27: Depth phi=m+1 & phi is exal implies phi in m-ExFormulasOf S
proof
set p=Depth phi, Phim=S-formulasOfMaxDepth m, E=m-ExFormulasOf S,
PhiM=S-formulasOfMaxDepth (m+1), N=m-NorFormulasOf S;
Z0: PhiM\Phim = (E\/N\/Phim)\Phim by Th9 .= (E\/N)\Phim by XBOOLE_1:40;
B0: m+0<m+1 by XREAL_1:8;
assume p=m+1; then phi is (m+1)-wff & not phi is m-wff by B0,Def30; then
phi in PhiM & not phi in Phim; then
Z1: phi in PhiM\Phim by XBOOLE_0:def 5;
assume phi is exal; then
not phi in N; hence phi in E by Z1, XBOOLE_0:def 3, Z0;
end;
Lm28: Depth (<*l*>^phi1) > Depth phi1
proof
set nor=TheNorSymbOf S, phi=<*l*>^phi1, m=Depth phi1, M=Depth phi,
L=LettersOf S; consider n such that
B1: M=n+1 by NAT_1:6; set Phin=S-formulasOfMaxDepth n;
phi in n-ExFormulasOf S by Lm27, B1; then
consider v being Element of L, psi being Element of Phin such that
B0: phi=<*v*>^psi & not contradiction;
v = (<*v*>^psi).1 by FINSEQ_1:41 .= l by B0, FINSEQ_1:41; then
psi=phi1 by B0, FINSEQ_1:33; then phi1 is n-wff; then
m<=n by Def30;
then m +0 < n+1 by XREAL_1:8; hence thesis by B1;
end;
definition
let S,m;
redefine func m-ExFormulasOf S -> Subset of (AllSymbolsOf S)*\{{}}; :: redefines -ExFormulasOf (FOMODEL2, definition)
coherence
proof
set IT=m-ExFormulasOf S, SS=AllSymbolsOf S, Phim=S-formulasOfMaxDepth m,
L=LettersOf S;
now
let x be object; assume x in IT; then ex l being Element of L,
phi being Element of Phim st x=<*l*>^phi;
hence x in SS*\{{}};
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let S,m;
cluster -> exal for Element of m-ExFormulasOf S;
coherence
proof
set E=m-ExFormulasOf S, L=LettersOf S, Phim=S-formulasOfMaxDepth m;
let x be Element of E; x in E; then consider l being Element of L,
phi being Element of Phim such that
A1: x=<*l*>^phi; thus thesis by A1;
end;
end;
Lm29: (Depth phi=m+1 & not phi is exal) implies phi in m-NorFormulasOf S
proof
set p=Depth phi, Phim=S-formulasOfMaxDepth m, E=m-ExFormulasOf S,
PhiM=S-formulasOfMaxDepth (m+1), N=m-NorFormulasOf S;
Z0: PhiM\Phim = (E\/N\/Phim)\Phim by Th9 .= (E\/N)\Phim by XBOOLE_1:40;
B0: m+0<m+1 by XREAL_1:8;
assume p=m+1; then phi is (m+1)-wff & not phi is m-wff by B0,Def30; then
phi in PhiM & not phi in Phim;then
Z1: phi in PhiM\Phim by XBOOLE_0:def 5; assume not phi is exal; then
not phi in E;
hence phi in N by Z0, Z1, XBOOLE_0:def 3;
end;
registration
let S;
cluster non literal for Element of S;
existence proof take TheNorSymbOf S; thus thesis; end;
end;
registration
let S, w; let s be non literal Element of S;
cluster <*s*>^w -> non exal for string of S;
coherence
proof
set IT=<*s*>^w, F=S-firstChar, SS=AllSymbolsOf S;
F.IT = IT.1 by FOMODEL0:6 .= s by FINSEQ_1:41; hence thesis;
end;
end;
registration
let S,w1,w2; let s be non literal Element of S;
cluster <*s*>^w1^w2 -> non exal for string of S;
coherence
proof
<*s*>^w1^w2 = <*s*>^(w1^w2) by FINSEQ_1:32; hence thesis;
end;
end;
registration
let S;
cluster TheNorSymbOf S -> non literal for Element of S;
coherence;
end;
theorem Th16:
phi in AllFormulasOf S
proof
set AF=AllFormulasOf S; consider m such that
A1: phi is m-wff by Def24; thus thesis by A1;
end;
Lm30: Depth (<*TheNorSymbOf S*>^phi1^phi2) > Depth phi1 &
Depth (<*TheNorSymbOf S*>^phi1^phi2) > Depth phi2
proof
set nor=TheNorSymbOf S, phi=<*nor*>^phi1^phi2, m1=Depth phi1, m2=Depth phi2,
M=Depth phi, L=LettersOf S, FF=AllFormulasOf S, SS=AllSymbolsOf S;
consider n such that
B0: M=n+1 by NAT_1:6; set Phin=S-formulasOfMaxDepth n;
phi in n-NorFormulasOf S by Lm29, B0; then
consider phi11, phi22 being Element of Phin such that
B1: phi=<*nor*>^phi11^phi22 & not contradiction;
reconsider phi111=phi11, phi222=phi22 as n-wff string of S by Def23;
<*nor*>^(phi1^phi2) = phi by FINSEQ_1:32
.= <*nor*>^(phi11^phi22) by B1, FINSEQ_1:32; then
B2: phi1^phi2=phi111^phi222 by FINSEQ_1:33;
phi111 in FF & phi1 in FF by Th16; then
phi1 is n-wff & phi2 is n-wff by FOMODEL0:def 19, B2; then
m1 <= n & m2 <= n by Def30; then m1+0<n+1 & m2+0 < n+1 by XREAL_1:8;
hence thesis by B0;
end;
Lm31: Depth (<*TheNorSymbOf S*>^phi1^phi2) = max(Depth phi1, Depth phi2)+1
proof
set nor=TheNorSymbOf S, phi=<*nor*>^phi1^phi2, m1=Depth phi1,
m2= Depth phi2, m=max(m1,m2), M=Depth phi; M<=M & M>m1 & M>m2 by Lm30; then
M>m by XXREAL_0:def 10; then
B1: m+1<=M by NAT_1:13;
reconsider mm = m as Nat by XXREAL_0:16;
reconsider d1=m-m1, d2=m-m2 as Nat;
phi1 is (m1+0*d1)-wff & phi2 is (m2+0*d2)-wff by Def30; then
phi1 is (m1+d1)-wff & phi2 is (m2+d2)-wff; then
reconsider phi11=phi1, phi22=phi2 as m-wff string of S;
J1:now
let n; assume phi is n-wff; then n>=M by Def30;
hence n>=m+1 by B1, XXREAL_0:2;
end;
set Phim=S-formulasOfMaxDepth mm, NF=mm-NorFormulasOf S,
PhiM=S-formulasOfMaxDepth (mm+1), EF=mm-ExFormulasOf S;
reconsider phi111=phi11, phi222=phi22 as Element of Phim by Def23;
phi=<*nor*>^phi111^phi222; then phi in NF;
then phi in EF\/NF\/Phim by Lm8; then reconsider ITT=phi as
Element of PhiM by Th9; ITT is (m+1)-wff; then
<*nor*>^phi11^phi22 is (m+1)-wff string of S;
hence M=m+1 by Def30,J1;
end;
notation
let S; let m be natural Number; let w;
antonym w is m-nonwff for w is m-wff;
end;
registration
let m, S;
::# cluster m-nonwff -> (non ((m)-wff)) string of S; coherence by DefWff3;
::# The clustering above gives a nasty misterious error, as all the schemes
::# cluster xxx -> non (yyy-attribute) type;
::# this is the reason why introduced attribute -nonwff itself, indeed :)
cluster non m-wff -> m-nonwff for string of S;
coherence;
end;
registration
let S, phi1, phi2;
cluster <*TheNorSymbOf S*>^phi1^phi2 ->
(max(Depth phi1, Depth phi2))-nonwff for string of S;
coherence
proof
set nor=TheNorSymbOf S, phi=<*nor*>^phi1^phi2, m1=Depth phi1, m2=Depth phi2,
m=Depth phi, M=max(m1,m2); m=M+1 by Lm31; then
m > M+0 by XREAL_1:8; hence thesis by Def30;
end;
end;
registration
let S,phi,l;
cluster <*l*>^phi -> (Depth phi)-nonwff for string of S;
coherence
proof
set m=Depth phi, psi=<*l*>^phi, M=Depth psi;
m<M by Lm28; hence thesis by Def30;
end;
end;
registration
let S,phi,l;
cluster <*l*>^phi -> (1+Depth phi)-wff for string of S;
coherence
proof
set m=Depth phi, psi=<*l*>^phi, M=Depth psi;
reconsider phii=phi as m-wff string of S by Def30;
<*l*>^phii is (m+1)-wff; hence thesis;
end;
end;
Lm32: for I being Relation st I in U-InterpretersOf S holds
dom I=OwnSymbolsOf S
proof
set O=OwnSymbolsOf S, II=U-InterpretersOf S; let I be Relation;
assume I in II; then consider f being
Element of Funcs(O,PFuncs(U*,U\/BOOLEAN)) such that
A1: I=f & f is (S,U)-interpreter-like; reconsider ff=f as
Function of O, PFuncs(U*,U\/BOOLEAN); thus dom I=O by A1, FUNCT_2:def 1;
end;
registration
let S,U;
cluster -> (OwnSymbolsOf S)-defined for Element of U-InterpretersOf S;
coherence
proof
set O=OwnSymbolsOf S, II=U-InterpretersOf S; let I be Element of II;
dom I c= O by Lm32; hence thesis by RELAT_1:def 18;
end;
end;
registration
let S,U;
cluster (OwnSymbolsOf S)-defined for Element of U-InterpretersOf S;
existence
proof
set II=U-InterpretersOf S; take the Element of II; thus thesis;
end;
end;
registration
let S,U;
cluster -> total for
(OwnSymbolsOf S)-defined (Element of U-InterpretersOf S);
coherence
proof
set O=OwnSymbolsOf S, II=U-InterpretersOf S;
let I be O-defined Element of II;
dom I=O by Lm32; hence thesis by PARTFUN1:def 2;
end;
end;
definition
let S, U; let I be Element of U-InterpretersOf S;
let x be literal Element of S, u be Element of U;
redefine func (x,u) ReassignIn I -> Element of U-InterpretersOf S; :: redefines ReassignIn (FOMODEL2, definition)
coherence
proof
set II=U-InterpretersOf S, IT=(x,u) ReassignIn I, O=OwnSymbolsOf S,
new={{}} --> u, g=x .--> new;
reconsider xx=x as own Element of S;
{x} c= O & dom g={x} by FOMODEL1:def 19, ZFMISC_1:31; then
reconsider G=dom g as Subset of O;
dom IT=dom I \/ G by FUNCT_4:def 1 .= O \/ G by PARTFUN1:def 2 .= O;
then reconsider ITT=IT as O-defined Function by RELAT_1:def 18;
ITT|O = ITT; hence thesis by Th2;
end;
end;
Lm33: 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
set II=U-InterpretersOf S; let I be Element of II; set g=(I,m)-TruthEval,
f=(S,U)-TruthEval m, Phim=S-formulasOfMaxDepth m;
f is Element of Funcs([:II, Phim:],BOOLEAN) by Th8; then reconsider ff=f as
Function of [:II, Phim:], BOOLEAN;
A1: dom ff=[:II, Phim:] by FUNCT_2:def 1; assume w is m-wff; then
w in Phim; then
[I,w] in dom f & g=(curry f).I by A1, ZFMISC_1:87; then
w in dom g & g.w=f.(I,w) by FUNCT_5:20; hence thesis;
end;
reserve I for Element of U-InterpretersOf S;
Lm34: 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 st f.((l,u) ReassignIn I, phi1)=TRUE)
proof
set II=U-InterpretersOf S, SS=AllSymbolsOf S, N=TheNorSymbOf S,
psi=<*l*>^phi1, FF=AllFormulasOf S, Phim=S-formulasOfMaxDepth m;
let f be PartFunc of [: II, SS*\{{}} :], BOOLEAN; assume
dom f=[:II, Phim:] & phi1 is m-wff;
set LH=f-ExFunctor(I,psi); reconsider psii=psi, phi11=phi1
as FinSequence of SS by FOMODEL0:26;
A1: (<*l*>^phi11)/^1=phi11 by FINSEQ_6:45;
hereby
assume LH=1; then consider
u being Element of U, v being literal Element of S such that
A2: (psi.1=v & f.((v,u) ReassignIn I, psi/^1)=TRUE) by Def15; take u;
thus f.((l,u) ReassignIn I, phi1)=TRUE by A2, A1, FINSEQ_1:41;
end;
given u such that
A3: f.((l,u) ReassignIn I, phi1)=TRUE;
ex u1, l1 st psii.1=l1 & f.((l1,u1) ReassignIn I, psii/^1)=TRUE
by A1, FINSEQ_1:41, A3; hence thesis by Def15;
end;
Lm35: I-TruthEval (<*l*>^phi) = TRUE iff
(ex u st ((l,u) ReassignIn I)-TruthEval phi=1)
proof
set Nor=TheNorSymbOf S, II=U-InterpretersOf S, SS= AllSymbolsOf S, D =
PFuncs([:II,SS*\{{}}:],BOOLEAN), m=Depth phi, M=m+1, L
= LettersOf S;
reconsider phii=phi as m-wff string of S by Def30;
reconsider psi=<*l*>^phi as M-wff string of S;
deffunc E(Element of D)=ExIterator($1);
deffunc N(Element of D)=NorIterator($1); set F=(S,U)-TruthEval;
reconsider mm=m, MM=M as Element of NAT by ORDINAL1:def 12;
set Phim=S-formulasOfMaxDepth m, PhiM=S-formulasOfMaxDepth M;
reconsider phiii=phii as Element of Phim by Def23;
reconsider ll=l as Element of L by FOMODEL1:def 14;
set FM=(S,U)-TruthEval M, Fm=(S,U)-TruthEval m, mNF=m-NorFormulasOf S,
mEF=m-ExFormulasOf S;
psi=<*ll*>^phiii; then
psi in mEF & not psi in mNF; then
[I,psi] in [:II,mEF:] & not [I,psi] in [:II, mNF:] by ZFMISC_1:87; then
A1: [I,psi] in dom ExIterator Fm & not [I,psi] in dom NorIterator Fm
by Lm18, Lm19;
A2: F.MM = ExIterator(F.mm)+*NorIterator(F.mm)+*F.mm by Def19;
Fm is Element of Funcs([:II, Phim:], BOOLEAN) by Th8; then
reconsider Fmm=Fm as Function of [:II, Phim:], BOOLEAN;
A3: not [I,psi] in dom (F.mm)
proof
A4: not psi in Phim by Def23;
dom (F.mm)=dom Fmm by Def20 .= [:II,Phim:] by FUNCT_2:def 1;
hence thesis by A4, ZFMISC_1:87;
end;
A5: dom Fmm=[:II, Phim:] by FUNCT_2:def 1;
A6: I-TruthEval psi = ((I,M)-TruthEval).psi by Def25 .=
FM.[I,psi] by Lm33 .= (F.MM).[I,psi] by Def20 .=
(ExIterator(F.mm) +* NorIterator(F.mm)).[I,psi] by A2, A3, FUNCT_4:11 .=
(ExIterator(F.mm) +* NorIterator(Fm)).[I,psi] by Def20 .=
(ExIterator(F.mm)).[I,psi] by FUNCT_4:11, A1 .=
(E(Fm)).(I,psi) by Def20 .=
Fm-ExFunctor(I,psi) by A1, Def16;
A7: (ex u st Fm.((l,u) ReassignIn I, phii)=TRUE) implies
ex u st ((l,u) ReassignIn I)-TruthEval phii=TRUE
proof
given u such that A8: Fm.((l,u) ReassignIn I, phii)=TRUE; take u;
set J=(l,u) ReassignIn I;
(J,m)-TruthEval.phii=TRUE by A8, Lm33; hence thesis by Def25;
end;
(ex u st ((l,u) ReassignIn I)-TruthEval phii=TRUE) implies
(ex u st Fm.((l,u) ReassignIn I, phii)=TRUE)
proof
given u such that A9: ((l,u) ReassignIn I)-TruthEval phii=TRUE; take u;
set J=(l,u) ReassignIn I;
(J,m)-TruthEval.phii=TRUE by A9, Def25; hence thesis by Lm33;
end;
hence thesis by A6, A5, Lm34, A7;
end;
Lm36: 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
set II=U-InterpretersOf S, SS=AllSymbolsOf S, N=TheNorSymbOf S,
phi2=w2, psi=<*N*>^phi1^phi2, FF=AllFormulasOf S, Phim=S-formulasOfMaxDepth m;
let f be PartFunc of [: II, SS*\{{}} :], BOOLEAN; assume
A1: dom f=[:II, Phim:] & phi1 is m-wff;
set LH=f-NorFunctor(I,psi), RH1=f.(I,phi1), RH2=f.(I,phi2);
hereby
assume LH=1; then consider w, w1 such that
A2: [I,w] in dom f & f.(I,w)=FALSE & f.(I,w1)=FALSE & psi=<*N*>^w^w1
by Def17;
A3: w in Phim & phi1 in Phim by A1, A2, ZFMISC_1:87;
<*N*>^(w^w1)=psi by A2, FINSEQ_1:32 .= <*N*>^(phi1^phi2) by FINSEQ_1:32;
then w^w1=phi1^phi2 by FINSEQ_1:33;
hence RH1=0 & RH2=0 by A2, FOMODEL0:def 19, A3;
end;
assume RH1=0 & RH2=0; hence LH=1 by A1, ZFMISC_1:87, Def17;
end;
Lm37: I-TruthEval (<*TheNorSymbOf S*>^phi1^phi2) = TRUE iff
(I-TruthEval phi1 = FALSE & I-TruthEval phi2 = FALSE)
proof
set Nor=TheNorSymbOf S, II=U-InterpretersOf S, SS= AllSymbolsOf S,
B=BOOLEAN, D=PFuncs([:II,SS*\{{}}:],BOOLEAN), m1=Depth phi1, m2=Depth phi2;
deffunc E(Element of D)=ExIterator($1);
deffunc N(Element of D)=NorIterator($1); set F=(S,U)-TruthEval;
reconsider m=max(m1,m2) as Nat by TARSKI:1;
set M=m+1;
reconsider d1=m-m1, d2=m-m2 as Nat;
phi1 is (m1+0*d1)-wff & phi2 is (m2+0*d2)-wff by Def30; then
phi1 is (m1+d1)-wff & phi2 is (m2+d2)-wff;
then reconsider phi11=phi1, phi22=phi2 as m-wff string of S;
reconsider phi=<*Nor*>^phi11^phi22 as (m+1)-wff
string of S; reconsider mm=m, MM=M as Element of NAT by ORDINAL1:def 12;
set Phim=S-formulasOfMaxDepth m, PhiM=S-formulasOfMaxDepth M;
set FM=(S,U)-TruthEval M, Fm=(S,U)-TruthEval m, mNF=m-NorFormulasOf S;
A1: I-TruthEval phi1 = ((I,m)-TruthEval).phi11 by Def25
.= Fm.(I,phi1) by Lm33;
A2: I-TruthEval phi22 = ((I,m)-TruthEval).phi22 by Def25
.= Fm.(I,phi2) by Lm33;
reconsider phi111=phi11, phi222=phi22 as Element of Phim by Def23;
phi=<*Nor*>^phi111^phi222; then phi in mNF; then
[I,phi] in [:II, mNF:] by ZFMISC_1:87; then
A3: [I,phi] in dom NorIterator Fm by Lm18;
A4: F.MM = ExIterator(F.mm)+*NorIterator(F.mm)+*F.mm by Def19;
Fm is Element of Funcs([:II, Phim:], BOOLEAN) by Th8; then
reconsider Fmm=Fm as Function of [:II, Phim:], BOOLEAN;
A5: not [I,phi] in dom (F.mm)
proof
A6: not phi in Phim by Def23;
dom (F.mm)=dom Fmm by Def20 .= [:II,Phim:] by FUNCT_2:def 1;
hence thesis by A6, ZFMISC_1:87;
end;
A7: dom Fmm=[:II, Phim:] by FUNCT_2:def 1;
I-TruthEval phi = ((I,M)-TruthEval).phi by Def25 .=
FM.[I,phi] by Lm33 .= (F.MM).[I,phi] by Def20 .=
(ExIterator(F.mm) +* NorIterator(F.mm)).[I,phi] by A4, A5, FUNCT_4:11 .=
(ExIterator(F.mm) +* NorIterator(Fm)).[I,phi] by Def20 .=
(N(Fm)).(I,phi) by FUNCT_4:13, A3 .= Fm-NorFunctor(I,phi) by A3, Def18;
hence thesis by A7, Lm36, A2, A1;
end;
definition
let S, w;
func xnot w -> string of S equals <*TheNorSymbOf S*>^w^w;
coherence;
end;
registration
let S, m; let phi be m-wff string of S;
cluster xnot phi -> (m+1)-wff for string of S;
coherence;
end;
registration
let S, phi;
cluster xnot phi -> wff for string of S;
coherence;
end;
registration
let S;
cluster TheEqSymbOf S -> non own for Element of S;
coherence
proof
set E=TheEqSymbOf S, R=RelSymbolsOf S, O=OwnSymbolsOf S;
E in {E} by TARSKI:def 1; then E in R\O by FOMODEL1:1; then not E in O by
XBOOLE_0:def 5; hence thesis;
end;
end;
definition
let S,X;
attr X is S-mincover means
for phi holds (phi in X iff not xnot phi in X);
end;
theorem Th17:
Depth(<*TheNorSymbOf S*>^phi1^phi2)=1+max(Depth phi1, Depth phi2) &
Depth (<*l*>^phi1) = Depth phi1 + 1
proof
set N=TheNorSymbOf S, m1=Depth phi1, m2=Depth phi2,
e=<*l*>^phi1, n=<*N*>^phi1^phi2; thus Depth n=1+max(m1,m2) by Lm31;
now
let m; assume C0: e is m-wff; assume m<(m1+1); then m<=m1 by NAT_1:13;
then m-m <= m1-m by XREAL_1:13; then
reconsider k=m1-m as Nat; e is (m+0*k)-wff by C0; then e is (m+k)-wff;
hence contradiction;
end; hence
Depth e=m1+1 by Def30;
end;
theorem (Depth phi=m+1) implies ((phi is exal iff phi in m-ExFormulasOf S)
& (phi is non exal iff phi in m-NorFormulasOf S)) by Lm27, Lm29;
theorem (I-TruthEval (<*l*>^phi) = TRUE iff
(ex u st ((l,u) ReassignIn I)-TruthEval phi=1) ) &
(I-TruthEval (<*TheNorSymbOf S*>^phi1^phi2) = TRUE iff
(I-TruthEval phi1 = FALSE & I-TruthEval phi2 = FALSE)) by Lm35, Lm37;
reserve I for (S,U)-interpreter-like Function;
theorem Th20:
(I,u)-TermEval.(m+1)|(S-termsOfMaxDepth.m) =I-TermEval|(S-termsOfMaxDepth.m)
proof
reconsider mm=m, MM=m+1 as Element of NAT by ORDINAL1:def 12;
set T=S-termsOfMaxDepth, TI=I-TermEval, TII=(I,u)-TermEval, TT=AllTermsOf S;
reconsider IM=TII.MM as Function of TT,U;
reconsider Tm=T.mm, TM=T.MM as Subset of TT by FOMODEL1:2;
set LH=IM|Tm, RH=TI|Tm;
A1: dom LH = Tm & dom RH = Tm by PARTFUN1:def 2;
now
let x be object; assume
A2: x in dom LH; then x in Tm null TT; then
reconsider tt=x as Element of TT; reconsider ttt=x as Element of Tm by A2;
LH.ttt\+\IM.ttt={} & RH.ttt\+\TI.ttt={}; then
A3: LH.x=IM.tt & RH.x=TI.x by FOMODEL0:29; then LH.x = I-TermEval tt
by A2,Def8 .= RH.x by A3, Def9;
hence LH.x=RH.x;
end;
hence thesis by A1, FUNCT_1:2;
end;
theorem Th21:
I-TermEval.t = (I.(S-firstChar.t)).((I-TermEval)*(SubTerms t))
proof
set u=the Element of U, TI=I-TermEval, TII=(I,u)-TermEval, TT=AllTermsOf S,
F=S-firstChar, s=F.t, m=Depth t, T=S-termsOfMaxDepth, ST=SubTerms t;
reconsider mm=m, MM=m+1 as Element of NAT by ORDINAL1:def 12;
A1: t is (m+0*1)-termal by FOMODEL1:def 40;
reconsider tm=t as m-termal string of S by FOMODEL1:def 40;
reconsider tM=t as (mm+1)-termal string of S by A1;
reconsider Tm=T.mm, TM=T.MM as Subset of TT by FOMODEL1:2;
reconsider ttt=tm as Element of T.mm by FOMODEL1:def 33;
reconsider tt=t as Element of TT by FOMODEL1:def 32; set V=I-TermEval tt;
reconsider IM=TII.MM as Function of TT, U;
SubTerms tM is Tm-valued; then
A2: dom (TI|Tm)=Tm & dom (IM|Tm)=Tm & rng ST c= Tm
by RELAT_1:def 19, PARTFUN1:def 2;
TI.t = V by Def9 .= (TII.MM).ttt by Def8 .=
(TII.(m+1+1)).tm by Lm6 .= (I.s).((TII.MM)*ST) by Th3 .=
(I.s).(((TII.MM)|Tm)*ST) by RELAT_1:165, A2 .= (I.s).((TI|Tm)*ST) by Th20
.= (I.s).(TI*ST) by A2, RELAT_1:165; hence thesis;
end;
definition
let S,phi;
set F=S-firstChar,d=Depth phi, s=F.phi, L=LettersOf S, N=TheNorSymbOf S,
FF=AllFormulasOf S, SS=AllSymbolsOf S;
defpred P[set] means ex phi1, p st p is SS-valued &
$1=[phi1,p] & phi=<*S-firstChar.phi*>^phi1^p;
func SubWffsOf phi -> set
means :Def34: ex phi1, p st p is (AllSymbolsOf S)-valued
& it=[phi1,p] & phi=<*S-firstChar.phi*>^phi1^p if phi is non 0wff
otherwise it=[phi,{}];
existence
proof
thus phi is non 0wff implies ex IT being set st P[IT]
proof
assume phi is non 0wff; then consider m such that
A1: d=m+1 by NAT_1:6;
per cases;
suppose phi is exal; then
phi in m-ExFormulasOf S by A1, Lm27; then consider ll being
Element of L, phi0 being Element of S-formulasOfMaxDepth m such that
A2: phi=<*ll*>^phi0;
A3: ll=phi.1 by A2, FINSEQ_1:41 .= s by FOMODEL0:6;
reconsider l=ll as literal Element of S;
reconsider phi1=phi0 as m-wff string of S by Def23;
reconsider IT=[phi1,{}] as set;
take IT;
take phi1;
take p={} null SS; thus p is SS-valued;
thus IT=[phi1,p]; thus thesis by A2, A3;
end;
suppose not phi is exal; then
phi in m-NorFormulasOf S by A1, Lm29; then consider phi0, psi0
being Element of S-formulasOfMaxDepth m such that
A4: phi=<*N*>^phi0^psi0;
A5: s = phi.1 by FOMODEL0:6 .= (<*N*>^(phi0^psi0)).1 by A4, FINSEQ_1:32 .= N
by FINSEQ_1:41; reconsider phi1=phi0, psi1=psi0 as m-wff string of S
by Def23; take IT=[phi1,psi0]; take phi1; take p=psi1;
thus p is SS-valued; thus IT=[phi1,p]; thus phi=<*s*>^phi1^p by A4, A5;
end;
end;
assume phi is 0wff; take IT=[phi,{}]; thus thesis;
end;
uniqueness
proof
let IT1, IT2 be set;
thus phi is non 0wff & P[IT1] & P[IT2] implies IT1=IT2
proof
assume phi is non 0wff; then
reconsider phi as non 0wff string of S;assume
A6: P[IT1] & P[IT2];
consider phi1,p1 such that
A7: p1 is SS-valued & IT1=[phi1,p1] & phi=<*s*>^phi1^p1 by A6;
consider phi2,p2 such that
A8: p2 is SS-valued & IT2=[phi2,p2] & phi=<*s*>^phi2^p2 by A6;
reconsider q1=p1, q2=p2 as SS-valued FinSequence by A7, A8; <*s*>^(phi1^p1)
= phi by A7, FINSEQ_1:32 .= <*s*>^(phi2^p2) by FINSEQ_1:32, A8; then
phi1^q1=phi2^q2 & phi1 in FF & phi2 in FF by Th16, FINSEQ_1:33;
then phi1=phi2 & q1=q2 by FOMODEL0:def 19; hence thesis by A7,A8;
end;
thus phi is 0wff & IT1=[phi,{}] & IT2=[phi,{}] implies IT1=IT2;
end;
consistency;
end;
definition
let S,phi; set IT=SubWffsOf phi, SS=AllSymbolsOf S, F=S-firstChar;
func head phi -> wff string of S equals (SubWffsOf phi)`1;
coherence
proof
per cases;
suppose phi is non 0wff; then consider phi1, p such that
A1: p is SS-valued & IT=[phi1,p] & phi=<*F.phi*>^phi1^p by Def34;
IT`1 \+\ phi1={} by A1; hence thesis by FOMODEL0:29;
end;
suppose phi is 0wff; then IT=[phi,{}] by Def34; then IT`1 \+\ phi={};
hence thesis by FOMODEL0:29;
end;
end;
func tail phi -> Element of (AllSymbolsOf S)* equals (SubWffsOf phi)`2;
coherence
proof
per cases;
suppose phi is non 0wff; then consider phi1, p such that
A2: p is SS-valued & IT=[phi1,p] & phi=<*F.phi*>^phi1^p by Def34;
IT`2=p & p is FinSequence of SS
by A2, FOMODEL0:26; hence thesis;
end;
suppose phi is 0wff; then IT=[phi,{}] by Def34; then IT`2 \+\ {}=
{} null SS; then reconsider ITT=IT`2 as SS-valued FinSequence;
ITT is FinSequence of SS by FOMODEL0:26; hence thesis;
end;
end;
end;
registration
let S,m;
cluster (S-formulasOfMaxDepth m) \ (AllFormulasOf S) -> empty for set;
coherence
proof
set Fm=S-formulasOfMaxDepth m, FF=AllFormulasOf S;
now
let x be object; assume x in Fm;
then reconsider phi=x as m-wff string of S
by Def23; phi in FF; hence x in FF;
end; then Fm c= FF; hence thesis;
end;
end;
registration
let S;
cluster (AtomicFormulasOf S) \ (AllFormulasOf S) -> empty for set;
coherence
proof (S-formulasOfMaxDepth 0)\(AllFormulasOf S)={};hence thesis by Lm16;end;
end;
theorem Depth (<*l*>^phi1) > Depth phi1 &
Depth (<*TheNorSymbOf S*>^phi1^phi2) > Depth phi1 &
Depth (<*TheNorSymbOf S*>^phi1^phi2) > Depth phi2 by Lm28, Lm30;
theorem Th23: (not phi is 0wff) implies
(phi=<*x*>^phi2^p2 iff (x=S-firstChar.phi & phi2=head phi & p2=tail phi))
proof
set Phi=SubWffsOf phi, F=S-firstChar, s=F.phi, SS=AllSymbolsOf S; assume
A1: not phi is 0wff; then consider phi1, p such that
A2: p is SS-valued & Phi=[phi1,p] & phi=<*s*>^phi1^p by Def34;
hereby
assume
A4: phi=<*x*>^phi2^p2; then
A5: phi.1 = (<*x*>^(phi2^p2)).1 by FINSEQ_1:32
.= x by FINSEQ_1:41; hence x=s by FOMODEL0:6;
rng p2 c= rng phi & rng phi c= SS
by A4, FINSEQ_1:30, RELAT_1:def 19; then
p2 is SS-valued & [phi2,p2]=[phi2,p2] & phi=<*s*>^phi2^p2
by XBOOLE_1:1, RELAT_1:def 19, A5, FOMODEL0:6, A4; then
Phi=[phi2,p2] by A1, Def34;
hence phi2=head phi & p2=tail phi;
end;
assume x=s & phi2=head phi & p2=tail phi; hence thesis by A2;
end;
registration
let S, m1;
cluster non exal for non 0wff m1-wff string of S;
existence
proof
set phi=the 0-wff string of S, N=TheNorSymbOf S, phi1=<*N*>^phi^phi;
consider m such that
A1: m1=m+1 by NAT_1:6; phi1 is non 0wff (1+0*m)-wff string of S; then
reconsider phi11=phi1 as non 0wff m1-wff string of S by A1;
take phi11; thus thesis;
end;
end;
registration
let S; let phi be exal wff string of S;
cluster tail phi -> empty for set;
coherence
proof
set d=Depth phi, L=LettersOf S, h=head phi, t=tail phi, F=S-firstChar,
FF=AllFormulasOf S, SS=AllSymbolsOf S, s=F.phi;
consider m such that
A1: d=m+1 by NAT_1:6; set Phim=S-formulasOfMaxDepth m;
phi in m-ExFormulasOf S by A1, Lm27; then consider ll being
Element of L, phim being Element of Phim such that
A2: phi=<*ll*>^phim;
reconsider phimm=phim as m-wff string of S by Def23;
phi = <*ll*>^phimm^{} by A2; hence thesis by Th23;
end;
end;
Lm38: (Depth phi=m+1 & not phi is exal) implies
ex phi2 being m-wff string of S st tail phi=phi2
proof
set d=Depth phi, Phim=S-formulasOfMaxDepth m, N=TheNorSymbOf S; assume
d=m+1 & not phi is exal; then phi in m-NorFormulasOf S by Lm29;
then consider phi1, phi2 being Element of Phim such that
A1: phi=<*N*>^phi1^phi2; reconsider
phi11=phi1, phi22=phi2 as m-wff string of S by Def23;
set d1=Depth phi11, d2=Depth phi22; take phi22;
phi=<*N*>^phi11^phi22 by A1; hence phi22=tail phi by Th23; thus thesis;
end;
definition
let S; let phi be non exal non 0wff wff string of S;
redefine func tail phi -> wff string of S; :: redefines tail (FOMODEL2, definition)
coherence
proof
consider m such that
A1: Depth phi=m+1 by NAT_1:6; consider phi2 being m-wff string of S such that
A2: tail phi=phi2 by A1, Lm38; thus thesis by A2;
end;
end;
registration
let S; let phi be non exal non 0wff wff string of S;
cluster tail phi -> wff for string of S;
coherence;
end;
registration
let S, phi0;
identify head phi0 with phi0 null;
compatibility
proof
phi0=[phi0,{}]`1 & SubWffsOf phi0=[phi0,{}]
by Def34; hence thesis;
end;
end;
registration
let S; let phi be non 0wff non exal wff string of S;
cluster S-firstChar.phi \+\ TheNorSymbOf S -> empty for set;
coherence
proof
set F=S-firstChar, N=TheNorSymbOf S, s=F.phi; consider m such that
A1: Depth phi=m+1 by NAT_1:6; phi in m-NorFormulasOf S by A1, Lm29;
then consider phi11,phi22 being Element of S-formulasOfMaxDepth m such that
A2: phi=<*N*>^phi11^phi22; F.phi = phi.1 by FOMODEL0:6 .=
(<*N*>^(phi11^phi22)).1 by A2, FINSEQ_1:32 .= N by FINSEQ_1:41; hence thesis;
end;
end;
Lm39: not phi is 0wff & not phi is exal & phi is (m+1)-wff implies
(head phi is m-wff string of S & tail phi is m-wff string of S)
proof
assume not phi is 0wff & not phi is exal & phi is (m+1)-wff;
then reconsider phii=phi as non 0wff non exal (m+1)-wff string of S;
set N=TheNorSymbOf S, F=S-firstChar, s=F.phii, dh=Depth (head phii),
dt=Depth(tail phii), M=max(dh,dt), d=Depth phii;
reconsider h=head phii as dh-wff string of S by Def30;
reconsider t=tail phii as dt-wff string of S by Def30;
A1: d <= m+1 by Def30; F.phii \+\ N={}; then s=N by FOMODEL0:29; then
phii=<*N*>^h^t by Th23; then
M+1 <= m+1 by A1, Th17; then M+1-1 <= m+1-1 by XREAL_1:8; then
M+(-dh)<=m+(-dh) & M+(-dt)<=m+(-dt) by XREAL_1:6; then
max(dh,dt)-dh<=m-dh & max(dh,dt)-dt<=m-dt; then 0<=m-dh & 0<=m-dt; then
reconsider nh=m-dh, nt=m-dt as Nat;
h is (dh+0*nh)-wff & t is (dt+0*nt)-wff; then
h is (dh+nh)-wff & t is (dt+nt)-wff; hence thesis;
end;
registration
let m,S; let phi be (m+1)-wff string of S;
cluster head phi -> m-wff for string of S;
coherence
proof
set d=Depth phi, F=S-firstChar, s=F.phi, N=TheNorSymbOf S,
dh=Depth (head phi);
reconsider h=head phi as dh-wff string of S by Def30;
A1: d <= m+1 by Def30;
per cases;
suppose phi is 0wff; then reconsider phi0=phi as 0-wff string of S;
phi0 is (0+0*m)-wff; then phi0 null phi0 is (0+m)-wff string of S;
then head phi0 is m-wff; hence thesis;
end;
suppose not phi is 0wff & not phi is exal; then reconsider
phii=phi as non 0wff non exal (m+1)-wff string of S;
head phii is m-wff string of S by Lm39; hence thesis;
end;
suppose not phi is 0wff & phi is exal;
then reconsider phii=phi as non 0wff exal (m+1)-wff string of S;
set t=tail phii; phii=<*s*>^h^t by Th23 .= <*s*>^h; then
dh+1<=m+1 by A1, Th17; then dh<=m by XREAL_1:8; then
dh+(-dh)<=m+(-dh) by XREAL_1:6; then reconsider n=m-dh as Nat;
h is (dh+0*n)-wff; then h is (dh+n)-wff; hence thesis;
end;
end;
end;
registration
let m, S; let phi be (m+1)-wff non exal non 0wff string of S;
cluster tail phi -> m-wff for string of S;
coherence by Lm39;
end;
theorem Th24: for I being Element of U-InterpretersOf S holds
(I,m)-TruthEval in Funcs(S-formulasOfMaxDepth m, BOOLEAN)
proof
set Phim=S-formulasOfMaxDepth m, II=U-InterpretersOf S;
let I be Element of II; reconsider F=curry ((S,U)-TruthEval m) as Function of
II, Funcs(Phim, BOOLEAN) by Lm17; F.I in Funcs(Phim, BOOLEAN); hence thesis;
end;
Lm40: for I being Element of U-InterpretersOf S holds
I-TruthEval phi0=I-AtomicEval phi0
proof
set II=U-InterpretersOf S; let I be Element of II; set LH=I-TruthEval phi0,
RH=I-AtomicEval phi0, f=(S,U)-TruthEval 0, Phi0=S-formulasOfMaxDepth 0,
AF=AtomicFormulasOf S, SS=AllSymbolsOf S;
reconsider phi000=phi0 as Element of Phi0 by Def23;
reconsider phi00=phi000 as Element of AF by Lm16;
reconsider z=0 as Element of NAT;
(I,0)-TruthEval is Element of Funcs(Phi0,BOOLEAN) by Th24; then
reconsider g=(I,0)-TruthEval as Function of Phi0, BOOLEAN;
set F=curry f;
reconsider F=curry f as Function of II, PFuncs(SS*\{{}},BOOLEAN) by Lm11;
dom F=II & dom g=Phi0 by FUNCT_2:def 1; then
I in dom F & g=F.I & phi000 in dom g; then
A1: g.phi0=f.(I,phi0) & [I,phi0] in dom f by FUNCT_5:31;
LH=g.phi0 by Def25 .=
((S,U)-TruthEval.z).[I,phi0] by A1, Def20
.= (S-TruthEval U).(I,phi00) by Def19 .= RH by Def14; hence thesis;
end;
registration
let S, U; let I be Element of U-InterpretersOf S; let phi0;
identify I-TruthEval phi0 with I-AtomicEval phi0;
compatibility by Lm40;
identify I-AtomicEval phi0 with I-TruthEval phi0;
compatibility;
end;
registration
let S;
cluster non literal for ofAtomicFormula Element of S;
existence proof take TheEqSymbOf S; thus thesis; end;
end;
Lm41: for I1, I2 being (S,U)-interpreter-like Function st
I1|X = I2|X holds I1-TermEval|(X*)=I2-TermEval|(X*)
::#to be replaced by FOMODEL3:Lm51
proof
set T=S-termsOfMaxDepth, O=OwnSymbolsOf S, TT=AllTermsOf S,
SS=AllSymbolsOf S, L=LettersOf S, F=S-firstChar, C=S-multiCat;
let I1,I2 be (S,U)-interpreter-like Function; set E1=I1-TermEval,
E2=I2-TermEval, I11=I1|X, I22=I2|X; assume
A1: I11=I22; then
A2: dom E1=TT & dom E2=TT & I11=I22 by FUNCT_2:def 1;
defpred P[Nat] means
I1-TermEval|(X*/\(T.$1)) = I2-TermEval|(X*/\(T.$1));
A3: P[0]
proof
set d=X*/\(T.0);
T.0 c= TT & d c= T.0 by FOMODEL1:2; then reconsider
dd=d as Subset of TT by XBOOLE_1:1;
A4: dom (E1|dd)=d & dom (E2|dd)=d by PARTFUN1:def 2;
now
let x be object; assume
A5: x in dom (E1|d);
reconsider dd as non empty Subset of TT by A5;
reconsider xd=x as Element of dd by A5;
reconsider t=x as 0-termal string of S by A5, A4, FOMODEL1:def 33;
set o=F.t, ST=SubTerms t; reconsider XX=X as non empty set by A5;
reconsider tx=x as non empty Element of XX* by A5, A4;
{tx.1} \ XX = {}; then tx.1 in XX by ZFMISC_1:60; then reconsider oo=o as
Element of XX by FOMODEL0:6; I11.oo \+\ I1.oo={} & I22.oo \+\ I2.oo={} &
E1|dd.xd\+\E1.xd={} & E2|dd.xd\+\E2.xd={}; then
A6: I11.o=I1.o & I22.o=I2.o & E1|d.x=E1.x & E2|d.x=E2.x by FOMODEL0:29;
hence E1|d.x = I1.o.(E1*ST) by Th21
.= I2.o.(E2*ST) by A1, A6 .= E2|d.x by A6, Th21;
end;
hence thesis by A4, FUNCT_1:2;
end;
A7: for n st P[n] holds P[n+1]
proof
let n; set d=X*/\(T.n), D=X*/\(T.(n+1)); reconsider nn=n, NN=n+1 as
Element of NAT by ORDINAL1:def 12; assume
A8: P[n];
D c= T.NN & d c= T.nn & T.nn c= TT & T.NN c= TT by FOMODEL1:2; then
reconsider DD=D, dd=d as Subset of TT by XBOOLE_1:1;
A9: dom (E1|dd) = d & dom(E2|dd)=d & dom (E1|DD)=D & dom (E2|DD)=D
by PARTFUN1:def 2;
now
let x be object; assume
A10: x in dom (E1|D);
reconsider t=x as (nn+1)-termal string of S by A10, A9, FOMODEL1:def 33;
reconsider XX=X as non empty set by A10;
reconsider DD as non empty Subset of TT
by A10; reconsider tx=x as non empty Element of XX* by A10, A9;
reconsider dx=x as Element of DD by A10;
set o=F.t, m=|.ar o.|;
{tx.1} \ XX = {}; then tx.1 in XX by ZFMISC_1:60; then reconsider oo=o as
Element of XX by FOMODEL0:6;
reconsider r=rng t as Subset of X by A10, A9, RELAT_1:def 19; r* c= X*; then
reconsider newords=(rng t)* as non empty Subset of X*;
reconsider ST=SubTerms t as newords-valued m-element FinSequence;
I11.oo \+\ I1.oo = {} & I22.oo \+\ I2.oo={}; then
A11: I11.oo=I1.oo & I22.oo=I2.oo by FOMODEL0:29;
E1|DD.dx \+\ E1.dx ={} & E2|DD.dx \+\ E2.dx={}; then
A12: E1|D.x= E1.x & E2|D.x=E2.x by FOMODEL0:29;
rng ST c= T.nn & rng ST c= X* by RELAT_1:def 19; then
A13: (E1|d)*ST = E1*ST & (E2|d)*ST=E2*ST by XBOOLE_1:19, A9, RELAT_1:165;
then I1.o.((E1|d)*ST) = E1.t by Th21;
hence E1|D.x=E2|D.x by A12, A8, A1, A11, A13, Th21;
end;
hence thesis by A9, FUNCT_1:2;
end;
A14: for m holds P[m] from NAT_1:sch 2(A3, A7);
set f1=E1|(X*), f2=E2|(X*);
A15: dom f1=X*/\TT & dom f2=X*/\TT by RELAT_1:61, A2;
now
let x be object; assume
A16: x in dom f1;
reconsider D=X*/\TT as non empty Subset of TT by A16, RELAT_1:61, A2;
reconsider t=x as termal string of S by A16, A15;
set m=Depth t; reconsider t as m-termal string of S by FOMODEL1:def 40;
A17: t in X* & t in T.m by A16, FOMODEL1:def 33;
reconsider Dm=X*/\(T.m) as non empty set by A17, XBOOLE_0:def 4;
reconsider tt=t as Element of Dm by A17, XBOOLE_0:def 4;
reconsider xx=x as Element of X* by A16; set g1=E1|Dm, g2=E2|Dm;
f1.xx \+\ E1.xx={} &
f2.xx\+\E2.xx={} & g1.tt\+\E1.tt={} & g2.tt\+\E2.tt={};
then f1.x=E1.x & f2.x=E2.x & g1.x=E1.x & g2.x=E2.x by FOMODEL0:29;
hence f1.x = f2.x by A14;
end;
hence thesis by A15, FUNCT_1:2;
end;
theorem
not l2 in rng p implies (l2,u) ReassignIn I-TermEval.p= I-TermEval.p
proof
set tt=p, II=U-InterpretersOf S, I2=(l2,u) ReassignIn I, f2=l2.-->({}.-->u);
tt null {} is ({}\/rng tt)-valued FinSequence; then
tt is FinSequence of (rng tt) by FOMODEL0:26; then
reconsider ttt=tt as Element of (rng tt)*;
I2-TermEval|((rng tt)*).ttt \+\ I2-TermEval.ttt={} &
I-TermEval|((rng tt)*).ttt \+\ I-TermEval.ttt={}; then
A1: I2-TermEval|((rng tt)*).tt=I2-TermEval.tt &
I-TermEval|((rng tt)*).tt=I-TermEval.tt by FOMODEL0:29;
assume not l2 in rng tt; then
{l2} misses rng tt by ZFMISC_1:50; then dom f2 misses rng tt; then I2|(rng tt)=
I|(rng tt) by FUNCT_4:72;
hence thesis by A1, Lm41;
end;
definition
let X,S,s;
attr s is X-occurring means :Def37:
s in SymbolsOf (((AllSymbolsOf S*)\{{}}) /\ X);
end;
definition
let S,s; let X;
attr X is s-containing means
s in SymbolsOf ((AllSymbolsOf S*)\{{}} /\ X);
end;
notation
let X,S,s;
antonym s is X-absent for s is X-occurring;
end;
notation
let S,s,X;
antonym X is s-free for X is s-containing;
end;
registration
let X be finite set; let S;
cluster X-absent for literal Element of S;
existence
proof
set L=LettersOf S, SS=AllSymbolsOf S; reconsider Y=(SS*\{{}})/\X as
FinSequence-membered Subset of X; reconsider Z=SymbolsOf Y as finite set;
reconsider free=L\Z as infinite Subset of L; set ll = the Element of free;
reconsider l=ll as literal Element of S by TARSKI:def 3;
take l; not l in Z by XBOOLE_0:def 5; hence thesis;
end;
end;
Lm42: w is termal implies rng w /\ LettersOf S <> {}
proof
set L=LettersOf S, F=S-firstChar, TT=AllTermsOf S, C=S-multiCat,
SS=AllSymbolsOf S, CC=SS-multiCat, T=S-termsOfMaxDepth;
reconsider TTT=TT as Subset of SS* by XBOOLE_1:1;
defpred P[Nat] means for w st w is $1-termal holds
(rng w) /\ L<>{};
A1: P[0]
proof
let w; assume w is 0-termal; then reconsider t0=w as 0-termal string of S;
reconsider l=F.t0 as literal Element of S;
reconsider ll=l as Element of L by FOMODEL1:def 14; t0 =
<*l*>^(C.(SubTerms t0)) by FOMODEL1:def 37 .= <*l*>^{} .= <*l*>;
then rng t0 /\ L={ll} null L by FINSEQ_1:38; hence thesis;
end;
A2: for k st P[k] holds P[k+1]
proof
let k; reconsider kk=k as Element of NAT by ORDINAL1:def 12; assume
A3: P[k]; let w; assume
w is (k+1)-termal; then reconsider t=w as (k+1)-termal string of S;
per cases;
suppose not t is 0-termal;
then F.t is operational by FOMODEL1:16;
then reconsider n=|.ar (F.t).| as non zero Nat; consider m such that
A4: n=m+1 by NAT_1:6; reconsider mm=m,nn=n as
Element of NAT by ORDINAL1:def 12;
reconsider tt=t as (kk+1)-termal string of S;
reconsider ST=SubTerms t as
(m+1)-element Element of TT* by A4; ST is (m+1+0)-element; then
{ST.(m+1)} \ TT = {}; then reconsider q=ST.(m+1) as Element of TTT by
ZFMISC_1:60; q is Element of SS* by TARSKI:def 3; then
reconsider qq=q as SS-valued FinSequence;
reconsider p=ST|(Seg m) as TTT-valued FinSequence;
ST|(Seg m)^<*ST.(m+1)*> \+\ ST={}; then
A5: ST=p^<*qq*> by FOMODEL0:29;
A6: C.ST=(C.p)^qq by A5, FOMODEL0:33;
t = <*F.t*>^((C.p)^qq) by FOMODEL1:def 37, A6; then
rng t = rng <*F.t*> \/ rng (C.p^qq) by FINSEQ_1:31 .=
{F.t} \/ rng (C.p^qq) by FINSEQ_1:38 .=
{F.t} \/ (rng (C.p) \/ rng qq) by FINSEQ_1:31 .=
rng qq \/ ({F.t} \/ rng (C.p))
by XBOOLE_1:4; then rng qq null ({F.t}\/rng(C.p)) c= rng t; then
A7: rng q /\ L c= rng t /\ L by XBOOLE_1:26;
SubTerms tt is (T.kk)-valued; then reconsider STT=ST as (T.kk)-valued
(m+1+0)-element FinSequence;
{STT.(m+1)} \ (T.kk) = {}; then reconsider qqq=q as Element of T.kk
by ZFMISC_1:60; reconsider tq=qqq as k-termal string of S
by FOMODEL1:def 33; (rng tq) /\ L <> {} by A3; hence thesis by A7;
end;
suppose t is 0-termal; hence thesis by A1;
end;
end;
A8: for m holds P[m] from NAT_1:sch 2(A1, A2);
assume w is termal; then reconsider t=w as termal string of S;
t is (Depth t)-termal by FOMODEL1:def 40; hence thesis by A8;
end;
registration
let S,t;
cluster rng t /\ LettersOf S -> non empty for set;
coherence by Lm42;
end;
Lm43: w is wff implies rng w /\ LettersOf S <> {}
proof
set L=LettersOf S, F=S-firstChar, TT=AllTermsOf S, C=S-multiCat,
SS=AllSymbolsOf S, CC=SS-multiCat, T=S-termsOfMaxDepth;
reconsider TTT=TT as Subset of SS* by XBOOLE_1:1;
defpred P[Nat] means for w st w is $1-wff holds rng w /\ L <> {};
A1: P[0]
proof
let w; assume w is 0-wff; then reconsider phi0=w as 0wff string of S;
reconsider r=F.phi0 as relational Element of S;
reconsider n=|.ar r.| as non zero Nat; consider m such that
A2: n=m+1 by NAT_1:6;
reconsider ST=SubTerms phi0 as (m+1+0)-element Element of TT* by A2;
reconsider p=ST|(Seg m) as SS*-valued FinSequence;
{ST.(m+1)}\TT={}; then reconsider q=ST.(m+1) as Element of TT by ZFMISC_1:60;
reconsider t=q as termal string of S;
ST|(Seg m) ^ <*q*> \+\ ST = {}; then
A3: ST=ST|(Seg m) ^ <*q*> by FOMODEL0:29;
reconsider qq=q as SS-valued FinSequence;
phi0=<*r*>^(C.ST) by FOMODEL1:def 38 .=
<*r*>^(C.p^qq) by A3, FOMODEL0:33; then rng phi0=rng <*r*> \/ rng (C.p^q)
by FINSEQ_1:31 .= rng <*r*> \/ (rng (C.p) \/ rng q) by FINSEQ_1:31 .=
rng q \/ (rng <*r*> \/ rng (C.p)) by XBOOLE_1:4; then
rng t null (rng <*r*> \/ rng (C.p)) c= rng phi0; then
rng t /\ L c= rng phi0 /\ L by XBOOLE_1:26; hence thesis;
end;
A4: for k st P[k] holds P[k+1]
proof
let k; assume
A5: P[k]; let w; assume w is (k+1)-wff; then reconsider
phi=w as (k+1)-wff string of S;
per cases;
suppose not phi is 0wff; then reconsider phii=phi as non 0wff
wff string of S; reconsider phi1=head phii as k-wff string of S;
phii=<*F.phii*>^phi1^(tail phi) by Th23; then rng phii=
rng (<*F.phii*>^phi1) \/ rng (tail phi) by FINSEQ_1:31 .=
rng phi1 \/ rng <*F.phii*> \/ rng (tail phi) by FINSEQ_1:31 .=
rng phi1 \/ (rng <*F.phii*> \/ rng (tail phi)) by XBOOLE_1:4; then
rng phi1 null (rng <*F.phii*> \/ rng (tail phi)) c= rng phii; then
rng phi1 /\ L c= rng phii /\ L by XBOOLE_1:26;
hence thesis by A5, XBOOLE_1:3;
end;
suppose phi is 0wff; hence thesis by A1;
end;
end;
A6: for m holds P[m] from NAT_1:sch 2(A1, A4);
assume w is wff; then reconsider phi=w as wff string of S;
phi is (Depth phi)-wff by Def30; hence thesis by A6;
end;
registration
let S, phi;
cluster rng phi /\ LettersOf S -> non empty for set;
coherence by Lm43;
end;
registration
let B,S; let A be Subset of B;
cluster A-occurring -> B-occurring for Element of S;
coherence
proof
set SS=AllSymbolsOf S, DA=A/\(SS*\{{}}), DB=B/\(SS*\{{}});
reconsider Y=DB as functional set; reconsider X=DA as Subset of Y by
XBOOLE_1:26;
A1: SymbolsOf X c= SymbolsOf Y by FOMODEL0:46; let s be Element of S;
assume s is A-occurring; then s in SymbolsOf X;
hence s is B-occurring by A1;
end;
end;
registration
let A,B,S;
cluster (A null B)-absent -> (A/\B)-absent for Element of S;
coherence;
end;
registration
let F be finite set; let A,S;
cluster A-absent -> (A\/F)-absent for F-absent Element of S;
coherence
proof
set SS=AllSymbolsOf S, strings=SS*\{{}};
reconsider DA=strings/\A, DF=strings/\F as Subset of strings;
reconsider D=DA\/DF as Subset of strings;
A1: D=strings/\(A\/F) by XBOOLE_1:23;
let s be F-absent Element of S; assume s is A-absent; then
not s in SymbolsOf DA & not s in SymbolsOf DF by Def37; then
not s in (SymbolsOf DA \/ SymbolsOf DF) by XBOOLE_0:def 3; then
not s in SymbolsOf D by FOMODEL0:47; hence thesis by A1;
end;
end;
registration
let S,U; let I be (S,U)-interpreter-like Function;
cluster (OwnSymbolsOf S)\(dom I) -> empty for set;
coherence
proof OwnSymbolsOf S c= dom I by Lm2; hence thesis; end;
end;
theorem ex u st u=I.l.{} & (l,u) ReassignIn I = I
proof
set O=OwnSymbolsOf S; O\(dom I)={}; then
A1: O c= dom I & {{}}={{}} by XBOOLE_1:37;
reconsider lo=l as Element of O by FOMODEL1:def 19; reconsider i=I.l as
Interpreter of l, U;
i is Function of 0-tuples_on U, U & 0-tuples_on U={{}}
by FOMODEL0:10, Def2; then reconsider ii=i as Function of {{}}, U;
reconsider e={} as Element of {{}} by TARSKI:def 1;
reconsider u=ii.e as Element of U; take u; thus u=I.l.{};
set h={}.-->u, H=l.-->h, J=(l,u) ReassignIn I; h= {{}} --> u; then
reconsider hh=h as Function of {{}}, U;
A2: dom H={lo}; then
A3: dom H c= dom I by A1;
for z be Element of {{}} holds ii.z=hh.z; then
A4: ii=hh by FUNCT_2:63;
now
let z be object; assume
A5: z in dom H;
thus H.z=h by FUNCOP_1:7, A5
.= I.z by A4, A5, TARSKI:def 1;
end; then H tolerates I by PARTFUN1:53, A3;
then J=H+*I by FUNCT_4:34 .= I
by A2, A1, XBOOLE_1:1, FUNCT_4:19; hence thesis;
end;
definition
let S,X;
attr X is S-covering means
for phi holds (phi in X or xnot phi in X);
end;
registration
let S;
cluster S-mincover -> S-covering for set;
coherence;
end;
registration
let U, S; let phi be non 0wff non exal wff 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
proof
set h=head phi, t=tail phi, A=I-TruthEval phi, B=I-TruthEval h,
C=I-TruthEval t, RH=B 'nor' C, F=S-firstChar, l=F.phi, N=TheNorSymbOf S;
l\+\N={}; then l=N by FOMODEL0:29; then
A1: phi=<*N*>^h^t by Th23;
RH=A
proof
per cases;
suppose A2: not RH=0;
not B=1 & not C=1 by A2; then B=0 & C=0 by FOMODEL0:39;
hence thesis by A1, Lm37;
end;
suppose A3: RH=0; then (1-B)=0 or (1-C)=0; then
not A=1 by A1, Lm37;
hence thesis by A3, FOMODEL0:39;
end;
end;
hence thesis;
end;
end;
definition
let S;
func ExFormulasOf S -> Subset of (AllSymbolsOf S)*\{{}} equals
{phi where phi is string of S: phi is wff & phi is exal};
coherence
proof
set SS=AllSymbolsOf S, strings=SS*\{{}}; defpred P[string of S] means
$1 is wff & $1 is exal; defpred Q[set] means not contradiction;
deffunc F(set)=$1;
A1: for w holds P[w] implies Q[w]; set IT={F(w): P[w]};
IT c= {F(w): Q[w]} from FRAENKEL:sch 1(A1);
hence thesis by DOMAIN_1:18;
end;
end;
registration
let S;
cluster ExFormulasOf S -> non empty for set;
coherence
proof the exal wff string of S in ExFormulasOf S; hence thesis; end;
end;
registration
let S;
cluster -> exal wff for Element of ExFormulasOf S;
coherence
proof
set EF=ExFormulasOf S; let x be Element of ExFormulasOf S;
x in EF; then consider w such that
A1: x=w & w is wff & w is exal; reconsider phi=x as
exal wff string of S by A1; phi is exal wff string of S; hence thesis;
end;
end;
registration
let S;
cluster -> wff for Element of ExFormulasOf S;
coherence;
end;
registration
let S;
cluster -> exal for Element of ExFormulasOf S;
coherence;
end;
registration
let S;
cluster ExFormulasOf S \ (AllFormulasOf S) -> empty for set;
coherence
proof
set EF=ExFormulasOf S, FF=AllFormulasOf S;
for x being object st x in EF holds x in FF by Th16;
then EF c= FF; hence thesis; end;
end;
registration
let U,S1; let S2 be S1-extending Language;
cluster (S2,U)-interpreter-like -> (S1,U)-interpreter-like for Function;
coherence
proof
set O1=OwnSymbolsOf S1, O2=OwnSymbolsOf S2, a1=the adicity of S1,
a2=the adicity of S2, AS1=AtomicFormulaSymbolsOf S1, E2=TheEqSymbOf S2,
AS2=AtomicFormulaSymbolsOf S2, E1=TheEqSymbOf S1; let I2 be Function;
assume I2 is (S2,U)-interpreter-like; then reconsider
I222=I2 as (S2,U)-interpreter-like Function; reconsider I22=I222 as
Interpreter of S2, U by Def4; O1\O2={}; then
A1: O1 c= O2 & dom a1=AS1 & dom a2=AS2 by XBOOLE_1:37, FUNCT_2:def 1;
a1 c= a2 by FOMODEL1:def 41; then
A2: dom a1 c= dom a2 by RELAT_1:11;
now
let s1 be own Element of S1;
A3: s1 in AS1 by FOMODEL1:def 20; then
A4: s1 in dom a1 by FUNCT_2:def 1;
s1 in AS2 by A3, A2, A1;
then reconsider s2=s1 as ofAtomicFormula Element of S2
by FOMODEL1:def 20; s1<>E1; then s2<>E2 & s2 <> TheNorSymbOf S2
by FOMODEL1:def 41; then s2 is Element of O2 by FOMODEL1:15; then
reconsider s2 as own Element of S2 by FOMODEL1:def 19; reconsider i2=I22.s2
as Interpreter of s2, U by Def3; set m2=ar s2, m1=ar s1;
a2.s2=(a2+*a1).s2 by FUNCT_4:98, FOMODEL1:def 41
.= a1.s2 by FUNCT_4:13,A4; then
A5: m1=m2;
per cases;
suppose
s2 is relational;
then s1 is relational & i2 is Function of |.m1.|-tuples_on U, BOOLEAN
by A5, Def2;
hence I2.s1 is Interpreter of s1, U by Def2;
end;
suppose not s2 is relational; then
i2 is Function of |.m1.|-tuples_on U, U & not s1 is relational
by A5, Def2;
hence I2.s1 is Interpreter of s1, U by Def2;
end;
end; then I2 is Interpreter of S1, U & I222 is Function-yielding
by Def3; hence thesis;
end;
end;
registration
let U, S1; let S2 be S1-extending Language;
let I be (S2,U)-interpreter-like Function;
cluster I|OwnSymbolsOf S1 -> (S1,U)-interpreter-like for Function;
coherence;
end;
registration
let U, S1; let S2 be S1-extending Language, I1 be Element of
U-InterpretersOf S1, I2 be (S2,U)-interpreter-like Function;
cluster I2 +* I1 -> (S2,U)-interpreter-like;
coherence
proof
set IT=I2+*I1, O1=OwnSymbolsOf S1, O2=OwnSymbolsOf S2, a1=the adicity of S1,
a2=the adicity of S2, AS1=AtomicFormulaSymbolsOf S1;
now
let s2 be own Element of S2;
per cases;
suppose s2 in dom I1; then
A1: s2 in O1 & IT.s2 = I1.s2 by FUNCT_4:13;
then reconsider s1=s2 as own Element of S1 by FOMODEL1:def 19;
s1 in AS1 by FOMODEL1:def 20; then
A2: s1 in dom a1 by FUNCT_2:def 1; reconsider i1=I1.s1 as
Interpreter of s1, U; set m2=ar s2, m1=ar s1;
a2.s2=(a2+*a1).s2 by FOMODEL1:def 41, FUNCT_4:98 .= a1.s2 by FUNCT_4:13,A2;
then
A3: m1=m2;
per cases;
suppose s1 is relational; then
s2 is relational & i1 is Function of |.m2.|-tuples_on U, BOOLEAN
by A3, Def2;
hence IT.s2 is Interpreter of s2, U by A1, Def2;
end;
suppose not s1 is relational; then
i1 is Function of |.m2.|-tuples_on U, U & not s2 is relational
by A3, Def2;
hence IT.s2 is Interpreter of s2, U by Def2, A1;
end;
end;
suppose not s2 in dom I1; then IT.s2=I2.s2 by FUNCT_4:11;
hence IT.s2 is Interpreter of s2, U;
end;
end; then IT is Interpreter of S2, U by Def3;
hence thesis;
end;
end;
definition
let U,S; let I be Element of U-InterpretersOf S; let X;
attr X is I-satisfied means :Def41:
for phi st phi in X holds I-TruthEval phi=1;
end;
definition
let S, U, X; let I be Element of U-InterpretersOf S;
attr I is X-satisfying means X is I-satisfied;
end;
registration
let U,S; let e be empty set; let I be Element of U-InterpretersOf S;
cluster e null I -> I-satisfied for set;
coherence;
end;
registration
let X,U,S; let I be Element of U-InterpretersOf S;
cluster I-satisfied for Subset of X;
existence
proof
reconsider e={} null I as Subset of X by XBOOLE_1:2; take e; thus thesis;
end;
end;
registration
let U,S; let I be Element of U-InterpretersOf S;
cluster I-satisfied for set;
existence
proof take the I-satisfied Subset of (the set); thus thesis; end;
end;
registration
let U,S; let I be Element of U-InterpretersOf S;
let X be I-satisfied set;
cluster -> I-satisfied for Subset of X;
coherence
by Def41;
end;
registration
let U,S; let I be Element of U-InterpretersOf S; let X,Y be I-satisfied set;
cluster X\/Y -> I-satisfied;
coherence
proof
now
let phi; assume phi in X\/Y; then phi in X or phi in Y by XBOOLE_0:def 3;
hence I-TruthEval phi=1 by Def41;
end; hence thesis;
end;
end;
registration
let U,S;
let I be Element of U-InterpretersOf S;
let X be I-satisfied set;
cluster I null X -> X-satisfying for Element of U-InterpretersOf S;
coherence;
end;
definition
let S, X;
attr X is S-correct means
for U being non empty set, I being
(Element of U-InterpretersOf S), x being I-satisfied set, phi st
[x,phi] in X holds I-TruthEval phi=1;
end;
registration
let S;
cluster {} null S -> S-correct for set;
coherence;
end;
registration
let S,X;
cluster S-correct for Subset of X;
existence
proof reconsider IT={} null S as Subset of X by XBOOLE_1:2; take IT;
thus IT is S-correct;
end;
end;
theorem for I being Element of U-InterpretersOf S holds
I-TruthEval phi=1 iff {phi} is I-satisfied
proof
let I be Element of U-InterpretersOf S;
thus I-TruthEval phi=1 implies {phi} is I-satisfied by TARSKI:def 1;
assume {phi} is I-satisfied; then reconsider X={phi} as I-satisfied set;
phi in X by TARSKI:def 1; hence I-TruthEval phi=1 by Def41;
end;
theorem s is {w}-occurring iff s in rng w by FOMODEL0:45;
registration
let U, S; let phi1, phi2; 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
proof
set F=S-firstChar, N=TheNorSymbOf S, phi=<*N*>^phi1^phi2,
A=I-TruthEval phi, A1=I-TruthEval phi1, A2=I-TruthEval phi2,
h=head phi, t=tail phi, H=I-TruthEval h, T=I-TruthEval t;
phi1=h & phi2=t by Th23;
hence thesis;
end;
end;
registration
let S, phi, U; let I be Element of U-InterpretersOf S;
cluster I-TruthEval xnot phi \+\ ('not' (I-TruthEval phi)) -> empty for set;
coherence
proof
set N=TheNorSymbOf S, v1=I-TruthEval phi, psi=xnot phi;
I-TruthEval (psi) \+\ (v1 'nor' v1)={}; hence thesis;
end;
end;
definition
let X, S, phi;
attr phi is X-implied means
for U being non empty set, I being Element of U-InterpretersOf S st
X is I-satisfied holds I-TruthEval phi=1;
end;
registration
let S,l,phi;
cluster head (<*l*>^phi) \+\ phi -> empty;
coherence
proof
set Phi=<*l*>^phi;
Phi=<*l*>^phi null {} .= <*l*>^phi^{}; then phi=head Phi by Th23;
hence thesis;
end;
end;