:: Equivalences of Inconsistency and {H}enkin Models
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-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 NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, FINSEQ_1, XBOOLE_0,
FINSET_1, FUNCT_1, ORDINAL1, RELAT_1, ARYTM_3, TARSKI, WELLORD2,
WELLORD1, CARD_1, NAT_1, CQC_THE1, ORDINAL4, XBOOLEAN, CALCUL_1,
CALCUL_2, ARYTM_1, INT_1, XXREAL_0, FUNCT_2, ZFMISC_1, VALUAT_1,
ZF_MODEL, MARGREL1, REALSET1, MCART_1, HENMODEL, NUMBER09;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, CALCUL_1, RELAT_1,
FUNCT_1, ORDINAL1, XCMPLX_0, XXREAL_0, INT_1, NAT_1, FINSEQ_1, QC_LANG1,
CQC_LANG, CQC_THE1, VALUAT_1, FINSET_1, RELSET_1, FUNCT_2, CARD_1,
MARGREL1, CQC_SIM1, DOMAIN_1, XTUPLE_0, MCART_1, NUMBERS, FINSEQ_3,
CALCUL_2, WELLORD1, WELLORD2;
constructors SETFAM_1, WELLORD1, WELLORD2, DOMAIN_1, XXREAL_0, NAT_1, INT_1,
FINSEQ_3, CQC_SIM1, SUBSTUT2, CALCUL_1, CALCUL_2, RELSET_1, XTUPLE_0,
NUMBERS;
registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0,
XREAL_0, INT_1, FINSEQ_1, QC_LANG1, CQC_LANG, FINSEQ_2, CARD_1, XTUPLE_0,
FUNCT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities XBOOLE_0, FINSEQ_2;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, FINSEQ_1, FINSEQ_3, FUNCT_1, VALUAT_1, XBOOLE_0, FINSEQ_2,
ZFMISC_1, RELAT_1, QC_LANG3, XBOOLE_1, NAT_1, MARGREL1, FUNCT_2,
RELSET_1, FINSET_1, CALCUL_1, CQC_THE1, ORDINAL2, AXIOMS, CALCUL_2,
CARD_2, INT_1, ORDINAL1, WELLORD1, WELLORD2, SUBSTUT2, XREAL_1, XXREAL_0,
FUNCOP_1, CARD_1, PARTFUN1;
schemes FUNCT_1, FINSEQ_1, CLASSES1;
begin :: Preliminaries and Equivalences of Inconsistency
reserve Al for QC-alphabet;
reserve a,a1,a2,b,c,d for set,
X,Y,Z for Subset of CQC-WFF(Al),
i,k,m,n for Nat,
p,q for Element of CQC-WFF(Al),
P for QC-pred_symbol of k,Al,
ll for CQC-variable_list of k,Al,
f,f1,f2,g for FinSequence of CQC-WFF(Al);
reserve A for non empty finite Subset of NAT;
theorem Th1:
for f being Function of n,A st ((ex m st succ m = n) & rng f = A
& for n,m st m in dom f & n in dom f & n < m holds f.n in f.m) holds f.(union n
) = union rng f
proof
let f be Function of n,A such that
A1: ex m st succ m = n and
A2: rng f = A and
A3: for n,m st m in dom f & n in dom f & n < m holds f.n in f.m;
thus f.(union n) c= union rng f
proof
let a be object;
consider m such that
A4: n = succ m by A1;
dom f = n by FUNCT_2:def 1;
then
A5: f.m in rng f by A4,FUNCT_1:3,ORDINAL1:6;
assume a in f.(union n);
then a in f.m by A4,ORDINAL2:2;
hence thesis by A5,TARSKI:def 4;
end;
thus union rng f c= f.(union n)
proof
let a be object;
assume a in union rng f;
then consider b such that
A6: a in b and
A7: b in rng f by TARSKI:def 4;
consider c being object such that
A8: c in dom f and
A9: f.c = b by A7,FUNCT_1:def 3;
dom f = n by PARTFUN1:def 2;
then
A10: dom f in NAT by ORDINAL1:def 12;
reconsider i = c as Ordinal by A8;
reconsider i as Element of NAT by A8,ORDINAL1:10,A10;
consider m such that
A11: n = succ m by A1;
i c= m by A8,A11,ORDINAL1:22;
then i c< m or i = m;
then
A12: i in m or i = m by ORDINAL1:11;
A13: dom f = n by FUNCT_2:def 1;
then
A14: m in dom f by A11,ORDINAL1:6;
A15: now
i in dom f by A12,A13,A14,ORDINAL1:10;
then f.i in rng f by FUNCT_1:3;
then reconsider i1 = f.i as Nat by A2;
f.m in rng f by A11,A13,FUNCT_1:3,ORDINAL1:6;
then reconsider i2 = f.m as Nat by A2;
assume f.i in f.m;
then i1 c= i2 by ORDINAL1:def 2;
then a in i2 by A6,A9;
hence thesis by A11,ORDINAL2:2;
end;
i in {k where k is Nat : k < m} or i = m by A12,AXIOMS:4;
then (ex k being Nat st k = i & k < m) or i = m;
hence thesis by A3,A6,A8,A9,A11,A14,A15,ORDINAL2:2;
end;
end;
theorem Th2:
union A in A & for a st a in A holds (a in union A or a = union A )
proof
consider a being Ordinal such that
A1: RelIncl A,RelIncl a are_isomorphic by WELLORD2:8,13;
consider F1 being Function such that
A2: F1 is_isomorphism_of RelIncl A,RelIncl a by A1,WELLORD1:def 8;
A3: dom F1 = field RelIncl A by A2,WELLORD1:def 7;
then dom F1 = A by WELLORD2:def 1;
then consider b being object such that
A4: b in dom F1 by XBOOLE_0:def 1;
rng F1 is finite by A3,FINSET_1:8;
then field RelIncl a is finite by A2,WELLORD1:def 7;
then
A5: a is finite by WELLORD2:def 1;
F1.b in rng F1 by A4,FUNCT_1:3;
then field RelIncl a is non empty by A2,WELLORD1:def 7;
then a is non empty by WELLORD2:def 1;
then
A6: {} in a by ORDINAL1:16,XBOOLE_1:3;
A7: now
assume a is limit_ordinal;
then omega c= a by A6,ORDINAL1:def 11;
hence contradiction by A5;
end;
RelIncl a,RelIncl A are_isomorphic by A1,WELLORD1:40;
then consider F being Function such that
A8: F is_isomorphism_of RelIncl a,RelIncl A by WELLORD1:def 8;
A9: for m,n st m in dom F & n in dom F & n < m holds F.n in F.m
proof
let m,n such that
A10: m in dom F and
A11: n in dom F and
A12: n < m;
F.n in rng F by A11,FUNCT_1:3;
then F.n in field RelIncl A by A8,WELLORD1:def 7;
then
A13: F.n in A by WELLORD2:def 1;
then reconsider b = F.n as Nat;
n in field RelIncl a by A8,A11,WELLORD1:def 7;
then
A14: n in a by WELLORD2:def 1;
F.m in rng F by A10,FUNCT_1:3;
then F.m in field RelIncl A by A8,WELLORD1:def 7;
then
A15: F.m in A by WELLORD2:def 1;
then reconsider c = F.m as Nat;
n in {i where i is Nat: i < m } by A12;
then n in m by AXIOMS:4;
then
A16: n c= m by ORDINAL1:def 2;
m in field RelIncl a by A8,A10,WELLORD1:def 7;
then m in a by WELLORD2:def 1;
then [n,m] in RelIncl a by A14,A16,WELLORD2:def 1;
then [F.n,F.m] in RelIncl A by A8,WELLORD1:def 7;
then
A17: F.n c= F.m by A13,A15,WELLORD2:def 1;
F is one-to-one by A8,WELLORD1:def 7;
then F.n <> F.m by A10,A11,A12;
then F.n c< F.m by A17;
then b in c by ORDINAL1:11;
hence thesis;
end;
reconsider a as Nat by A5;
dom F = field RelIncl a by A8,WELLORD1:def 7;
then
A18: dom F = a by WELLORD2:def 1;
A19: now
let b be Ordinal;
A20: a in NAT by ORDINAL1:def 12;
assume succ b = a;
then b in a by ORDINAL1:6;
hence b in NAT by ORDINAL1:10,A20;
end;
A21: ex m st succ m = a
proof
consider b being Ordinal such that
A22: succ b = a by A7,ORDINAL1:29;
reconsider b as Element of NAT by A19,A22;
take b;
thus thesis by A22;
end;
then consider m such that
A23: succ m = a;
A24: rng F = field RelIncl A by A8,WELLORD1:def 7;
then
A25: rng F = A by WELLORD2:def 1;
then reconsider F as Function of a,A by A18,FUNCT_2:1;
A26: for n,m st m in dom F & n in dom F & n < m holds F.n in F.m by A9;
rng F = A by A24,WELLORD2:def 1;
then
A27: F.(union a) = union rng F by A21,A26,Th1;
A28: union a = m by A23,ORDINAL2:2;
hence union A in A by A25,A18,A23,A27,FUNCT_1:3,ORDINAL1:6;
thus for b st b in A holds (b in union A or b = union A)
proof
let b such that
A29: b in A;
now
A30: m in dom F by A18,A23,ORDINAL1:6;
assume
A31: b <> union A;
consider c being object such that
A32: c in dom F and
A33: F.c = b by A25,A29,FUNCT_1:def 3;
dom F = a by PARTFUN1:def 2;
then
A34: dom F in NAT by ORDINAL1:def 12;
reconsider c as Element of NAT by A32,ORDINAL1:10,A34;
c in m or c = m by A23,A32,ORDINAL1:8;
then c in {k where k is Nat : k < m}
by A25,A23,A27,A31,A33,AXIOMS:4,ORDINAL2:2;
then ex k being Nat st k = c & k < m;
hence thesis by A9,A25,A27,A28,A32,A33,A30;
end;
hence thesis;
end;
end;
reserve C for non empty set;
theorem Th3:
for f being sequence of C, X being finite set st (for n,m st
m in dom f & n in dom f & n < m holds f.n c= f.m) & X c= union rng f holds ex k
st X c= f.k
proof
let f be sequence of C, X be finite set such that
A1: for n,m st m in dom f & n in dom f & n < m holds f.n c= f.m and
A2: X c= union rng f;
A3: now
deffunc F(object) = min* {i : $1 in f.i};
consider g being Function such that
A4: dom g = X &
for a being object st a in X holds g.a = F(a) from FUNCT_1:sch 3;
reconsider A = rng g as finite set by A4,FINSET_1:8;
A5: now
let b be object;
assume b in A;
then consider a being object such that
A6: a in dom g & g.a = b by FUNCT_1:def 3;
b = min* {i : a in f.i} by A4,A6;
hence b in NAT;
end;
assume not X is empty;
then ex c being object st c in dom g by A4;
then reconsider A as non empty finite Subset of NAT by A5,FUNCT_1:3
,TARSKI:def 3;
union A in A by Th2;
then reconsider a = union A as Nat;
take a;
thus X c= f.a
proof
let b be object;
assume
A7: b in X;
then consider c such that
A8: b in c and
A9: c in rng f by A2,TARSKI:def 4;
consider d being object such that
A10: d in dom f and
A11: f.d = c by A9,FUNCT_1:def 3;
reconsider d as Nat by A10;
d in {i : b in f.i} by A8,A11;
then reconsider Y = {i : b in f.i} as non empty set;
now
let a be object;
assume a in Y;
then ex i st i = a & b in f.i;
hence a in NAT by ORDINAL1:def 12;
end;
then reconsider Y as non empty Subset of NAT by TARSKI:def 3;
A12: g.b = min* Y by A4,A7;
then reconsider Y9 = g.b as Nat;
Y9 in Y by A12,NAT_1:def 1;
then
A13: ex i st i = g.b & b in f.i;
A14: dom f = NAT by FUNCT_2:def 1;
A15: now
assume Y9 in a;
then Y9 in {k where k is Nat : k < a} by AXIOMS:4;
then consider k being Nat such that
A16: k = Y9 & k < a;
A17: a in NAT by ORDINAL1:def 12;
Y9 in NAT by ORDINAL1:def 12;
then f.Y9 c= f.a by A1,A14,A16,A17;
hence thesis by A13;
end;
Y9 in A by A4,A7,FUNCT_1:3;
hence thesis by A13,A15,Th2;
end;
end;
now
assume
A18: X is empty;
take k = 0;
{} c= f.k;
hence thesis by A18;
end;
hence thesis by A3;
end;
definition
let Al;
let X,p;
pred X |- p means
ex f st rng f c= X & |- f^<*p*>;
end;
definition
let Al;
let X;
attr X is Consistent means
for p holds not (X |- p & X |- 'not' p);
end;
notation
let Al;
let X;
antonym X is Inconsistent for X is Consistent;
end;
definition
let Al;
let f be FinSequence of CQC-WFF(Al);
attr f is Consistent means
for p holds not (|- f^<*p*> & |- f^<*'not' p*>);
end;
notation
let Al;
let f be FinSequence of CQC-WFF(Al);
antonym f is Inconsistent for f is Consistent;
end;
theorem Th4:
X is Consistent & rng g c= X implies g is Consistent
proof
assume that
A1: X is Consistent and
A2: rng g c= X;
now
assume g is Inconsistent;
then consider p such that
A3: |- g^<*p*> & |- g^<*'not' p*>;
X |- p & X |- 'not' p by A2,A3;
hence contradiction by A1;
end;
hence thesis;
end;
theorem Th5:
|- f^<*p*> implies |- f^g^<*p*>
proof
A1: Ant(f^<*p*>) = f & Ant(f^g^<*p*>) = f^g by CALCUL_1:5;
Suc(f^g^<*p*>) = p by CALCUL_1:5;
then
A2: Suc(f^<*p*>) = Suc(f^g^<*p*>) by CALCUL_1:5;
assume |- f^<*p*>;
hence thesis by A1,A2,CALCUL_1:8,36;
end;
:: Ebb et al, Chapter IV, Lemma 7.2
theorem Th6:
X is Inconsistent iff for p holds X |- p
proof
thus X is Inconsistent implies for p holds X |- p
proof
assume X is Inconsistent;
then consider q such that
A1: X |- q and
A2: X |- 'not' q;
consider f2 such that
A3: rng f2 c= X and
A4: |- f2^<*'not' q*> by A2;
let p;
consider f1 such that
A5: rng f1 c= X and
A6: |- f1^<*q*> by A1;
take f3 = f1^f2;
A7: rng f3 = rng f1 \/ rng f2 by FINSEQ_1:31;
A8: |- f1^f2^<*'not' q*> by A4,CALCUL_2:20;
|- f1^f2^<*q*> by A6,Th5;
hence thesis by A5,A3,A8,A7,CALCUL_2:25,XBOOLE_1:8;
end;
assume for p holds X |- p;
then X |- VERUM(Al) & X |- 'not' VERUM(Al);
hence thesis;
end;
:: One direction of Ebb et al, Chapter IV, Lemma 7.4
theorem Th7:
X is Inconsistent implies ex Y st Y c= X & Y is finite & Y is Inconsistent
proof
assume X is Inconsistent;
then consider p such that
A1: X |- p and
A2: X |- 'not' p;
consider f1 such that
A3: rng f1 c= X and
A4: |- f1^<*p*> by A1;
consider f2 such that
A5: rng f2 c= X and
A6: |- f2^<*'not' p*> by A2;
reconsider Y = rng(f1^f2) as Subset of CQC-WFF(Al);
take Y;
Y = rng f1 \/ rng f2 by FINSEQ_1:31;
hence Y c= X by A3,A5,XBOOLE_1:8;
|- f1^f2^<*'not' p*> by A6,CALCUL_2:20;
then
A7: Y |- 'not' p;
|- f1^f2^<*p*> by A4,Th5;
then Y |- p;
hence thesis by A7;
end;
Lm1: for f,g be FinSequence holds Seg len(f^g) = Seg len f \/ seq(len f,len g)
proof
let f,g be FinSequence;
thus Seg len(f^g) = dom(f^g) by FINSEQ_1:def 3
.= dom f \/ seq(len f,len g) by CALCUL_2:9
.= Seg len f \/ seq(len f,len g) by FINSEQ_1:def 3;
end;
theorem
X \/ {p} |- q implies ex g st rng g c= X & |- g^<*p*>^<*q*>
proof
assume X \/ {p} |- q;
then consider f such that
A1: rng f c= X \/ {p} and
A2: |- f^<*q*>;
A3: now
set g = f - {p};
reconsider A = f"{p} as finite set;
reconsider B = dom f as finite set;
set n = card A;
set h = g^IdFinS(p,n);
A4: len IdFinS(p,n) = n by CARD_1:def 7;
A c= B by RELAT_1:132;
then A c= Seg len f by FINSEQ_1:def 3;
then
a5: A is included_in_Seg by FINSEQ_1:def 13;
A6: now
let i;
reconsider j = i-len g as Integer;
assume
A7: i in seq(len g,n);
then
A8: 1+len g <= i by CALCUL_2:1;
then
A9: 1 <= j by XREAL_1:19;
i <= n+len g by A7,CALCUL_2:1;
then
A10: j <= n by XREAL_1:20;
0 <= j by A8,XREAL_1:19;
then reconsider j as Element of NAT by INT_1:3;
j in Seg n by A9,A10,FINSEQ_1:1;
hence i-len g in dom Sgm(A) by a5,FINSEQ_3:40;
end;
assume not rng f c= X;
then consider a being object such that
A11: a in rng f and
A12: not a in X;
a in X or a in {p} by A1,A11,XBOOLE_0:def 3;
then a = p by A12,TARSKI:def 1;
then consider i being Nat such that
A13: i in B and
A14: f.i = p by A11,FINSEQ_2:10;
reconsider C = B \ A as finite set;
defpred P[Nat,object] means
($1 in Seg len g implies $2 = Sgm(B \ A).$1) & (
$1 in seq(len g,n) implies $2 = Sgm(A).($1 - len g));
A15: card C = card B - n by CARD_2:44,RELAT_1:132
.= card Seg len f - n by FINSEQ_1:def 3
.= len f - n by FINSEQ_1:57
.= len g by FINSEQ_3:59;
A16: for k be Nat st k in Seg len h ex a being object st P[k,a]
proof
let k be Nat such that
k in Seg len h;
now
assume
A17: k in Seg len g;
take a = Sgm(B\A).k;
Seg len g misses seq(len g,n) by CALCUL_2:8;
hence P[k,a] by A17,XBOOLE_0:3;
end;
hence thesis;
end;
consider F being FinSequence such that
A18: dom F = Seg len h & for k be Nat st k in Seg len h holds P[k,F.k]
from FINSEQ_1:sch 1(A16);
A20: dom Sgm(C) = Seg card C by FINSEQ_3:40;
A21: rng F = B
proof
now
let a be object;
assume a in rng F;
then consider i being Nat such that
A22: i in dom F and
A23: F.i = a by FINSEQ_2:10;
A24: now
assume i in Seg len g;
then a = Sgm(C).i & i in dom Sgm(C) by A18,A15,A22,A23,
FINSEQ_3:40;
then a in rng Sgm(C) by FUNCT_1:3;
then a in C by FINSEQ_1:def 14;
hence a in B;
end;
A25: now
A26: rng Sgm(A) = A by a5,FINSEQ_1:def 14;
A27: A c= B by RELAT_1:132;
assume
A28: i in seq(len g,n);
then a = Sgm(A).(i-len g) by A18,A22,A23;
then a in A by A6,A28,A26,FUNCT_1:3;
hence a in B by A27;
end;
i in Seg len g \/ seq(len g,n) by A4,A18,A22,Lm1;
hence a in B by A24,A25,XBOOLE_0:def 3;
end;
hence rng F c= B;
let a be object such that
A29: a in B;
A30: now
assume not a in A;
then a in C by A29,XBOOLE_0:def 5;
then a in rng Sgm(C) by FINSEQ_1:def 14;
then consider i being Nat such that
A32: i in dom Sgm(C) and
A33: Sgm(C).i = a by FINSEQ_2:10;
A34: 1 <= i by A32,FINSEQ_3:25;
len Sgm(C) = len g by A20,A15,FINSEQ_1:def 3;
then
A35: i <= len g by A32,FINSEQ_3:25;
len g <= len h by CALCUL_1:6;
then i <= len h by A35,XXREAL_0:2;
then
A36: i in Seg len h by A34,FINSEQ_1:1;
i in Seg len g by A34,A35,FINSEQ_1:1;
then a = F.i by A18,A33,A36;
hence thesis by A18,A36,FUNCT_1:3;
end;
now
assume
A37: a in A;
rng Sgm(A) = A by a5,FINSEQ_1:def 14;
then consider i being Nat such that
A38: i in dom Sgm(A) and
A39: Sgm(A).i = a by A37,FINSEQ_2:10;
reconsider i as Nat;
set m = i + len g;
len Sgm(A) = n by a5,FINSEQ_3:39;
then i <= n by A38,FINSEQ_3:25;
then
A40: m <= n+len g by XREAL_1:6;
then m <= len g + len IdFinS(p,n) by CARD_1:def 7;
then
A41: m <= len h by FINSEQ_1:22;
A42: 1 <= i by A38,FINSEQ_3:25;
then 1+len g <= m by XREAL_1:6;
then
A43: m in seq(len g,n) by A40,CALCUL_2:1;
i <= m by NAT_1:11;
then 1 <= m by A42,XXREAL_0:2;
then m in dom h by A41,FINSEQ_3:25;
then
A44: m in Seg len h by FINSEQ_1:def 3;
a = Sgm(A).(m - len g) by A39;
then a = F.m by A18,A43,A44;
hence thesis by A18,A44,FUNCT_1:3;
end;
hence thesis by A30;
end;
A45: len h = len g + len IdFinS(p,n) by FINSEQ_1:22
.= len f - n + len IdFinS(p,n) by FINSEQ_3:59
.= len f - n + n by CARD_1:def 7
.= len f;
then
A46: dom F = B by A18,FINSEQ_1:def 3;
then reconsider F as Relation of B,B by A21,RELSET_1:4;
rng F c= B;
then reconsider F as Function of B,B by A46,FUNCT_2:2;
F is one-to-one
proof
let a1,a2 be object such that
A47: a1 in dom F and
A48: a2 in dom F and
A49: F.a1 = F.a2;
A50: a2 in Seg len g \/ seq(len g,n) by A4,A18,A48,Lm1;
A51: now
assume
A52: a1 in Seg len g;
then
A53: a1 in dom Sgm(C) by A15,FINSEQ_3:40;
F.a1 = Sgm(C).a1 by A18,A47,A52;
then F.a1 in rng Sgm(C) by A53,FUNCT_1:3;
then
A54: F.a1 in C by FINSEQ_1:def 14;
A55: now
assume
A56: a2 in seq(len g,n);
then reconsider i = a2 as Nat;
Sgm(A).(i-len g) in rng Sgm(A) by A6,A56,FUNCT_1:3;
then F.a2 in rng Sgm(A) by A18,A48,A56;
then F.a2 in A by a5,FINSEQ_1:def 14;
hence contradiction by A49,A54,XBOOLE_0:def 5;
end;
now
assume
A57: a2 in Seg len g;
then F.a2 = Sgm(C).a2 by A18,A48;
then
A58: Sgm(C).a1 = Sgm(C).a2 by A18,A47,A49,A52;
A59: Sgm(C) is one-to-one by FINSEQ_3:92;
a2 in dom Sgm(C) by A15,A57,FINSEQ_3:40;
hence thesis by A53,A58,A59;
end;
hence thesis by A50,A55,XBOOLE_0:def 3;
end;
A60: now
assume
A61: a1 in seq(len g,n);
then reconsider i = a1 as Nat;
A62: i-len g in dom Sgm(A) by A6,A61;
A63: now
assume
A64: a2 in seq(len g,n);
then reconsider i1 = a2 as Nat;
F.a2 = Sgm(A).(i1-len g) by A18,A48,A64;
then
A65: Sgm(A).(i1-len g) = Sgm(A).(i-len g) by A18,A47,A49,A61;
A66: Sgm(A) is one-to-one by a5,FINSEQ_3:92;
i1-len g in dom Sgm(A) by A6,A64;
then i1-len g+len g = i-len g+len g by A62,A65,A66;
hence thesis;
end;
Sgm(A).(i-len g) in rng Sgm(A) by A6,A61,FUNCT_1:3;
then F.a1 in rng Sgm(A) by A18,A47,A61;
then
A67: F.a1 in A by a5,FINSEQ_1:def 14;
now
assume a2 in Seg len g;
then F.a2 = Sgm(C).a2 & a2 in dom Sgm(C) by A18,A15,A48,
FINSEQ_3:40;
then F.a2 in rng Sgm(C) by FUNCT_1:3;
then F.a2 in C by FINSEQ_1:def 14;
hence contradiction by A49,A67,XBOOLE_0:def 5;
end;
hence thesis by A50,A63,XBOOLE_0:def 3;
end;
a1 in Seg len g \/ seq(len g,n) by A4,A18,A47,Lm1;
hence thesis by A51,A60,XBOOLE_0:def 3;
end;
then reconsider F as Permutation of dom f by A21,FUNCT_2:57;
consider j being Nat such that
A68: j in dom F and
A69: F.j = i by A21,A13,FINSEQ_2:10;
A70: dom Per(f,F) = B by CALCUL_2:19
.= dom F by A18,A45,FINSEQ_1:def 3
.= dom h by A18,FINSEQ_1:def 3;
A71: now
let k be Nat such that
A72: k in dom h;
A73: k in Seg len h by A72,FINSEQ_1:def 3;
A74: now
A75: k in dom (F*f) by A70,A72,CALCUL_2:def 2;
given i be Nat such that
A76: i in dom IdFinS(p,n) and
A77: k = len g + i;
len IdFinS(p,n) = n by CARD_1:def 7;
then
A78: i <= n by A76,FINSEQ_3:25;
then
A79: k <= n+len g by A77,XREAL_1:6;
A80: 1 <= i by A76,FINSEQ_3:25;
then 1+len g <= k by A77,XREAL_1:6;
then
A81: k in seq(len g,n) by A79,CALCUL_2:1;
then F.k = Sgm(A).(k-len g) by A18,A73;
then F.k in rng Sgm(A) by A6,A81,FUNCT_1:3;
then F.k in A by a5,FINSEQ_1:def 14;
then f.(F.k) in {p} by FUNCT_1:def 7;
then f.(F.k) = p by TARSKI:def 1;
then (F*f).k = p by A75,FUNCT_1:12;
then
A82: Per(f,F).k = p by CALCUL_2:def 2;
i in Seg n by A80,A78,FINSEQ_1:1;
hence Per(f,F).k = IdFinS(p,n).i by A82,FUNCOP_1:7
.= h.k by A76,A77,FINSEQ_1:def 7;
end;
now
assume
A83: k in dom g;
then
A84: k in dom Sgm(C) by A20,A15,FINSEQ_1:def 3;
k in Seg len g by A83,FINSEQ_1:def 3;
then
A85: F.k = Sgm(C).k by A18,A73;
k in dom (F*f) by A70,A72,CALCUL_2:def 2;
then (F*f).k = f.(Sgm(C).k) by A85,FUNCT_1:12;
hence Per(f,F).k = f.(Sgm(C).k) by CALCUL_2:def 2
.= (Sgm(C)*f).k by A84,FUNCT_1:13
.= g.k by FINSEQ_3:def 1
.= h.k by A83,FINSEQ_1:def 7;
end;
hence Per(f,F).k = h.k by A72,A74,FINSEQ_1:25;
end;
then
A86: Per(f,F) = h by A70;
reconsider h as FinSequence of CQC-WFF(Al) by A70,A71,FINSEQ_1:13;
(F*f).j = p by A14,A68,A69,FUNCT_1:13;
then
A87: h.j = p by A86,CALCUL_2:def 2;
A88: now
assume
A89: j in dom g;
then g.j = p by A87,FINSEQ_1:def 7;
then
A90: g.j in {p} by TARSKI:def 1;
A91: rng g = rng f \ {p} by FINSEQ_3:65;
g.j in rng g by A89,FUNCT_1:3;
hence contradiction by A90,A91,XBOOLE_0:def 5;
end;
j in dom f by A68;
then j in dom h by A70,CALCUL_2:19;
then consider k be Nat such that
A92: k in dom IdFinS(p,n) and
j = len g + k by A88,FINSEQ_1:25;
reconsider g as FinSequence of CQC-WFF(Al) by FINSEQ_3:86;
1 <= k & k <= len IdFinS(p,n) by A92,FINSEQ_3:25;
then 1 <= len IdFinS(p,n) by XXREAL_0:2;
then
A93: 1 <= n by CARD_1:def 7;
|- h^<*q*> by A2,A86,CALCUL_2:30;
then
A94: |- g^<*p*>^<*q*> by A93,CALCUL_2:32;
take g;
rng g = rng f \ {p} & rng f \ {p} c= (X \/ {p}) \ {p} by A1,FINSEQ_3:65
,XBOOLE_1:33;
then
A95: rng g c= X \ {p} by XBOOLE_1:40;
X \ {p} c= X by XBOOLE_1:36;
hence thesis by A94,A95,XBOOLE_1:1;
end;
now
assume
A96: rng f c= X;
take f;
|- f^<*p*>^<*q*> by A2,Th5;
hence thesis by A96;
end;
hence thesis by A3;
end;
:: Corresponds to Ebb et al, Chapter IV, Lemma 7.6 (a)
theorem
X |- p iff X \/ {'not' p} is Inconsistent
proof
thus X |- p implies X \/ {'not' p} is Inconsistent
proof
assume X |- p;
then consider f such that
A1: rng f c= X and
A2: |- f^<*p*>;
set f2 = f^<*'not' p*>;
set f1 = f^<*'not' p*>^<*'not' p*>;
A3: Ant(f1) = f^<*'not' p*> by CALCUL_1:5;
1 in Seg 1 by FINSEQ_1:1;
then 1 in dom <*'not' p*> by FINSEQ_1:38;
then
A4: len f+1 in dom (Ant(f1)) by A3,FINSEQ_1:28;
Suc(f1) = 'not' p by CALCUL_1:5;
then (Ant(f1)).(len f+1) = Suc(f1) by A3,FINSEQ_1:42;
then Suc(f1) is_tail_of Ant(f1) by A4,CALCUL_1:def 16;
then
A5: |- f1 by CALCUL_1:33;
A6: 0+1 <= len f2 by CALCUL_1:10;
Ant(f2) = f & Suc(f2) = 'not' p by CALCUL_1:5;
then
A7: rng f2 = rng f \/ {'not' p} by A6,CALCUL_1:3;
|- f^<*'not' p*>^<*p*> by A2,Th5;
then not f^<*'not' p*> is Consistent by A5;
hence thesis by A1,A7,Th4,XBOOLE_1:9;
end;
thus X \/ {'not' p} is Inconsistent implies X |- p
proof
assume X \/ {'not' p} is Inconsistent;
then X \/ {'not' p} |- p by Th6;
then consider f such that
A8: rng f c= X \/ {'not' p} and
A9: |- f^<*p*>;
now
set g = f - {'not' p};
reconsider A = f"{'not' p} as finite set;
reconsider B = dom f as finite set;
set n = card A;
set h = g^IdFinS('not' p,n);
A10: len IdFinS('not' p,n) = n by CARD_1:def 7;
A c= B by RELAT_1:132;
then A c= Seg len f by FINSEQ_1:def 3;
then
a11: A is included_in_Seg by FINSEQ_1:def 13;
A12: now
let i;
reconsider j = i-len g as Integer;
assume
A13: i in seq(len g,n);
then
A14: 1+len g <= i by CALCUL_2:1;
then
A15: 1 <= j by XREAL_1:19;
i <= n+len g by A13,CALCUL_2:1;
then
A16: j <= n by XREAL_1:20;
0 <= j by A14,XREAL_1:19;
then reconsider j as Element of NAT by INT_1:3;
j in Seg n by A15,A16,FINSEQ_1:1;
hence i-len g in dom Sgm(A) by a11,FINSEQ_3:40;
end;
assume not rng f c= X;
then consider a being object such that
A17: a in rng f and
A18: not a in X;
a in X or a in {'not' p} by A8,A17,XBOOLE_0:def 3;
then a = 'not' p by A18,TARSKI:def 1;
then consider i being Nat such that
A19: i in B and
A20: f.i = 'not' p by A17,FINSEQ_2:10;
reconsider C = B \ A as finite set;
defpred P[Nat,object] means
($1 in Seg len g implies $2 = Sgm(B \ A).$1) &
($1 in seq(len g,n) implies $2 = Sgm(A).($1 - len g));
A21: card C = card B - n by CARD_2:44,RELAT_1:132
.= card Seg len f - n by FINSEQ_1:def 3
.= len f - n by FINSEQ_1:57
.= len g by FINSEQ_3:59;
A22: for k be Nat st k in Seg len h ex a being object st P[k,a]
proof
let k be Nat such that
k in Seg len h;
now
assume
A23: k in Seg len g;
take a = Sgm(B\A).k;
Seg len g misses seq(len g,n) by CALCUL_2:8;
hence P[k,a] by A23,XBOOLE_0:3;
end;
hence thesis;
end;
consider F being FinSequence such that
A24: dom F = Seg len h & for k be Nat st k in Seg len h holds P[k,F.
k] from FINSEQ_1:sch 1(A22);
A26: dom Sgm(C) = Seg card C by FINSEQ_3:40;
A27: rng F = B
proof
now
let a be object;
assume a in rng F;
then consider i being Nat such that
A28: i in dom F and
A29: F.i = a by FINSEQ_2:10;
A30: now
assume i in Seg len g;
then a = Sgm(C).i & i in dom Sgm(C) by A24,A21,A28,A29,
FINSEQ_3:40;
then a in rng Sgm(C) by FUNCT_1:3;
then a in C by FINSEQ_1:def 14;
hence a in B;
end;
A31: now
A32: rng Sgm(A) = A by a11,FINSEQ_1:def 14;
A33: A c= B by RELAT_1:132;
assume
A34: i in seq(len g,n);
then a = Sgm(A).(i-len g) by A24,A28,A29;
then a in A by A12,A34,A32,FUNCT_1:3;
hence a in B by A33;
end;
i in Seg len g \/ seq(len g,n) by A10,A24,A28,Lm1;
hence a in B by A30,A31,XBOOLE_0:def 3;
end;
hence rng F c= B;
let a be object such that
A35: a in B;
A36: now
assume not a in A;
then a in C by A35,XBOOLE_0:def 5;
then a in rng Sgm(C) by FINSEQ_1:def 14;
then consider i being Nat such that
A38: i in dom Sgm(C) and
A39: Sgm(C).i = a by FINSEQ_2:10;
A40: 1 <= i by A38,FINSEQ_3:25;
len Sgm(C) = len g by A26,A21,FINSEQ_1:def 3;
then
A41: i <= len g by A38,FINSEQ_3:25;
len g <= len h by CALCUL_1:6;
then i <= len h by A41,XXREAL_0:2;
then
A42: i in Seg len h by A40,FINSEQ_1:1;
i in Seg len g by A40,A41,FINSEQ_1:1;
then a = F.i by A24,A39,A42;
hence thesis by A24,A42,FUNCT_1:3;
end;
now
assume
A43: a in A;
rng Sgm(A) = A by a11,FINSEQ_1:def 14;
then consider i being Nat such that
A44: i in dom Sgm(A) and
A45: Sgm(A).i = a by A43,FINSEQ_2:10;
reconsider i as Nat;
set m = i + len g;
len Sgm(A) = n by a11,FINSEQ_3:39;
then i <= n by A44,FINSEQ_3:25;
then
A46: m <= n+len g by XREAL_1:6;
then m <= len g + len IdFinS('not' p,n) by CARD_1:def 7;
then
A47: m <= len h by FINSEQ_1:22;
A48: 1 <= i by A44,FINSEQ_3:25;
then 1+len g <= m by XREAL_1:6;
then
A49: m in seq(len g,n) by A46,CALCUL_2:1;
i <= m by NAT_1:11;
then 1 <= m by A48,XXREAL_0:2;
then m in dom h by A47,FINSEQ_3:25;
then
A50: m in Seg len h by FINSEQ_1:def 3;
a = Sgm(A).(m - len g) by A45;
then a = F.m by A24,A49,A50;
hence thesis by A24,A50,FUNCT_1:3;
end;
hence thesis by A36;
end;
A51: len h = len g + len IdFinS('not' p,n) by FINSEQ_1:22
.= len f - n + len IdFinS('not' p,n) by FINSEQ_3:59
.= len f - n + n by CARD_1:def 7
.= len f;
then
A52: dom F = B by A24,FINSEQ_1:def 3;
then reconsider F as Relation of B,B by A27,RELSET_1:4;
rng F c= B;
then reconsider F as Function of B,B by A52,FUNCT_2:2;
F is one-to-one
proof
let a1,a2 be object such that
A53: a1 in dom F and
A54: a2 in dom F and
A55: F.a1 = F.a2;
A56: a2 in Seg len g \/ seq(len g,n) by A10,A24,A54,Lm1;
A57: now
assume
A58: a1 in Seg len g;
then
A59: a1 in dom Sgm(C) by A21,FINSEQ_3:40;
F.a1 = Sgm(C).a1 by A24,A53,A58;
then F.a1 in rng Sgm(C) by A59,FUNCT_1:3;
then
A60: F.a1 in C by FINSEQ_1:def 14;
A61: now
assume
A62: a2 in seq(len g,n);
then reconsider i = a2 as Nat;
Sgm(A).(i-len g) in rng Sgm(A) by A12,A62,FUNCT_1:3;
then F.a2 in rng Sgm(A) by A24,A54,A62;
then F.a2 in A by a11,FINSEQ_1:def 14;
hence contradiction by A55,A60,XBOOLE_0:def 5;
end;
now
assume
A63: a2 in Seg len g;
then F.a2 = Sgm(C).a2 by A24,A54;
then
A64: Sgm(C).a1 = Sgm(C).a2 by A24,A53,A55,A58;
A65: Sgm(C) is one-to-one by FINSEQ_3:92;
a2 in dom Sgm(C) by A21,A63,FINSEQ_3:40;
hence thesis by A59,A64,A65;
end;
hence thesis by A56,A61,XBOOLE_0:def 3;
end;
A66: now
assume
A67: a1 in seq(len g,n);
then reconsider i = a1 as Nat;
A68: i-len g in dom Sgm(A) by A12,A67;
A69: now
assume
A70: a2 in seq(len g,n);
then reconsider i1 = a2 as Nat;
F.a2 = Sgm(A).(i1-len g) by A24,A54,A70;
then
A71: Sgm(A).(i1-len g) = Sgm(A).(i-len g) by A24,A53,A55,A67;
A72: Sgm(A) is one-to-one by a11,FINSEQ_3:92;
i1-len g in dom Sgm(A) by A12,A70;
then i1-len g = i-len g by A68,A71,A72;
hence thesis;
end;
Sgm(A).(i-len g) in rng Sgm(A) by A12,A67,FUNCT_1:3;
then F.a1 in rng Sgm(A) by A24,A53,A67;
then
A73: F.a1 in A by a11,FINSEQ_1:def 14;
now
assume a2 in Seg len g;
then
F.a2 = Sgm(C).a2 & a2 in dom Sgm(C) by A24,A21,A54,FINSEQ_3:40;
then F.a2 in rng Sgm(C) by FUNCT_1:3;
then F.a2 in C by FINSEQ_1:def 14;
hence contradiction by A55,A73,XBOOLE_0:def 5;
end;
hence thesis by A56,A69,XBOOLE_0:def 3;
end;
a1 in Seg len g \/ seq(len g,n) by A10,A24,A53,Lm1;
hence thesis by A57,A66,XBOOLE_0:def 3;
end;
then reconsider F as Permutation of dom f by A27,FUNCT_2:57;
consider j being Nat such that
A74: j in dom F and
A75: F.j = i by A27,A19,FINSEQ_2:10;
A76: dom Per(f,F) = B by CALCUL_2:19
.= dom F by A24,A51,FINSEQ_1:def 3
.= dom h by A24,FINSEQ_1:def 3;
A77: now
let k be Nat such that
A78: k in dom h;
A79: k in Seg len h by A78,FINSEQ_1:def 3;
A80: now
A81: k in dom (F*f) by A76,A78,CALCUL_2:def 2;
given i be Nat such that
A82: i in dom IdFinS('not' p,n) and
A83: k = len g + i;
len IdFinS('not' p,n) = n by CARD_1:def 7;
then
A84: i <= n by A82,FINSEQ_3:25;
then
A85: k <= n+len g by A83,XREAL_1:6;
A86: 1 <= i by A82,FINSEQ_3:25;
then 1+len g <= k by A83,XREAL_1:6;
then
A87: k in seq(len g,n) by A85,CALCUL_2:1;
then F.k = Sgm(A).(k-len g) by A24,A79;
then F.k in rng Sgm(A) by A12,A87,FUNCT_1:3;
then F.k in A by a11,FINSEQ_1:def 14;
then f.(F.k) in {'not' p} by FUNCT_1:def 7;
then f.(F.k) = 'not' p by TARSKI:def 1;
then (F*f).k = 'not' p by A81,FUNCT_1:12;
then
A88: Per(f,F).k = 'not' p by CALCUL_2:def 2;
i in Seg n by A86,A84,FINSEQ_1:1;
hence Per(f,F).k = IdFinS('not' p,n).i by A88,FUNCOP_1:7
.= h.k by A82,A83,FINSEQ_1:def 7;
end;
now
assume
A89: k in dom g;
then
A90: k in dom Sgm(C) by A26,A21,FINSEQ_1:def 3;
k in Seg len g by A89,FINSEQ_1:def 3;
then
A91: F.k = Sgm(C).k by A24,A79;
k in dom (F*f) by A76,A78,CALCUL_2:def 2;
then (F*f).k = f.(Sgm(C).k) by A91,FUNCT_1:12;
hence Per(f,F).k = f.(Sgm(C).k) by CALCUL_2:def 2
.= (Sgm(C)*f).k by A90,FUNCT_1:13
.= g.k by FINSEQ_3:def 1
.= h.k by A89,FINSEQ_1:def 7;
end;
hence Per(f,F).k = h.k by A78,A80,FINSEQ_1:25;
end;
then
A92: Per(f,F) = h by A76;
reconsider h as FinSequence of CQC-WFF(Al) by A76,A77,FINSEQ_1:13;
(F*f).j = 'not' p by A20,A74,A75,FUNCT_1:13;
then
A93: h.j = 'not' p by A92,CALCUL_2:def 2;
A94: now
assume
A95: j in dom g;
then g.j = 'not' p by A93,FINSEQ_1:def 7;
then
A96: g.j in {'not' p} by TARSKI:def 1;
A97: rng g = rng f \ {'not' p} by FINSEQ_3:65;
g.j in rng g by A95,FUNCT_1:3;
hence contradiction by A96,A97,XBOOLE_0:def 5;
end;
j in dom f by A74;
then j in dom h by A76,CALCUL_2:19;
then consider k be Nat such that
A98: k in dom IdFinS('not' p,n) and
j = len g + k by A94,FINSEQ_1:25;
reconsider g as FinSequence of CQC-WFF(Al) by FINSEQ_3:86;
1 <= k & k <= len IdFinS('not' p,n) by A98,FINSEQ_3:25;
then 1 <= len IdFinS('not' p,n) by XXREAL_0:2;
then
A99: 1 <= n by CARD_1:def 7;
|- h^<*p*> by A9,A92,CALCUL_2:30;
then
A100: |- g^<*'not' p*>^<*p*> by A99,CALCUL_2:32;
rng g = rng f \ {'not' p} & rng f \ {'not' p} c= (X \/ {'not' p})
\ {'not' p } by A8,FINSEQ_3:65,XBOOLE_1:33;
then
A101: rng g c= X \ {'not' p} by XBOOLE_1:40;
X \ {'not' p} c= X by XBOOLE_1:36;
then
A102: rng g c= X by A101;
|- g^<*p*>^<*p*> by CALCUL_2:21;
then |- g^<*p*> by A100,CALCUL_2:26;
hence thesis by A102;
end;
hence thesis by A9;
end;
end;
:: Similar to Ebb et al, Chapter IV, Lemma 7.6 (a)
theorem
X |- 'not' p iff X \/ {p} is Inconsistent
proof
thus X |- 'not' p implies X \/ {p} is Inconsistent
proof
assume X |- 'not' p;
then consider f such that
A1: rng f c= X and
A2: |- f^<*'not' p*>;
set f2 = f^<*p*>;
set f1 = f^<*p*>^<*p*>;
A3: Ant(f1) = f^<*p*> by CALCUL_1:5;
1 in Seg 1 by FINSEQ_1:1;
then 1 in dom <*p*> by FINSEQ_1:38;
then
A4: len f+1 in dom (Ant(f1)) by A3,FINSEQ_1:28;
Suc(f1) = p by CALCUL_1:5;
then (Ant(f1)).(len f+1) = Suc(f1) by A3,FINSEQ_1:42;
then Suc(f1) is_tail_of Ant(f1) by A4,CALCUL_1:def 16;
then
A5: |- f1 by CALCUL_1:33;
A6: 0+1 <= len f2 by CALCUL_1:10;
Ant(f2) = f & Suc(f2) = p by CALCUL_1:5;
then
A7: rng f2 = rng f \/ {p} by A6,CALCUL_1:3;
|- f^<*p*>^<*'not' p*> by A2,Th5;
then not f^<*p*> is Consistent by A5;
hence thesis by A1,A7,Th4,XBOOLE_1:9;
end;
thus X \/ {p} is Inconsistent implies X |- 'not' p
proof
assume X \/ {p} is Inconsistent;
then X \/ {p} |- 'not' p by Th6;
then consider f such that
A8: rng f c= X \/ {p} and
A9: |- f^<*'not' p*>;
now
set g = f - {p};
reconsider A = f"{p} as finite set;
reconsider B = dom f as finite set;
set n = card A;
set h = g^IdFinS(p,n);
A10: len IdFinS(p,n) = n by CARD_1:def 7;
A c= B by RELAT_1:132;
then A c= Seg len f by FINSEQ_1:def 3;
then
a11: A is included_in_Seg by FINSEQ_1:def 13;
A12: now
let i;
reconsider j = i-len g as Integer;
assume
A13: i in seq(len g,n);
then
A14: 1+len g <= i by CALCUL_2:1;
then
A15: 1 <= j by XREAL_1:19;
i <= n+len g by A13,CALCUL_2:1;
then
A16: j <= n by XREAL_1:20;
0 <= j by A14,XREAL_1:19;
then reconsider j as Element of NAT by INT_1:3;
j in Seg n by A15,A16,FINSEQ_1:1;
hence i-len g in dom Sgm(A) by a11,FINSEQ_3:40;
end;
assume not rng f c= X;
then consider a being object such that
A17: a in rng f and
A18: not a in X;
a in X or a in {p} by A8,A17,XBOOLE_0:def 3;
then a = p by A18,TARSKI:def 1;
then consider i being Nat such that
A19: i in B and
A20: f.i = p by A17,FINSEQ_2:10;
reconsider C = B \ A as finite set;
defpred P[Nat,object] means
($1 in Seg len g implies $2 = Sgm(B \ A).$1) &
($1 in seq(len g,n) implies $2 = Sgm(A).($1 - len g));
A21: card C = card B - n by CARD_2:44,RELAT_1:132
.= card Seg len f - n by FINSEQ_1:def 3
.= len f - n by FINSEQ_1:57
.= len g by FINSEQ_3:59;
A22: for k be Nat st k in Seg len h ex a being object st P[k,a]
proof
let k be Nat such that
k in Seg len h;
now
assume
A23: k in Seg len g;
take a = Sgm(B\A).k;
Seg len g misses seq(len g,n) by CALCUL_2:8;
hence P[k,a] by A23,XBOOLE_0:3;
end;
hence thesis;
end;
consider F being FinSequence such that
A24: dom F = Seg len h & for k be Nat st k in Seg len h holds P[k,F.
k] from FINSEQ_1:sch 1(A22);
A26: dom Sgm(C) = Seg card C by FINSEQ_3:40;
A27: rng F = B
proof
now
let a be object;
assume a in rng F;
then consider i being Nat such that
A28: i in dom F and
A29: F.i = a by FINSEQ_2:10;
A30: now
assume i in Seg len g;
then a = Sgm(C).i & i in dom Sgm(C) by A24,A21,A28,A29,
FINSEQ_3:40;
then a in rng Sgm(C) by FUNCT_1:3;
then a in C by FINSEQ_1:def 14;
hence a in B;
end;
A31: now
A32: rng Sgm(A) = A by a11,FINSEQ_1:def 14;
A33: A c= B by RELAT_1:132;
assume
A34: i in seq(len g,n);
then a = Sgm(A).(i-len g) by A24,A28,A29;
then a in A by A12,A34,A32,FUNCT_1:3;
hence a in B by A33;
end;
i in Seg len g \/ seq(len g,n) by A10,A24,A28,Lm1;
hence a in B by A30,A31,XBOOLE_0:def 3;
end;
hence rng F c= B;
let a be object such that
A35: a in B;
A36: now
assume not a in A;
then a in C by A35,XBOOLE_0:def 5;
then a in rng Sgm(C) by FINSEQ_1:def 14;
then consider i being Nat such that
A38: i in dom Sgm(C) and
A39: Sgm(C).i = a by FINSEQ_2:10;
A40: 1 <= i by A38,FINSEQ_3:25;
len Sgm(C) = len g by A26,A21,FINSEQ_1:def 3;
then
A41: i <= len g by A38,FINSEQ_3:25;
len g <= len h by CALCUL_1:6;
then i <= len h by A41,XXREAL_0:2;
then
A42: i in Seg len h by A40,FINSEQ_1:1;
i in Seg len g by A40,A41,FINSEQ_1:1;
then a = F.i by A24,A39,A42;
hence thesis by A24,A42,FUNCT_1:3;
end;
now
assume
A43: a in A;
rng Sgm(A) = A by a11,FINSEQ_1:def 14;
then consider i being Nat such that
A44: i in dom Sgm(A) and
A45: Sgm(A).i = a by A43,FINSEQ_2:10;
reconsider i as Nat;
set m = i + len g;
len Sgm(A) = n by a11,FINSEQ_3:39;
then i <= n by A44,FINSEQ_3:25;
then
A46: m <= n+len g by XREAL_1:6;
then m <= len g + len IdFinS(p,n) by CARD_1:def 7;
then
A47: m <= len h by FINSEQ_1:22;
A48: 1 <= i by A44,FINSEQ_3:25;
then 1+len g <= m by XREAL_1:6;
then
A49: m in seq(len g,n) by A46,CALCUL_2:1;
i <= m by NAT_1:11;
then 1 <= m by A48,XXREAL_0:2;
then m in dom h by A47,FINSEQ_3:25;
then
A50: m in Seg len h by FINSEQ_1:def 3;
a = Sgm(A).(m - len g) by A45;
then a = F.m by A24,A49,A50;
hence thesis by A24,A50,FUNCT_1:3;
end;
hence thesis by A36;
end;
A51: len h = len g + len IdFinS(p,n) by FINSEQ_1:22
.= len f - n + len IdFinS(p,n) by FINSEQ_3:59
.= len f - n + n by CARD_1:def 7
.= len f;
then
A52: dom F = B by A24,FINSEQ_1:def 3;
then reconsider F as Relation of B,B by A27,RELSET_1:4;
rng F c= B;
then reconsider F as Function of B,B by A52,FUNCT_2:2;
F is one-to-one
proof
let a1,a2 be object such that
A53: a1 in dom F and
A54: a2 in dom F and
A55: F.a1 = F.a2;
A56: a2 in Seg len g \/ seq(len g,n) by A10,A24,A54,Lm1;
A57: now
assume
A58: a1 in Seg len g;
then
A59: a1 in dom Sgm(C) by A21,FINSEQ_3:40;
F.a1 = Sgm(C).a1 by A24,A53,A58;
then F.a1 in rng Sgm(C) by A59,FUNCT_1:3;
then
A60: F.a1 in C by FINSEQ_1:def 14;
A61: now
assume
A62: a2 in seq(len g,n);
then reconsider i = a2 as Nat;
Sgm(A).(i-len g) in rng Sgm(A) by A12,A62,FUNCT_1:3;
then F.a2 in rng Sgm(A) by A24,A54,A62;
then F.a2 in A by a11,FINSEQ_1:def 14;
hence contradiction by A55,A60,XBOOLE_0:def 5;
end;
now
assume
A63: a2 in Seg len g;
then F.a2 = Sgm(C).a2 by A24,A54;
then
A64: Sgm(C).a1 = Sgm(C).a2 by A24,A53,A55,A58;
A65: Sgm(C) is one-to-one by FINSEQ_3:92;
a2 in dom Sgm(C) by A21,A63,FINSEQ_3:40;
hence thesis by A59,A64,A65;
end;
hence thesis by A56,A61,XBOOLE_0:def 3;
end;
A66: now
assume
A67: a1 in seq(len g,n);
then reconsider i = a1 as Nat;
A68: i-len g in dom Sgm(A) by A12,A67;
A69: now
assume
A70: a2 in seq(len g,n);
then reconsider i1 = a2 as Nat;
F.a2 = Sgm(A).(i1-len g) by A24,A54,A70;
then
A71: Sgm(A).(i1-len g) = Sgm(A).(i-len g) by A24,A53,A55,A67;
A72: Sgm(A) is one-to-one by a11,FINSEQ_3:92;
i1-len g in dom Sgm(A) by A12,A70;
then i1-len g+len g = i-len g+len g by A68,A71,A72;
hence thesis;
end;
Sgm(A).(i-len g) in rng Sgm(A) by A12,A67,FUNCT_1:3;
then F.a1 in rng Sgm(A) by A24,A53,A67;
then
A73: F.a1 in A by a11,FINSEQ_1:def 14;
now
assume a2 in Seg len g;
then
F.a2 = Sgm(C).a2 & a2 in dom Sgm(C) by A24,A21,A54,FINSEQ_3:40;
then F.a2 in rng Sgm(C) by FUNCT_1:3;
then F.a2 in C by FINSEQ_1:def 14;
hence contradiction by A55,A73,XBOOLE_0:def 5;
end;
hence thesis by A56,A69,XBOOLE_0:def 3;
end;
a1 in Seg len g \/ seq(len g,n) by A10,A24,A53,Lm1;
hence thesis by A57,A66,XBOOLE_0:def 3;
end;
then reconsider F as Permutation of dom f by A27,FUNCT_2:57;
consider j being Nat such that
A74: j in dom F and
A75: F.j = i by A27,A19,FINSEQ_2:10;
A76: dom Per(f,F) = B by CALCUL_2:19
.= dom F by A24,A51,FINSEQ_1:def 3
.= dom h by A24,FINSEQ_1:def 3;
A77: now
let k be Nat such that
A78: k in dom h;
A79: k in Seg len h by A78,FINSEQ_1:def 3;
A80: now
A81: k in dom (F*f) by A76,A78,CALCUL_2:def 2;
given i be Nat such that
A82: i in dom IdFinS(p,n) and
A83: k = len g + i;
len IdFinS(p,n) = n by CARD_1:def 7;
then
A84: i <= n by A82,FINSEQ_3:25;
then
A85: k <= n+len g by A83,XREAL_1:6;
A86: 1 <= i by A82,FINSEQ_3:25;
then 1+len g <= k by A83,XREAL_1:6;
then
A87: k in seq(len g,n) by A85,CALCUL_2:1;
then F.k = Sgm(A).(k-len g) by A24,A79;
then F.k in rng Sgm(A) by A12,A87,FUNCT_1:3;
then F.k in A by a11,FINSEQ_1:def 14;
then f.(F.k) in {p} by FUNCT_1:def 7;
then f.(F.k) = p by TARSKI:def 1;
then (F*f).k = p by A81,FUNCT_1:12;
then
A88: Per(f,F).k = p by CALCUL_2:def 2;
i in Seg n by A86,A84,FINSEQ_1:1;
hence Per(f,F).k = IdFinS(p,n).i by A88,FUNCOP_1:7
.= h.k by A82,A83,FINSEQ_1:def 7;
end;
now
assume
A89: k in dom g;
then
A90: k in dom Sgm(C) by A26,A21,FINSEQ_1:def 3;
k in Seg len g by A89,FINSEQ_1:def 3;
then
A91: F.k = Sgm(C).k by A24,A79;
k in dom (F*f) by A76,A78,CALCUL_2:def 2;
then (F*f).k = f.(Sgm(C).k) by A91,FUNCT_1:12;
hence Per(f,F).k = f.(Sgm(C).k) by CALCUL_2:def 2
.= (Sgm(C)*f).k by A90,FUNCT_1:13
.= g.k by FINSEQ_3:def 1
.= h.k by A89,FINSEQ_1:def 7;
end;
hence Per(f,F).k = h.k by A78,A80,FINSEQ_1:25;
end;
then
A92: Per(f,F) = h by A76;
reconsider h as FinSequence of CQC-WFF(Al) by A76,A77,FINSEQ_1:13;
(F*f).j = p by A20,A74,A75,FUNCT_1:13;
then
A93: h.j = p by A92,CALCUL_2:def 2;
A94: now
assume
A95: j in dom g;
then g.j = p by A93,FINSEQ_1:def 7;
then
A96: g.j in {p} by TARSKI:def 1;
A97: rng g = rng f \ {p} by FINSEQ_3:65;
g.j in rng g by A95,FUNCT_1:3;
hence contradiction by A96,A97,XBOOLE_0:def 5;
end;
j in dom f by A74;
then j in dom h by A76,CALCUL_2:19;
then consider k be Nat such that
A98: k in dom IdFinS(p,n) and
j = len g + k by A94,FINSEQ_1:25;
reconsider g as FinSequence of CQC-WFF(Al) by FINSEQ_3:86;
1 <= k & k <= len IdFinS(p,n) by A98,FINSEQ_3:25;
then 1 <= len IdFinS(p,n) by XXREAL_0:2;
then
A99: 1 <= n by CARD_1:def 7;
|- h^<*'not' p*> by A9,A92,CALCUL_2:30;
then
A100: |- g^<*p*>^<*'not' p*> by A99,CALCUL_2:32;
rng g = rng f \ {p} & rng f \ {p} c= (X \/ {p}) \ {p} by A8,FINSEQ_3:65
,XBOOLE_1:33;
then
A101: rng g c= X \ {p} by XBOOLE_1:40;
X \ {p} c= X by XBOOLE_1:36;
then
A102: rng g c= X by A101;
|- g^<*'not' p*>^<*'not' p*> by CALCUL_2:21;
then |- g^<*'not' p*> by A100,CALCUL_2:26;
hence thesis by A102;
end;
hence thesis by A9;
end;
end;
begin :: Unions of Consistent Sets
:: Ebb et al, Chapter IV, Lemma 7.7
theorem
for f being sequence of bool CQC-WFF(Al) st (for n,m st m in dom f & n
in dom f & n < m holds f.n is Consistent & f.n c= f.m) holds (union rng f) is
Consistent
proof
let f be sequence of bool CQC-WFF(Al);
assume
A1: for n,m st m in dom f & n in dom f & n < m holds f.n is Consistent &
f.n c= f.m;
now
A2: for n st n in dom f holds f.n is Consistent
proof
let n such that
A3: n in dom f;
n+1 in NAT;
then n < n+1 & n+1 in dom f by FUNCT_2:def 1,NAT_1:13;
hence thesis by A1,A3;
end;
assume not union rng f is Consistent;
then consider Z such that
A4: Z c= union rng f & Z is finite and
A5: Z is Inconsistent by Th7;
for n,m st m in dom f & n in dom f & n < m holds f.n c= f.m by A1;
then consider k such that
A6: Z c= f.k by A4,Th3;
reconsider Y = f.k as Subset of CQC-WFF(Al);
consider p such that
A7: Z |- p and
A8: Z |- 'not' p by A5;
consider f1 such that
A9: rng f1 c= Z and
A10: |- f1^<*p*> by A7;
consider f2 such that
A11: rng f2 c= Z and
A12: |- f2^<*'not' p*> by A8;
rng(f1^f2) = rng f1 \/ rng f2 by FINSEQ_1:31;
then rng(f1^f2) c= Z by A9,A11,XBOOLE_1:8;
then
A13: rng(f1^f2) c= Y by A6;
|- f1^f2^<*'not' p*> by A12,CALCUL_2:20;
then
A14: Y |- 'not' p by A13;
|- f1^f2^<*p*> by A10,Th5;
then Y |- p by A13;
then
A15: not Y is Consistent by A14;
k in NAT by ORDINAL1:def 12;
then k in dom f by FUNCT_2:def 1;
hence contradiction by A15,A2;
end;
hence thesis;
end;
begin :: Construction of a Henkin Model
reserve A for non empty set,
v for Element of Valuations_in(Al,A),
J for interpretation of Al,A;
theorem Th12:
X is Inconsistent implies for J,v holds not J,v |= X
proof
reconsider p = 'not' VERUM(Al) as Element of CQC-WFF(Al);
assume not X is Consistent;
then X |- 'not' VERUM(Al) by Th6;
then consider f such that
A1: rng f c= X and
A2: |- f^<*'not' VERUM(Al)*>;
let J,v;
A3: Suc(f^<*p*>) = p by CALCUL_1:5;
rng Ant(f^<*p*>) c= X by A1,CALCUL_1:5;
then p is_formal_provable_from X by A2,A3,CALCUL_1:def 10;
then
A4: X |= p by CALCUL_1:32;
now
assume J,v |= X;
then J,v |= 'not' VERUM(Al) by A4,CALCUL_1:def 12;
then not J,v |= VERUM(Al) by VALUAT_1:17;
hence contradiction by VALUAT_1:32;
end;
hence thesis;
end;
theorem Th13:
{VERUM(Al)} is Consistent
proof
set A =the non empty set,J =the interpretation of Al,A ,v =the Element of
Valuations_in(Al,A);
J,v |= VERUM(Al) by VALUAT_1:32;
then for p st p in {VERUM(Al)} holds J,v |= p by TARSKI:def 1;
then J,v |= {VERUM(Al)} by CALCUL_1:def 11;
hence thesis by Th12;
end;
registration
let Al;
cluster Consistent for Subset of CQC-WFF(Al);
existence
proof
{VERUM(Al)} is Consistent by Th13;
hence thesis;
end;
end;
reserve CX for Consistent Subset of CQC-WFF(Al),
P9 for Element of QC-pred_symbols(Al);
definition
let Al;
func HCar(Al) -> non empty set equals
bound_QC-variables(Al);
coherence;
end;
definition
let Al;
let P be (Element of QC-pred_symbols(Al)), ll be CQC-variable_list of (
the_arity_of P), Al;
redefine func P!ll -> Element of CQC-WFF(Al); :: redefines ! (QC_LANG1, definition)
coherence
proof
set k = the_arity_of P;
reconsider P9 = P as QC-pred_symbol of k,Al by QC_LANG3:1;
P9!ll is Element of CQC-WFF(Al);
hence thesis;
end;
end;
:: The Henkin Model (Ebb et al, Chapter V, §1)
definition
let Al;
let CX;
mode Henkin_interpretation of CX -> interpretation of Al,HCar(Al) means
:Def5:
for
P being (Element of QC-pred_symbols(Al)), r being Element of relations_on
HCar(Al) st it.P = r holds for a holds a in r iff
ex ll being CQC-variable_list of (the_arity_of P), Al st a = ll &
CX |- P!ll;
existence
proof
defpred P[object,object] means ex P9 st P9 = $1 & $2 = {ll where ll is
CQC-variable_list of (the_arity_of P9), Al : CX |- P9!ll};
set A = QC-pred_symbols(Al);
A1: for a being object st a in A ex b being object st P[a,b]
proof
let a be object;
assume a in A;
then reconsider a as Element of QC-pred_symbols(Al);
consider b such that
A2: b = {ll where ll is CQC-variable_list of (the_arity_of a), Al :
CX |- a!ll};
take b;
take a;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = A &
for a being object st a in A holds P[a,f.a] from CLASSES1:sch 1(A1);
A4: for P being (Element of QC-pred_symbols(Al)), r being Element of
relations_on HCar(Al) st f.P = r holds for a holds a in r iff ex ll being
CQC-variable_list of (the_arity_of P), Al st a = ll & CX |- P!ll
proof
let P be (Element of QC-pred_symbols(Al)),
r be Element of relations_on HCar(Al)
such that
A5: f.P = r;
let a;
thus a in r implies ex ll being CQC-variable_list of
(the_arity_of P), Al st
a = ll & CX |- P!ll
proof
assume
A6: a in r;
ex P9 st P9 = P & f.P = {ll where ll is CQC-variable_list of (
the_arity_of P9), Al : CX |- P9!ll} by A3;
hence thesis by A5,A6;
end;
thus (ex ll being CQC-variable_list of (the_arity_of P), Al
st a = ll & CX |- P!ll) implies a in r
proof
given ll being CQC-variable_list of (the_arity_of P),Al such that
A7: a = ll & CX |- P!ll;
ex P9 st P9 = P & f.P = {l where l is CQC-variable_list of (
the_arity_of P9), Al : CX |- P9!l} by A3;
hence thesis by A5,A7;
end;
end;
A8: for P being (Element of QC-pred_symbols(Al)), r being Element of
relations_on HCar(Al) st f.P = r holds r = empty_rel(HCar(Al)) or
the_arity_of P = the_arity_of r
proof
let P be (Element of QC-pred_symbols(Al)),
r be Element of relations_on HCar(Al)
such that
A9: f.P = r;
consider P9 such that
A10: P9 = P & f.P = {ll where ll is CQC-variable_list of (
the_arity_of P9), Al : CX |- P9!ll} by A3;
assume
A11: not r = empty_rel(HCar(Al));
then r <> {} by MARGREL1:9;
then consider a being object such that
A12: a in r by XBOOLE_0:def 1;
consider ll9 being CQC-variable_list of (the_arity_of P9), Al
such that
A13: a = ll9 and
CX |- P9!ll9 by A9,A12,A10;
rng ll9 c= bound_QC-variables(Al) by RELAT_1:def 19;
then reconsider a as FinSequence of HCar(Al) by A13,FINSEQ_1:def 4;
the_arity_of r = len a by A11,A12,MARGREL1:def 10;
hence thesis by A10,A13,CARD_1:def 7;
end;
for b being object holds b in rng f implies b in relations_on HCar(Al)
proof let b be object;
reconsider bb=b as set by TARSKI:1;
assume b in rng f;
then consider a being object such that
A14: a in dom f and
A15: b = f.a by FUNCT_1:def 3;
consider P9 such that
A16: P9 = a & f.a = {ll where ll is CQC-variable_list of (
the_arity_of P9), Al : CX |- P9!ll} by A3,A14;
for c being object holds c in bb implies c in HCar(Al)*
proof let c be object;
assume c in bb;
then consider
ll being CQC-variable_list of (the_arity_of P9), Al such that
A17: c = ll and
CX |- P9!ll by A15,A16;
rng ll c= bound_QC-variables(Al) by RELAT_1:def 19;
then ll is FinSequence of HCar(Al) by FINSEQ_1:def 4;
hence thesis by A17,FINSEQ_1:def 11;
end;
then
A18: bb c= HCar(Al)*;
for fin,fin9 being FinSequence of HCar(Al) st fin in bb & fin9 in bb
holds len fin = len fin9
proof
let fin,fin9 be FinSequence of HCar(Al);
assume that
A19: fin in bb and
A20: fin9 in bb;
ex ll being CQC-variable_list of (the_arity_of P9), Al st fin = ll &
CX |- P9!ll by A15,A16,A19;
then
A21: len fin = the_arity_of P9 by CARD_1:def 7;
ex ll9 being CQC-variable_list of (the_arity_of P9), Al st fin9 = ll9
& CX |- P9!ll9 by A15,A16,A20;
hence thesis by A21,CARD_1:def 7;
end;
hence thesis by A18,MARGREL1:def 7;
end;
then rng f c= relations_on HCar(Al);
then reconsider f as Function of A,relations_on HCar(Al) by A3,FUNCT_2:2;
reconsider f as interpretation of Al,HCar(Al) by A8,VALUAT_1:def 5;
take f;
thus thesis by A4;
end;
end;
definition
let Al;
func valH(Al) -> Element of Valuations_in (Al,HCar(Al)) equals
id bound_QC-variables(Al);
coherence by VALUAT_1:def 1;
end;
begin :: Some Properties of the Henkin Model
reserve JH for Henkin_interpretation of CX;
theorem Th14:
(valH(Al))*'ll = ll
proof
A1: for i st i in dom ((valH(Al))*'ll) holds (valH(Al)).(ll.i) = ll.i
proof
A2: dom((valH(Al))*'ll) c= dom ll by RELAT_1:25;
let i;
assume i in dom ((valH(Al))*'ll);
then
A3: ll.i in rng ll by A2,FUNCT_1:3;
rng ll c= bound_QC-variables(Al) by RELAT_1:def 19;
hence thesis by A3,FUNCT_1:18;
end;
A4: for i st 1 <= i & i <= k holds (valH(Al)).(ll.i) = ll.i
proof
let i such that
A5: 1 <= i and
A6: i <= k;
i <= len ((valH(Al))*'ll) by A6,VALUAT_1:def 3;
then i in dom ((valH(Al))*'ll) by A5,FINSEQ_3:25;
hence thesis by A1;
end;
A7: len ll = k by CARD_1:def 7;
then
A8: dom ll = Seg k by FINSEQ_1:def 3;
A9: for i being Nat st i in dom ll holds ((valH(Al))*'ll).i = ll.i
proof
let i be Nat such that
A10: i in dom ll;
reconsider i as Nat;
A11: 1 <= i & i <= k by A8,A10,FINSEQ_1:1;
then ((valH(Al))*'ll).i = (valH(Al)).(ll.i) by VALUAT_1:def 3;
hence thesis by A4,A11;
end;
len ((valH(Al))*'ll) = k by VALUAT_1:def 3;
hence thesis by A7,A9,FINSEQ_2:9;
end;
theorem Th15:
|- f^<*VERUM(Al)*>
proof
set PR = <*[f^<*VERUM(Al)*>,1]*>;
A1: rng PR = {[f^<*VERUM(Al)*>,1]} by FINSEQ_1:38;
now
let a be object;
assume a in rng PR;
then
A2: a = [f^<*VERUM(Al)*>,1] by A1,TARSKI:def 1;
f^<*VERUM(Al)*> in set_of_CQC-WFF-seq(Al) by CALCUL_1:def 6;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A2,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng PR c= [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
then reconsider
PR as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds :] by
FINSEQ_1:def 4;
now
let n be Nat such that
A3: 1 <= n and
A4: n <= len PR;
n <= 1 by A4,FINSEQ_1:39;
then n = 1 by A3,XXREAL_0:1;
then PR.n = [f^<*VERUM(Al)*>,1];
then (PR.n)`1 = f^<*VERUM(Al)*> & (PR.n)`2 = 1;
hence PR,n is_a_correct_step by CALCUL_1:def 7;
end;
then
A5: PR is a_proof by CALCUL_1:def 8;
PR.1 = [f^<*VERUM(Al)*>,1];
then PR.(len PR) = [f^<*VERUM(Al)*>,1] by FINSEQ_1:40;
then (PR.(len PR))`1 = f^<*VERUM(Al)*>;
hence thesis by A5,CALCUL_1:def 9;
end;
theorem
JH,valH(Al) |= VERUM(Al) iff CX |- VERUM(Al)
proof
set f = <*>CQC-WFF(Al);
rng f c= CX & |- f^<*VERUM(Al)*> by Th15;
hence thesis by VALUAT_1:32;
end;
theorem
JH,valH(Al) |= P!ll iff CX |- P!ll
proof
thus JH,valH(Al) |= P!ll implies CX |- P!ll
proof
set rel = JH.P;
reconsider rel as Element of relations_on HCar(Al);
assume JH,valH(Al) |= P!ll;
then Valid(P!ll,JH).valH(Al) = TRUE by VALUAT_1:def 7;
then ((valH(Al))*'ll) in rel by VALUAT_1:7;
then ll in rel by Th14;
then
ex ll9 being CQC-variable_list of (the_arity_of P), Al st
ll9 = ll & CX |- P!ll9 by Def5;
hence thesis;
end;
thus CX |- P!ll implies JH,valH(Al) |= P!ll
proof
P is (QC-pred_symbol of the_arity_of P, Al) by QC_LANG3:1;
then
A1: the_arity_of P = k by SUBSTUT2:3;
assume CX |- P!ll;
then ll in JH.P by A1,Def5;
then ((valH(Al))*'ll) in JH.P by Th14;
then Valid(P!ll,JH).valH(Al) = TRUE by VALUAT_1:7;
hence thesis by VALUAT_1:def 7;
end;
end;