Copyright (c) 1990 Association of Mizar Users
environ
vocabulary ORDINAL2, ARYTM, BOOLE, FINSET_1, FUNCT_1, RELAT_1, MCART_1,
FINSEQ_1, CQC_LANG, QC_LANG1, ZF_LANG, ARYTM_1, QMAX_1, CQC_THE1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0,
RELAT_1, FUNCT_1, ORDINAL2, NAT_1, FINSET_1, FINSEQ_1, MCART_1, QC_LANG1,
CQC_LANG;
constructors NAT_1, CQC_LANG, XREAL_0, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FINSET_1, RELSET_1, XREAL_0, CQC_LANG, FINSEQ_1, ARYTM_3,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, AXIOMS, ZFMISC_1, FINSET_1, FINSEQ_1, MCART_1, FUNCT_1,
NAT_1, REAL_1, EQREL_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes NAT_1, FUNCT_1, FRAENKEL, XBOOLE_0;
begin
:: --------- Auxiliary theorems
reserve n for natural number;
canceled;
theorem n <= 1 implies n = 0 or n = 1
proof
assume A1: n <= 1;
assume A2: not (n = 0 or n = 1);
then n < 0+1 by A1,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem n <= 2 implies n = 0 or n = 1 or n = 2
proof
assume A1: n <= 2;
assume A2: not (n = 0 or n = 1 or n = 2);
then n < 1+1 by A1,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem n <= 3 implies n = 0 or n = 1 or n = 2 or n = 3
proof
assume A1: n <= 3;
assume A2: not (n = 0 or n = 1 or n = 2 or n = 3);
then n < 2+1 by A1,REAL_1:def 5;
then n <= 2 by NAT_1:38;
then n < 1+1 by A2,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem n <= 4 implies n = 0 or n = 1 or n = 2 or n = 3
or n = 4
proof
assume A1: n <= 4;
assume A2: not (n = 0 or n = 1 or n = 2 or n = 3 or n = 4);
then n < 3+1 by A1,REAL_1:def 5;
then n <= 3 by NAT_1:38;
then n < 2+1 by A2,REAL_1:def 5;
then n <= 2 by NAT_1:38;
then n < 1+1 by A2,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem n <= 5 implies n = 0 or n = 1 or n = 2 or n = 3
or n = 4 or n = 5
proof
assume A1: n <= 5;
assume A2: not (n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5);
then n < 4+1 by A1,REAL_1:def 5;
then n <= 4 by NAT_1:38;
then n < 3+1 by A2,REAL_1:def 5;
then n <= 3 by NAT_1:38;
then n < 2+1 by A2,REAL_1:def 5;
then n <= 2 by NAT_1:38;
then n < 1+1 by A2,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem n <= 6 implies n = 0 or n = 1 or n = 2 or n = 3
or n = 4 or n = 5 or n = 6
proof
assume A1: n <= 6;
assume A2: not (n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or
n = 6);
then n < 5+1 by A1,REAL_1:def 5;
then n <= 5 by NAT_1:38;
then n < 4+1 by A2,REAL_1:def 5;
then n <= 4 by NAT_1:38;
then n < 3+1 by A2,REAL_1:def 5;
then n <= 3 by NAT_1:38;
then n < 2+1 by A2,REAL_1:def 5;
then n <= 2 by NAT_1:38;
then n < 1+1 by A2,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem n <= 7 implies n = 0 or n = 1 or n = 2 or n = 3
or n = 4 or n = 5 or n = 6 or n = 7
proof
assume A1: n <= 7;
assume A2: not (n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or
n = 6 or n = 7);
then n < 6+1 by A1,REAL_1:def 5;
then n <= 6 by NAT_1:38;
then n < 5+1 by A2,REAL_1:def 5;
then n <= 5 by NAT_1:38;
then n < 4+1 by A2,REAL_1:def 5;
then n <= 4 by NAT_1:38;
then n < 3+1 by A2,REAL_1:def 5;
then n <= 3 by NAT_1:38;
then n < 2+1 by A2,REAL_1:def 5;
then n <= 2 by NAT_1:38;
then n < 1+1 by A2,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem n <= 8 implies n = 0 or n = 1 or n = 2 or n = 3
or n = 4 or n = 5 or n = 6 or n = 7 or n = 8
proof
assume A1: n <= 8;
assume A2: not (n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or
n = 6 or n = 7 or n = 8);
then n < 7+1 by A1,REAL_1:def 5;
then n <= 7 by NAT_1:38;
then n < 6+1 by A2,REAL_1:def 5;
then n <= 6 by NAT_1:38;
then n < 5+1 by A2,REAL_1:def 5;
then n <= 5 by NAT_1:38;
then n < 4+1 by A2,REAL_1:def 5;
then n <= 4 by NAT_1:38;
then n < 3+1 by A2,REAL_1:def 5;
then n <= 3 by NAT_1:38;
then n < 2+1 by A2,REAL_1:def 5;
then n <= 2 by NAT_1:38;
then n < 1+1 by A2,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
theorem Th10: n <= 9 implies n = 0 or n = 1 or n = 2 or n = 3
or n = 4 or n = 5 or n = 6 or n = 7 or n = 8 or n = 9
proof
assume A1: n <= 9;
assume A2: not (n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or
n = 6 or n = 7 or n = 8 or n = 9);
then n < 8+1 by A1,REAL_1:def 5;
then n <= 8 by NAT_1:38;
then n < 7+1 by A2,REAL_1:def 5;
then n <= 7 by NAT_1:38;
then n < 6+1 by A2,REAL_1:def 5;
then n <= 6 by NAT_1:38;
then n < 5+1 by A2,REAL_1:def 5;
then n <= 5 by NAT_1:38;
then n < 4+1 by A2,REAL_1:def 5;
then n <= 4 by NAT_1:38;
then n < 3+1 by A2,REAL_1:def 5;
then n <= 3 by NAT_1:38;
then n < 2+1 by A2,REAL_1:def 5;
then n <= 2 by NAT_1:38;
then n < 1+1 by A2,REAL_1:def 5;
then n <= 1 by NAT_1:38;
then n < 0+1 by A2,REAL_1:def 5;
then n <= 0 by NAT_1:38;
hence contradiction by A2,NAT_1:18;
end;
reserve i,j,n,k,l for Nat;
reserve a for set;
theorem Th11: {k: k <= n + 1} = {i: i <= n} \/ {n + 1}
proof
thus {k: k <= n + 1} c= {i: i <= n} \/ {n + 1}
proof
let a; assume a in {k: k <= n + 1};
then consider k such that A1: k=a & k <= n+1;
k = a & (k <= n or k = n+1) by A1,NAT_1:26;
then a in {i: i <= n} or a in {n + 1} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
thus {i:i <= n} \/ {n+1} c= {k: k <= n + 1}
proof
let a; assume a in {i:i <= n} \/ {n+1};
then a in {i:i <= n} or a in {n+1} by XBOOLE_0:def 2;
then A2: (ex i st a=i & i <= n) or a = n + 1 by TARSKI:def 1;
now given i such that A3: a=i & i <= n;
n <= n + 1 by NAT_1:29;
then i <= n + 1 by A3,AXIOMS:22;
hence a in {k: k <= n + 1} by A3;
end;
hence thesis by A2;
end;
end;
theorem Th12: for n holds {k: k <= n} is finite
proof
defpred P[Nat] means {k: k <= $1} is finite;
{k: k <= 0} = {0}
proof
thus {k: k <= 0} c= {0}
proof
let a; assume a in {k: k <= 0};
then consider k such that A1: k = a & k <= 0;
k = 0 by A1,NAT_1:19;
hence thesis by A1,TARSKI:def 1;
end;
thus {0} c= {k: k <= 0}
proof
let a; assume a in {0};
then a = 0 & 0 <= 0 by TARSKI:def 1;
hence a in {k: k <= 0};
end;
end;
then A2: P[0];
A3: for n st P[n] holds P[n+1]
proof
let n;
assume A4: P[n];
{l: l <= n + 1} = {k: k <= n} \/ {n + 1} by Th11;
hence P[n+1] by A4,FINSET_1:14;
end;
thus for n being Nat holds P[n] from Ind(A2,A3);
end;
reserve X,Y,Z for set;
deffunc F(set) = $1`1;
theorem X is finite & X c= [:Y,Z:] implies
ex A,B being set st A is finite & A c= Y & B is finite & B c= Z &
X c= [:A,B:]
proof
deffunc G(set) = $1`2;
assume A1: X is finite & X c= [:Y,Z:];
consider f being Function such that
A2: dom f = X and A3: for a st a in X holds f.a = F(a) from Lambda;
consider g being Function such that
A4: dom g = X and A5: for a st a in X holds g.a = G(a) from Lambda;
take A = rng f, B = rng g;
thus A is finite by A1,A2,FINSET_1:26;
thus A c= Y
proof
let a; assume a in A;
then consider x being set such that A6: x in
dom f & f.x = a by FUNCT_1:def 5;
consider y,z being set such that A7: y in Y & z in Z & x = [y,z]
by A1,A2,A6,ZFMISC_1:def 2;
f.x = x`1 by A2,A3,A6
.= y by A7,MCART_1:7;
hence thesis by A6,A7;
end;
thus B is finite by A1,A4,FINSET_1:26;
thus B c= Z
proof
let a; assume a in B;
then consider x being set such that A8: x in
dom g & g.x = a by FUNCT_1:def 5;
consider y,z being set such that A9: y in Y & z in Z & x = [y,z]
by A1,A4,A8,ZFMISC_1:def 2;
g.x = x`2 by A4,A5,A8
.= z by A9,MCART_1:7;
hence thesis by A8,A9;
end;
thus X c= [:A,B:]
proof
let a; assume A10: a in X;
then consider x,y being set such that A11: x in Y & y in Z & a=[x,y]
by A1,ZFMISC_1:def 2;
A12: g.a = a`2 by A5,A10
.= y by A11,MCART_1:7;
f.a = a`1 by A3,A10
.= x by A11,MCART_1:7;
then x in A & y in B by A2,A4,A10,A12,FUNCT_1:def 5;
hence a in [:A,B:] by A11,ZFMISC_1:106;
end;
end;
theorem Th14: X is finite & Z is finite & X c= [:Y,Z:] implies
ex A being set st A is finite & A c= Y & X c= [:A,Z:]
proof
assume A1: X is finite & Z is finite & X c= [:Y,Z:];
consider f being Function such that
A2: dom f = X and A3: for a st a in X holds f.a = F(a) from Lambda;
take A = rng f;
thus A is finite by A1,A2,FINSET_1:26;
thus A c= Y
proof
let a; assume a in A;
then consider x being set such that A4: x in
dom f & f.x = a by FUNCT_1:def 5;
consider y,z being set such that A5: y in Y & z in Z & x = [y,z]
by A1,A2,A4,ZFMISC_1:def 2;
f.x = x`1 by A2,A3,A4
.= y by A5,MCART_1:7;
hence thesis by A4,A5;
end;
thus X c= [:A,Z:]
proof
let a; assume A6: a in X;
then consider x,y being set such that A7: x in Y & y in Z & a=[x,y]
by A1,ZFMISC_1:def 2;
f.a = a`1 by A3,A6
.= x by A7,MCART_1:7;
then x in A by A2,A6,FUNCT_1:def 5;
hence thesis by A7,ZFMISC_1:106;
end;
end;
Lm1: <*a*> <> {}
proof
len<*a*> = 1 by FINSEQ_1:56;
hence thesis by FINSEQ_1:25;
end;
:: --------- The axiomatic of a first-order calculus
reserve T,S,X,Y for Subset of CQC-WFF;
reserve p,q,r,t,F,H,G for Element of CQC-WFF;
reserve s for QC-formula;
reserve x,y for bound_QC-variable;
definition let T;
attr T is being_a_theory means
:Def1: VERUM in T & for p,q,r,s,x,y holds
('not' p => p) => p in T &
p => ('not' p => q) in T &
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in T &
(p '&' q => q '&' p in T) &
(p in T & p => q in T implies q in T) &
(All(x,p) => p in T) &
(p => q in T & not x in still_not-bound_in p implies p => All(x,q) in T) &
(s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s & s.x in T
implies s.y in T);
synonym T is_a_theory;
end;
canceled 10;
theorem T is_a_theory & S is_a_theory implies T /\ S is_a_theory
proof
assume that A1: T is_a_theory and A2: S is_a_theory;
VERUM in T & VERUM in S by A1,A2,Def1;
hence VERUM in T /\ S by XBOOLE_0:def 3;
let p,q,r,s,x,y;
('not' p => p) => p in T & ('not' p => p) => p in S by A1,A2,Def1;
hence ('not' p => p) => p in T /\ S by XBOOLE_0:def 3;
p => ('not' p => q) in T & p => ('not' p => q) in S by A1,A2,Def1;
hence p => ('not' p => q) in T /\ S by XBOOLE_0:def 3;
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in T &
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in S by A1,A2,Def1;
hence (p => q) => ('not'(q '&' r) => 'not'
(p '&' r)) in T /\ S by XBOOLE_0:def 3;
p '&' q => q '&' p in T & p '&' q => q '&' p in S by A1,A2,Def1;
hence p '&' q => q '&' p in T /\ S by XBOOLE_0:def 3;
(p in T & p => q in T implies q in T) & (p in S & p => q in S implies q in
S)
by A1,A2,Def1;
hence (p in T /\ S & p => q in T /\ S implies q in T /\ S) by XBOOLE_0:def 3
;
All(x,p) => p in T & All(x,p) => p in S by A1,A2,Def1;
hence All(x,p) => p in T /\ S by XBOOLE_0:def 3;
(p => q in T & not x in still_not-bound_in p implies p => All(x,q) in T) &
(p => q in S & not x in still_not-bound_in p implies p => All(x,q) in S)
by A1,A2,Def1;
hence p => q in T /\ S & not x in still_not-bound_in p implies
p => All(x,q) in T /\ S by XBOOLE_0:def 3;
(s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s & s.x in
T
implies s.y in T) &
(s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s & s.x in S
implies s.y in S) by A1,A2,Def1;
hence s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x in T /\ S implies s.y in T /\ S by XBOOLE_0:def 3;
end;
:: --------- The consequence operation
definition let X;
func Cn(X) -> Subset of CQC-WFF means
:Def2: t in it iff for T st T is_a_theory & X c= T holds t in T;
existence
proof
defpred P[set] means for T st T is_a_theory & X c= T holds $1 in T;
consider Y being set such that
A1: for a holds a in Y iff a in CQC-WFF & P[a] from Separation;
Y c= CQC-WFF
proof
let a; assume a in Y;
hence a in CQC-WFF by A1;
end;
then reconsider Z=Y as Subset of CQC-WFF;
take Z;
thus t in Z iff for T st T is_a_theory & X c= T holds t in T by A1;
end;
uniqueness
proof
let Y,Z be Subset of CQC-WFF such that
A2: t in Y iff for T st T is_a_theory & X c= T holds t in T and
A3: t in Z iff for T st T is_a_theory & X c= T holds t in T;
a in Y iff a in Z
proof
thus a in Y implies a in Z
proof
assume A4: a in Y;
then reconsider t=a as Element of CQC-WFF;
for T st T is_a_theory & X c= T holds t in T by A2,A4;
hence a in Z by A3;
end;
thus a in Z implies a in Y
proof
assume A5: a in Z;
then reconsider t=a as Element of CQC-WFF;
for T st T is_a_theory & X c= T holds t in T by A3,A5;
hence a in Y by A2;
end;
end;
hence thesis by TARSKI:2;
end;
end;
canceled;
theorem Th27: VERUM in Cn(X)
proof
T is_a_theory & X c= T implies VERUM in T by Def1;
hence thesis by Def2;
end;
theorem Th28: ('not' p => p) => p in Cn(X)
proof
T is_a_theory & X c= T implies ('not' p => p) => p in T by Def1;
hence thesis by Def2;
end;
theorem Th29: p => ('not' p => q) in Cn(X)
proof
T is_a_theory & X c= T implies p => ('not' p => q) in T by Def1;
hence thesis by Def2;
end;
theorem Th30: (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in Cn(X)
proof
T is_a_theory & X c= T implies
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in T by Def1;
hence thesis by Def2;
end;
theorem Th31: p '&' q => q '&' p in Cn(X)
proof
T is_a_theory & X c= T implies p '&' q => q '&' p in T by Def1;
hence thesis by Def2;
end;
theorem Th32: p in Cn(X) & p => q in Cn(X) implies q in Cn(X)
proof
assume that A1: p in Cn(X) and A2: p => q in Cn(X);
T is_a_theory & X c= T implies q in T
proof
assume that A3: T is_a_theory and A4: X c= T;
p in T & p => q in T by A1,A2,A3,A4,Def2;
hence thesis by A3,Def1;
end;
hence thesis by Def2;
end;
theorem Th33: All(x,p) => p in Cn(X)
proof
T is_a_theory & X c= T implies All(x,p) => p in T by Def1;
hence thesis by Def2;
end;
theorem
Th34: p => q in Cn(X) & not x in still_not-bound_in p implies
p => All(x,q) in Cn(X)
proof assume
A1: p => q in Cn(X) & not x in still_not-bound_in p;
T is_a_theory & X c= T implies p => All(x,q) in T
proof assume
A2: T is_a_theory & X c= T;
then p => q in T by A1,Def2;
hence thesis by A1,A2,Def1;
end;
hence thesis by Def2;
end;
theorem
Th35: s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x in Cn(X) implies s.y in Cn(X)
proof assume
A1: s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s & s.x in
Cn(X);
then reconsider s1 = s.x as Element of CQC-WFF;
reconsider q = s.y as Element of CQC-WFF by A1;
T is_a_theory & X c= T implies q in T
proof assume
A2: T is_a_theory & X c= T;
then s1 in T by A1,Def2;
hence thesis by A1,A2,Def1;
end;
hence thesis by Def2;
end;
theorem Th36: Cn(X) is_a_theory
proof
thus VERUM in Cn(X) by Th27;
let p,q,r,s,x,y;
thus ('not' p => p) =>p in Cn(X) & p => ('not' p => q) in Cn(X) &
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in Cn(X) &
p '&' q => q '&' p in Cn(X) & (p in Cn(X) & p => q in Cn(X) implies q in
Cn(X))
by Th28,Th29,Th30,Th31,Th32;
thus thesis by Th33,Th34,Th35;
end;
theorem Th37: T is_a_theory & X c= T implies Cn(X) c= T
proof
assume that A1:T is_a_theory and A2: X c= T;
thus Cn(X) c= T
proof
let a; assume a in Cn(X);
hence thesis by A1,A2,Def2;
end;
end;
theorem Th38: X c= Cn(X)
proof
let a; assume A1: a in X;
then reconsider t=a as Element of CQC-WFF;
for T st T is_a_theory & X c= T holds t in T by A1;
hence a in Cn(X) by Def2;
end;
theorem Th39: X c= Y implies Cn(X) c= Cn(Y)
proof
assume A1: X c= Y;
thus Cn(X) c= Cn(Y)
proof
let a; assume A2: a in Cn(X);
then reconsider t=a as Element of CQC-WFF;
for T st T is_a_theory & Y c= T holds t in T
proof
let T such that A3:T is_a_theory and A4:Y c= T;
X c= T by A1,A4,XBOOLE_1:1;
hence t in T by A2,A3,Def2;
end;
hence thesis by Def2;
end;
end;
Lm2: Cn(Cn(X)) c= Cn(X)
proof
let a; assume A1: a in Cn(Cn(X));
then reconsider t=a as Element of CQC-WFF;
for T st T is_a_theory & X c= T holds t in T
proof
let T; assume that A2: T is_a_theory and A3: X c= T;
Cn(X) c= T by A2,A3,Th37;
hence t in T by A1,A2,Def2;
end;
hence thesis by Def2;
end;
theorem Cn(Cn(X)) = Cn(X)
proof
Cn(Cn(X)) c= Cn(X) & Cn(X) c= Cn(Cn(X)) by Lm2,Th38;
hence thesis by XBOOLE_0:def 10;
end;
theorem Th41: T is_a_theory iff Cn(T) = T
proof
thus T is_a_theory implies Cn(T) = T
proof
assume A1: T is_a_theory;
A2: T c= Cn(T) by Th38;
Cn(T) c= T
proof
let a; assume a in Cn(T);
hence a in T by A1,Def2;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
thus Cn(T) = T implies T is_a_theory by Th36;
end;
:: ---------- The notion of proof
definition
func Proof_Step_Kinds -> set equals
:Def3: {k: k <= 9};
coherence;
end;
definition
cluster Proof_Step_Kinds -> non empty;
coherence
proof
9 in {k: k <= 9};
hence thesis by Def3;
end;
end;
canceled;
theorem Th43:
0 in Proof_Step_Kinds & 1 in Proof_Step_Kinds & 2 in Proof_Step_Kinds &
3 in Proof_Step_Kinds & 4 in Proof_Step_Kinds & 5 in Proof_Step_Kinds &
6 in Proof_Step_Kinds & 7 in Proof_Step_Kinds & 8 in Proof_Step_Kinds &
9 in Proof_Step_Kinds by Def3;
theorem Proof_Step_Kinds is finite by Def3,Th12;
reserve f,g for FinSequence of [:CQC-WFF,Proof_Step_Kinds:];
theorem Th45:
1 <= n & n <= len f implies
(f.n)`2 = 0 or (f.n)`2 = 1 or (f.n)`2 = 2 or (f.n)`2 = 3 or (f.n)`2 = 4
or (f.n)`2 = 5 or (f.n)`2 = 6 or (f.n)`2 = 7 or (f.n)`2 = 8 or
(f.n)`2 = 9
proof
assume A1: 1 <= n & n <= len f;
A2: dom f = Seg len f & rng f c= [:CQC-WFF,Proof_Step_Kinds:]
by FINSEQ_1:def 3,def 4;
then n in dom f by A1,FINSEQ_1:3;
then f.n in rng f by FUNCT_1:def 5;
then (f.n)`2 in Proof_Step_Kinds by A2,MCART_1:10;
then ex k st k = (f.n)`2 & k <= 9 by Def3;
hence thesis by Th10;
end;
definition let PR be (FinSequence of [:CQC-WFF,Proof_Step_Kinds:]),n,X;
pred PR,n is_a_correct_step_wrt X means
:Def4:
(PR.n)`1 in X if (PR.n)`2 = 0,
(PR.n)`1 = VERUM if (PR.n)`2 = 1,
ex p st (PR.n)`1 = ('not' p => p) => p if (PR.n)`2 = 2,
ex p,q st (PR.n)`1 = p => ('not' p => q) if (PR.n)`2 = 3,
ex p,q,r st (PR.n)`1 = (p => q) => ('not'(q '&' r) => 'not'(p '&' r))
if (PR.n)`2 = 4,
ex p,q st (PR.n)`1 = p '&' q => q '&' p
if (PR.n)`2 = 5,
ex p,x st (PR.n)`1 = All(x,p) => p if (PR.n)`2 = 6,
ex i,j,p,q st 1 <= i & i < n & 1 <= j & j < i & p = (PR.j)`1 & q = (PR.n)`1 &
(PR.i)`1 = p => q if (PR.n)`2 = 7,
ex i,p,q,x st 1 <= i & i < n & (PR.i)`1 = p => q &
not x in still_not-bound_in p & (PR.n)`1 = p => All(x,q)
if (PR.n)`2 = 8,
ex i,x,y,s st 1 <= i & i < n & s.x in CQC-WFF & s.y in CQC-WFF &
not x in still_not-bound_in s & s.x = (PR.i)`1 & s.y = (PR.n)`1
if (PR.n)`2 = 9;
consistency;
end;
definition let X,f;
pred f is_a_proof_wrt X means
:Def5: f <> {} &
for n st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt X;
end;
canceled 11;
theorem f is_a_proof_wrt X implies rng f <> {}
proof
assume f is_a_proof_wrt X;
then f <> {} by Def5;
hence thesis by FINSEQ_1:27;
end;
theorem Th58: f is_a_proof_wrt X implies 1 <= len f
proof
assume f is_a_proof_wrt X;
then f <> {} by Def5;
then len f <> 0 & 0 <= len f by FINSEQ_1:25,NAT_1:18;
then 0+1 <= len f by NAT_1:38;
hence thesis;
end;
theorem f is_a_proof_wrt X implies (f.1)`2 = 0 or (f.1)`2 = 1 or
(f.1)`2 = 2 or (f.1)`2 = 3 or (f.1)`2 = 4 or (f.1)`2 = 5 or (f.1)`2 = 6
proof
assume A1: f is_a_proof_wrt X;
then A2: 1 <= 1 & 1 <= len f by Th58;
then A3: f,1 is_a_correct_step_wrt X by A1,Def5;
assume A4: not((f.1)`2 = 0 or (f.1)`2 = 1 or (f.1)`2 = 2 or (f.1)`2 = 3
or (f.1)`2 = 4 or (f.1)`2 = 5 or (f.1)`2 = 6);
per cases by A2,A4,Th45;
suppose (f.1)`2 = 7;
then ex i,j,p,q st 1 <= i & i < 1 & 1 <= j & j < i &
p = (f.j)`1 & q = (f.1)`1 & (f.i)`1 = p => q by A3,Def4;
hence contradiction;
suppose (f.1)`2 = 8;
then ex i,p,q,x st 1 <= i & i < 1 & (f.i)`1 = p => q &
not x in still_not-bound_in p & (f.1)`1 = p => All(x,q) by A3,Def4;
hence contradiction;
suppose (f.1)`2 = 9;
then ex i,x,y,s st 1 <= i & i < 1 &
s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x = (f.i)`1 & (f.1)`1 = s.y by A3,Def4;
hence contradiction;
end;
theorem Th60:
1 <= n & n <= len f implies
(f,n is_a_correct_step_wrt X iff f^g,n is_a_correct_step_wrt X)
proof
assume A1: 1 <= n & n <= len f;
then n in Seg(len f) by FINSEQ_1:3;
then n in dom f by FINSEQ_1:def 3;
then A2: (f^g).n = f.n by FINSEQ_1:def 7;
len(f^g) = len f + len g by FINSEQ_1:35;
then len f <= len(f^g) by NAT_1:29;
then A3: 1 <= n & n <= len(f^g) by A1,AXIOMS:22;
thus f,n is_a_correct_step_wrt X implies f^g,n is_a_correct_step_wrt X
proof
assume A4: f,n is_a_correct_step_wrt X;
per cases by A3,Th45;
case ((f^g).n)`2 = 0;
hence ((f^g).n)`1 in X by A2,A4,Def4;
case ((f^g).n)`2 = 1;
hence ((f^g).n)`1 = VERUM by A2,A4,Def4;
case ((f^g).n)`2 = 2;
hence thesis by A2,A4,Def4;
case ((f^g).n)`2 = 3;
hence thesis by A2,A4,Def4;
case ((f^g).n)`2 = 4;
hence thesis by A2,A4,Def4;
case ((f^g).n)`2 = 5;
hence thesis by A2,A4,Def4;
case ((f^g).n)`2 = 6;
hence thesis by A2,A4,Def4;
case ((f^g).n)`2 = 7;
then consider i,j,r,t such that A5: 1 <= i & i < n & 1 <= j & j < i
and A6: r = (f.j)`1 and A7: t = (f.n)`1 and A8: (f.i)`1 = r => t
by A2,A4,Def4;
i <= len f & j <= n by A1,A5,AXIOMS:22;
then i in Seg(len f) & j <= len f by A5,AXIOMS:22,FINSEQ_1:3;
then i in Seg(len f) & j in Seg(len f) by A5,FINSEQ_1:3;
then i in dom f & j in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i & f.j = (f^g).j by FINSEQ_1:def 7;
hence thesis by A2,A5,A6,A7,A8;
case ((f^g).n)`2 = 8;
then consider i,r,t,x such that A9: 1 <= i & i < n and
A10: (f.i)`1 = r => t & not x in still_not-bound_in r &
(f.n)`1 = r => All(x,t) by A2,A4,Def4;
i <= len f by A1,A9,AXIOMS:22;
then i in Seg(len f) by A9,FINSEQ_1:3;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A2,A9,A10;
case ((f^g).n)`2 = 9;
then consider i,x,y,s such that A11: 1 <= i & i < n and
A12: s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x = (f.i)`1 & (f.n)`1 = s.y by A2,A4,Def4;
i <= len f by A1,A11,AXIOMS:22;
then i in Seg(len f) by A11,FINSEQ_1:3;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A2,A11,A12;
end;
assume A13: f^g,n is_a_correct_step_wrt X;
per cases by A1,Th45;
case (f.n)`2 = 0;
hence thesis by A2,A13,Def4;
case (f.n)`2 = 1;
hence thesis by A2,A13,Def4;
case (f.n)`2 = 2;
hence thesis by A2,A13,Def4;
case (f.n)`2 = 3;
hence thesis by A2,A13,Def4;
case (f.n)`2 = 4;
hence thesis by A2,A13,Def4;
case (f.n)`2 = 5;
hence thesis by A2,A13,Def4;
case (f.n)`2 = 6;
hence thesis by A2,A13,Def4;
case (f.n)`2 = 7;
then consider i,j,r,t such that A14: 1 <= i & i < n & 1 <= j & j < i
and A15: r = ((f^g).j)`1 and A16: t = ((f^g).n)`1 and
A17: ((f^g).i)`1 = r => t by A2,A13,Def4;
i <= len f & j <= n by A1,A14,AXIOMS:22;
then i in Seg(len f) & j <= len f by A14,AXIOMS:22,FINSEQ_1:3;
then i in Seg(len f) & j in Seg(len f) by A14,FINSEQ_1:3;
then i in dom f & j in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i & f.j = (f^g).j by FINSEQ_1:def 7;
hence thesis by A2,A14,A15,A16,A17;
case (f.n)`2 = 8;
then consider i,r,t,x such that A18: 1 <= i & i < n and
A19: ((f^g).i)`1 = r => t & not x in still_not-bound_in r &
((f^g).n)`1 = r => All(x,t) by A2,A13,Def4;
i <= len f by A1,A18,AXIOMS:22;
then i in Seg(len f) by A18,FINSEQ_1:3;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A2,A18,A19;
case (f.n)`2 = 9;
then consider i,x,y,s such that A20: 1 <= i & i < n and
A21: s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x = ((f^g).i)`1 & ((f^g).n)`1 = s.y by A2,A13,Def4;
i <= len f by A1,A20,AXIOMS:22;
then i in Seg(len f) by A20,FINSEQ_1:3;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A2,A20,A21;
end;
theorem Th61:
1 <= n & n <= len g & g,n is_a_correct_step_wrt X implies
(f^g),(n+len f) is_a_correct_step_wrt X
proof
assume that A1: 1 <= n & n <= len g and
A2: g,n is_a_correct_step_wrt X;
n in Seg(len g) by A1,FINSEQ_1:3;
then n in dom g by FINSEQ_1:def 3;
then A3: g.n = (f^g).(n+len f) by FINSEQ_1:def 7;
n + len f <= len f + len g by A1,AXIOMS:24;
then A4: 1 <= n+len f & n+len f <= len(f^g) by A1,FINSEQ_1:35,NAT_1:37;
per cases by A4,Th45;
case ((f^g).(n+len f))`2 = 0;
hence ((f^g).(n+len f))`1 in X by A2,A3,Def4;
case ((f^g).(n+len f))`2 = 1;
hence ((f^g).(n+len f))`1 = VERUM by A2,A3,Def4;
case ((f^g).(n+len f))`2 = 2;
hence thesis by A2,A3,Def4;
case ((f^g).(n+len f))`2 = 3;
hence thesis by A2,A3,Def4;
case ((f^g).(n+len f))`2 = 4;
hence thesis by A2,A3,Def4;
case ((f^g).(n+len f))`2 = 5;
hence thesis by A2,A3,Def4;
case ((f^g).(n+len f))`2 = 6;
hence thesis by A2,A3,Def4;
case ((f^g).(n+len f))`2 = 7;
then consider i,j,r,t such that A5: 1 <= i & i < n & 1 <= j & j < i
and A6: r = (g.j)`1 and A7: t = (g.n)`1 and A8: (g.i)`1 = r => t
by A2,A3,Def4;
A9: 1 <= i+len f & i+len f < n+len f by A5,NAT_1:37,REAL_1:53;
A10: 1 <= j+len f & j+len f < i+len f by A5,NAT_1:37,REAL_1:53;
i <= len g & j <= n by A1,A5,AXIOMS:22;
then i in Seg(len g) & j <= len g by A5,AXIOMS:22,FINSEQ_1:3;
then i in Seg(len g) & j in Seg(len g) by A5,FINSEQ_1:3;
then i in dom g & j in dom g by FINSEQ_1:def 3;
then g.i = (f^g).(i+len f) & g.j = (f^g).(j+len f) by FINSEQ_1:def 7;
hence thesis by A3,A6,A7,A8,A9,A10;
case ((f^g).(n+len f))`2 = 8;
then consider i,r,t,x such that A11: 1 <= i & i < n and
A12: (g.i)`1 = r => t & not x in still_not-bound_in r &
(g.n)`1 = r => All(x,t) by A2,A3,Def4;
A13: 1 <= len f+i & len f+i < n+len f by A11,NAT_1:37,REAL_1:53;
i <= len g by A1,A11,AXIOMS:22;
then i in Seg(len g) by A11,FINSEQ_1:3;
then i in dom g by FINSEQ_1:def 3;
then g.i = (f^g).(len f+i) by FINSEQ_1:def 7;
hence thesis by A3,A12,A13;
case ((f^g).(n+len f))`2 = 9;
then consider i,x,y,s such that A14: 1 <= i & i < n and
A15: s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x = (g.i)`1 & (g.n)`1 = s.y by A2,A3,Def4;
A16: 1 <= len f+i & len f+i < n+len f by A14,NAT_1:37,REAL_1:53;
i <= len g by A1,A14,AXIOMS:22;
then i in Seg(len g) by A14,FINSEQ_1:3;
then i in dom g by FINSEQ_1:def 3;
then g.i = (f^g).(len f+i) by FINSEQ_1:def 7;
hence thesis by A3,A15,A16;
end;
theorem Th62:
f is_a_proof_wrt X & g is_a_proof_wrt X implies f^g is_a_proof_wrt X
proof
assume that A1: f is_a_proof_wrt X and
A2: g is_a_proof_wrt X;
f <> {} by A1,Def5;
hence f^g <> {} by FINSEQ_1:48;
let n such that A3: 1 <= n & n <= len(f^g);
now per cases;
suppose A4: n <= len f;
then f,n is_a_correct_step_wrt X by A1,A3,Def5;
hence (f^g),n is_a_correct_step_wrt X by A3,A4,Th60;
suppose A5: len f < n;
then reconsider k=n - len f as Nat by EQREL_1:1;
A6: k + len f = n + (- len f) + len f by XCMPLX_0:def 8
.= n + (- len f + len f) by XCMPLX_1:1
.= n + 0 by XCMPLX_0:def 6
.= n;
then k + len f <= len g + len f & len f + 1 <= k + len f by A3,A5,
FINSEQ_1:35,NAT_1:38;
then A7: 1 <= k & k <= len g by REAL_1:53;
then g,k is_a_correct_step_wrt X by A2,Def5;
hence (f^g),n is_a_correct_step_wrt X by A6,A7,Th61;
end;
hence thesis;
end;
theorem
f is_a_proof_wrt X & X c= Y implies f is_a_proof_wrt Y
proof
assume that A1: f is_a_proof_wrt X and A2: X c= Y;
thus f <> {} by A1,Def5;
let n;
assume A3: 1 <= n & n <= len f;
then A4: f,n is_a_correct_step_wrt X by A1,Def5;
per cases by A3,Th45;
case (f.n)`2 = 0;
then (f.n)`1 in X by A4,Def4;
hence (f.n)`1 in Y by A2;
case (f.n)`2 = 1;
hence thesis by A4,Def4;
case (f.n)`2 = 2;
hence thesis by A4,Def4;
case (f.n)`2 = 3;
hence thesis by A4,Def4;
case (f.n)`2 = 4;
hence thesis by A4,Def4;
case (f.n)`2 = 5;
hence thesis by A4,Def4;
case (f.n)`2 = 6;
hence thesis by A4,Def4;
case (f.n)`2 = 7;
hence thesis by A4,Def4;
case (f.n)`2 = 8;
hence thesis by A4,Def4;
case (f.n)`2 = 9;
hence thesis by A4,Def4;
end;
theorem Th64: f is_a_proof_wrt X & 1 <= l & l <= len f implies (f.l)`1 in Cn(X)
proof
assume that A1: f is_a_proof_wrt X and A2: 1 <= l & l <= len f;
for n holds 1 <= n & n <= len f implies (f.n)`1 in Cn(X)
proof
defpred P[Nat] means 1 <= $1 & $1 <= len f implies (f.$1)`1 in Cn(X);
A3: for n st for k st k < n holds P[k] holds P[n]
proof
let n; assume
A4: for k st k < n holds P[k];
assume
A5: 1 <= n & n <= len f;
then A6: f,n is_a_correct_step_wrt X by A1,Def5;
now per cases by A5,Th45;
suppose (f.n)`2 = 0;
then (f.n)`1 in X & X c= Cn(X) by A6,Def4,Th38;
hence (f.n)`1 in Cn(X);
suppose (f.n)`2 = 1;
then (f.n)`1 = VERUM by A6,Def4;
hence (f.n)`1 in Cn(X) by Th27;
suppose (f.n)`2 = 2;
then ex p st (f.n)`1 = ('not' p => p) => p by A6,Def4;
hence (f.n)`1 in Cn(X) by Th28;
suppose (f.n)`2 = 3;
then ex p,q st (f.n)`1 = p => ('not' p => q) by A6,Def4;
hence (f.n)`1 in Cn(X) by Th29;
suppose (f.n)`2 = 4;
then ex p,q,r st (f.n)`1 = (p => q) => ('not'(q '&' r) => 'not'
(p '&' r))
by A6,Def4;
hence (f.n)`1 in Cn(X) by Th30;
suppose (f.n)`2 = 5;
then ex p,q st (f.n)`1 = p '&' q => q '&' p by A6,Def4;
hence (f.n)`1 in Cn(X) by Th31;
suppose (f.n)`2 = 6;
then ex p,x st (f.n)`1 = All(x,p) => p by A6,Def4;
hence (f.n)`1 in Cn(X) by Th33;
suppose (f.n)`2 = 7;
then consider i,j,p,q such that A7: 1 <= i & i < n & 1 <= j & j < i and
A8: p = (f.j)`1 and A9: q = (f.n)`1 and A10: (f.i)`1 = p => q
by A6,Def4;
A11: j < n by A7,AXIOMS:22;
1 <= i & i <= len f by A5,A7,AXIOMS:22;
then 1 <= i & i <= len f & 1 <= j & j <= len f by A7,AXIOMS:22;
then (f.j)`1 in Cn(X) & (f.i)`1 in Cn(X) by A4,A7,A11;
hence (f.n)`1 in Cn(X) by A8,A9,A10,Th32;
suppose (f.n)`2 = 8;
then consider i,p,q,x such that A12: 1 <= i & i < n and
A13: (f.i)`1 = p => q and A14: not x in still_not-bound_in p and
A15: (f.n)`1 = p => All(x,q) by A6,Def4;
1 <= i & i <= len f by A5,A12,AXIOMS:22;
then (f.i)`1 in Cn(X) by A4,A12;
hence (f.n)`1 in Cn(X) by A13,A14,A15,Th34;
suppose (f.n)`2 = 9;
then consider i,x,y,s such that
A16: 1 <= i & i < n and
A17: s.x in CQC-WFF & s.y in CQC-WFF and
A18: not x in still_not-bound_in s and A19:s.x = (f.i)`1 and A20:(f.n)`1
= s.y
by A6,Def4;
1 <= i & i <= len f by A5,A16,AXIOMS:22;
then (f.i)`1 in Cn(X) by A4,A16;
hence (f.n)`1 in Cn(X) by A17,A18,A19,A20,Th35;
end;
hence thesis;
end;
thus for n holds P[n] from Comp_Ind(A3);
end;
hence thesis by A2;
end;
definition let f;
assume A1: f <> {};
func Effect(f) -> Element of CQC-WFF
equals :Def6: (f.(len f))`1;
coherence
proof
len f <> 0 & 0 <= len f by A1,FINSEQ_1:25,NAT_1:18;
then 0+1 <= len f by NAT_1:38;
then len f in Seg len f & Seg len f = dom f by FINSEQ_1:3,def 3;
then f.(len f) in rng f & rng f c= [:CQC-WFF,Proof_Step_Kinds:]
by FINSEQ_1:def 4,FUNCT_1:def 5;
hence (f.(len f))`1 is Element of CQC-WFF by MCART_1:10;
end;
end;
canceled;
theorem Th66: f is_a_proof_wrt X implies Effect(f) in Cn(X)
proof
assume A1: f is_a_proof_wrt X;
then 1 <= len f & len f <= len f by Th58;
then (f.(len f))`1 in Cn(X) & f <> {}by A1,Def5,Th64;
hence thesis by Def6;
end;
:: ---------- A consequence as a set of all provable formulas
Lm3: for X holds {p: ex f st f is_a_proof_wrt X & Effect(f) = p} c= CQC-WFF
proof
let X;
defpred P[set] means ex f st f is_a_proof_wrt X & Effect(f) = $1;
thus {p: P[p] } c= CQC-WFF from Fr_Set0;
end;
theorem Th67: X c= {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let a; assume A1: a in X;
then reconsider p=a as Element of CQC-WFF;
reconsider pp=[p,0] as Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,
ZFMISC_1:106;
set f=<*pp*>;
A2: f <> {} by Lm1;
A3: len f = 1 & f.1 = pp by FINSEQ_1:57;
then (f.len f)`1 = p by MCART_1:7;
then A4: Effect(f) = p by A2,Def6;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt X
proof
assume 1 <= n & n <= len f;
then A5: n=1 by A3,AXIOMS:21;
then (f.1)`2 = 0 & (f.n)`1 in X by A1,A3,MCART_1:7;
hence f,n is_a_correct_step_wrt X by A5,Def4;
end;
then f is_a_proof_wrt X by A2,Def5;
hence thesis by A4;
end;
Lm4: for X holds VERUM in {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let X;
reconsider pp=[VERUM,1] as Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,
ZFMISC_1:106;
set f=<*pp*>;
A1: f <> {} by Lm1;
A2: len f = 1 & f.1 = pp by FINSEQ_1:57;
then (f.len f)`1 = VERUM by MCART_1:7;
then A3: Effect(f) = VERUM by A1,Def6;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt X
proof
assume 1 <= n & n <= len f;
then A4: n=1 by A2,AXIOMS:21;
then (f.1)`2 = 1 & (f.n)`1 = VERUM by A2,MCART_1:7;
hence f,n is_a_correct_step_wrt X by A4,Def4;
end;
then f is_a_proof_wrt X by A1,Def5;
hence thesis by A3;
end;
Lm5: for X holds
('not' p => p) => p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let X;
reconsider pp=[('not' p => p) => p,2] as
Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,ZFMISC_1:106;
set f=<*pp*>;
A1: f <> {} by Lm1;
A2: len f = 1 & f.1 = pp by FINSEQ_1:57;
then (f.len f)`1 = ('not' p => p) => p by MCART_1:7;
then A3: Effect(f) = ('not' p => p) => p by A1,Def6;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt X
proof
assume 1 <= n & n <= len f;
then A4: n=1 by A2,AXIOMS:21;
then (f.1)`2 = 2 & (f.n)`1 = ('not' p => p) => p by A2,MCART_1:7;
hence f,n is_a_correct_step_wrt X by A4,Def4;
end;
then f is_a_proof_wrt X by A1,Def5;
hence thesis by A3;
end;
Lm6: for X holds
p => ('not' p => q) in {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let X;
reconsider pp=[p => ('not' p => q),3] as
Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,ZFMISC_1:106;
set f=<*pp*>;
A1: f <> {} by Lm1;
A2: len f = 1 & f.1 = pp by FINSEQ_1:57;
then (f.len f)`1 = p => ('not' p => q) by MCART_1:7;
then A3: Effect(f) = p => ('not' p => q) by A1,Def6;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt X
proof
assume 1 <= n & n <= len f;
then A4: n=1 by A2,AXIOMS:21;
then (f.1)`2 = 3 & (f.n)`1 = p => ('not' p => q) by A2,MCART_1:7;
hence f,n is_a_correct_step_wrt X by A4,Def4;
end;
then f is_a_proof_wrt X by A1,Def5;
hence p => ('not' p => q) in
{F: ex f st f is_a_proof_wrt X & Effect(f) = F} by A3
;
end;
Lm7: for X holds (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in
{F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let X;
reconsider pp=[(p => q) => ('not'(q '&' r) => 'not'(p '&' r)),4] as
Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,ZFMISC_1:106;
set f=<*pp*>;
A1: f <> {} by Lm1;
A2: len f = 1 & f.1 = pp by FINSEQ_1:57;
then (f.len f)`1 = (p => q) => ('not'(q '&' r) => 'not'
(p '&' r)) by MCART_1:7;
then A3: Effect(f) = (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) by A1,
Def6;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt X
proof
assume 1 <= n & n <= len f;
then A4: n=1 by A2,AXIOMS:21;
then (f.1)`2 = 4 & (f.n)`1 = (p => q) => ('not'(q '&' r) => 'not'
(p '&' r))
by A2,MCART_1:7;
hence f,n is_a_correct_step_wrt X by A4,Def4;
end;
then f is_a_proof_wrt X by A1,Def5;
hence (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in
{t: ex f st f is_a_proof_wrt X & Effect(f) = t} by A3;
end;
Lm8: for X holds p '&' q => q '&' p in
{F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let X;
reconsider pp=[p '&' q => q '&' p,5] as
Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,ZFMISC_1:106;
set f=<*pp*>;
A1: f <> {} by Lm1;
A2: len f = 1 & f.1 = pp by FINSEQ_1:57;
then (f.len f)`1 = p '&' q => q '&' p by MCART_1:7;
then A3: Effect(f) = p '&' q => q '&' p by A1,Def6;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt X
proof
assume 1 <= n & n <= len f;
then A4: n=1 by A2,AXIOMS:21;
then (f.1)`2 = 5 & (f.n)`1 = p '&' q => q '&' p by A2,MCART_1:7;
hence f,n is_a_correct_step_wrt X by A4,Def4;
end;
then f is_a_proof_wrt X by A1,Def5;
hence p '&' q => q '&' p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
by A3;
end;
Lm9: for X holds p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} &
p => q in {G: ex f st f is_a_proof_wrt X & Effect(f) = G} implies
q in {H: ex f st f is_a_proof_wrt X & Effect(f) = H}
proof
let X;
assume that A1: p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} and
A2: p => q in {F: ex f st f is_a_proof_wrt X & Effect(f) = F};
ex t st t=p & ex f st f is_a_proof_wrt X & Effect(f)=t by A1;
then consider f such that A3: f is_a_proof_wrt X & Effect(f) = p;
ex r st r=p => q & ex f st f is_a_proof_wrt X &
Effect(f) = r by A2;
then consider g such that A4: g is_a_proof_wrt X & Effect(g) = p => q;
A5: f <> {} & g <> {} by A3,A4,Def5;
reconsider qq=[q,7] as Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,
ZFMISC_1:106;
set h=f^g^<*qq*>;
<*qq*> <> {} by Lm1;
then A6: h <> {} by FINSEQ_1:48;
A7: len h = len(f^g) + len(<*qq*>) by FINSEQ_1:35
.= len(f^g) + 1 by FINSEQ_1:57;
then A8: len h = len f + len g + 1 by FINSEQ_1:35;
h.(len h) = qq by A7,FINSEQ_1:59;
then (h.(len h))`1 = q by MCART_1:7;
then A9: Effect(h) = q by A6,Def6;
1 <= n & n <= len h implies h,n is_a_correct_step_wrt X
proof
assume A10: 1 <= n & n <= len h;
now per cases by A8,A10,NAT_1:26;
suppose n <= len f + len g;
then A11: 1 <= n & n <= len(f^g) by A10,FINSEQ_1:35;
f^g is_a_proof_wrt X by A3,A4,Th62;
then f^g,n is_a_correct_step_wrt X by A11,Def5;
hence h,n is_a_correct_step_wrt X by A11,Th60;
suppose A12: n = len h;
then h.n = qq by A7,FINSEQ_1:59;
then A13: (h.n)`2 = 7 & (h.n)`1 = q by MCART_1:7;
len f <> 0 by A3,Th58;
then len f in Seg(len f) by FINSEQ_1:5;
then len f in dom f & h = f^(g^<*qq*>)
by FINSEQ_1:45,def 3;
then A14: (h.len f)`1 = (f.len f)`1 by FINSEQ_1:def 7
.= p by A3,A5,Def6;
dom g = Seg(len g) & len g <> 0 by A4,Th58,FINSEQ_1:def 3;
then A15: len g in dom g by FINSEQ_1:5;
1 <= len f & len f <= len f + len g by A3,Th58,NAT_1:29;
then len f + len g <> 0 by AXIOMS:22;
then len f + len g in Seg(len f + len g) by FINSEQ_1:5;
then len f + len g in Seg(len(f^g)) by FINSEQ_1:35;
then len f + len g in dom(f^g) by FINSEQ_1:def 3;
then A16: (h.(len f + len g))`1 = ((f^g).(len f + len g))`1
by FINSEQ_1:def 7
.= (g.len g)`1 by A15,FINSEQ_1:def 7
.= p => q by A4,A5,Def6;
1 <= len g & len f <= len f by A4,Th58;
then len f < len f + 1 & len f + 1 <= len f + len g
by NAT_1:38,REAL_1:55;
then A17: 1 <= len f & len f < len f + len g by A3,Th58,AXIOMS:22;
then 1 <= len f + len g & len f + len g < n by A8,A12,NAT_1:37,38;
hence h,n is_a_correct_step_wrt X by A13,A14,A16,A17,Def4;
end;
hence thesis;
end;
then h is_a_proof_wrt X by A6,Def5;
hence q in {H: ex f st f is_a_proof_wrt X & Effect(f) = H} by A9;
end;
Lm10: for X holds
All(x,p) => p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let X;
reconsider pp=[All(x,p) => p,6] as
Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,ZFMISC_1:106;
set f=<*pp*>;
A1: f <> {} by Lm1;
A2: len f = 1 & f.1 = pp by FINSEQ_1:57;
then (f.len f)`1 = All(x,p) => p by MCART_1:7;
then A3: Effect(f) = All(x,p) => p by A1,Def6;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt X
proof
assume 1 <= n & n <= len f;
then A4: n=1 by A2,AXIOMS:21;
then (f.1)`2 = 6 & (f.n)`1 = All(x,p) => p by A2,MCART_1:7;
hence f,n is_a_correct_step_wrt X by A4,Def4;
end;
then f is_a_proof_wrt X by A1,Def5;
hence All(x,p) => p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} by A3
;
end;
Lm11: for X holds
p => q in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} &
not x in still_not-bound_in p implies
p => All(x,q) in {G: ex f st f is_a_proof_wrt X & Effect(f) = G}
proof
let X;
assume that A1: p => q in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} and
A2: not x in still_not-bound_in p;
ex t st t=p => q & ex f st f is_a_proof_wrt X &
Effect(f) = t by A1;
then consider f such that A3: f is_a_proof_wrt X & Effect(f) = p => q;
A4: f <> {} by A3,Def5;
reconsider qq=[p => All(x,q),8] as
Element of [:CQC-WFF,Proof_Step_Kinds:] by Th43,ZFMISC_1:106;
set h = f^<*qq*>;
<*qq*> <> {} by Lm1;
then A5: h <> {} by FINSEQ_1:48;
A6: len h = len f + len <*qq*> by FINSEQ_1:35
.= len f + 1 by FINSEQ_1:56;
1 <= n & n <= len h implies h,n is_a_correct_step_wrt X
proof
assume A7: 1 <= n & n <= len h;
now per cases by A6,A7,NAT_1:26;
suppose A8: n <= len f;
then f,n is_a_correct_step_wrt X by A3,A7,Def5;
hence h,n is_a_correct_step_wrt X by A7,A8,Th60;
suppose A9: n = len h;
then h.n = qq by A6,FINSEQ_1:59;
then A10: (h.n)`2 = 8 & (h.n)`1 = p => All(x,q) by MCART_1:7;
len f <> 0 by A3,Th58;
then len f in Seg(len f) by FINSEQ_1:5;
then len f in dom f by FINSEQ_1:def 3;
then A11: (h.len f)`1 = (f.len f)`1 by FINSEQ_1:def 7
.= p => q by A3,A4,Def6;
1 <= len f & len f < n by A3,A6,A9,Th58,NAT_1:38;
hence h,n is_a_correct_step_wrt X by A2,A10,A11,Def4;
end;
hence thesis;
end;
then A12: h is_a_proof_wrt X by A5,Def5;
Effect(h) = (h.(len f + 1))`1 by A5,A6,Def6
.= qq`1 by FINSEQ_1:59
.= p => All(x,q) by MCART_1:7;
hence p => All(x,q) in
{G: ex f st f is_a_proof_wrt X & Effect(f) = G} by A12;
end;
Lm12: for X holds s.x in CQC-WFF & s.y in CQC-WFF &
not x in still_not-bound_in s &
s.x in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} implies
s.y in {G: ex f st f is_a_proof_wrt X & Effect(f) = G}
proof
let X;
assume that A1: s.x in CQC-WFF & s.y in CQC-WFF and
A2: not x in still_not-bound_in s and
A3: s.x in {F: ex f st f is_a_proof_wrt X & Effect(f) = F};
ex t st t=s.x & ex f st f is_a_proof_wrt X &
Effect(f) = t by A3;
then consider f such that A4: f is_a_proof_wrt X & Effect(f) = s.x;
A5: f <> {} by A4,Def5;
reconsider qq=[s.y,9] as Element of [:CQC-WFF,Proof_Step_Kinds:] by A1,Th43,
ZFMISC_1:106;
set h = f^<*qq*>;
<*qq*> <> {} by Lm1;
then A6: h <> {} by FINSEQ_1:48;
A7: len h = len f + len <*qq*> by FINSEQ_1:35
.= len f + 1 by FINSEQ_1:56;
1 <= n & n <= len h implies h,n is_a_correct_step_wrt X
proof
assume A8:1 <= n & n <= len h;
now per cases by A7,A8,NAT_1:26;
suppose A9: n <= len f;
then f,n is_a_correct_step_wrt X by A4,A8,Def5;
hence h,n is_a_correct_step_wrt X by A8,A9,Th60;
suppose A10: n = len h;
then h.n = qq by A7,FINSEQ_1:59;
then A11: (h.n)`2 = 9 & (h.n)`1 = s.y by MCART_1:7;
len f <> 0 by A4,Th58;
then len f in Seg(len f) by FINSEQ_1:5;
then len f in dom f by FINSEQ_1:def 3;
then A12: (h.len f)`1 = (f.len f)`1 by FINSEQ_1:def 7
.= s.x by A4,A5,Def6;
1 <= len f & len f < n by A4,A7,A10,Th58,NAT_1:38;
hence h,n is_a_correct_step_wrt X by A1,A2,A11,A12,Def4;
end;
hence thesis;
end;
then A13: h is_a_proof_wrt X by A6,Def5;
Effect(h) = (h.(len f + 1))`1 by A6,A7,Def6
.= qq`1 by FINSEQ_1:59
.= s.y by MCART_1:7;
hence thesis by A13;
end;
theorem Th68: for X holds Y = {p: ex f st f is_a_proof_wrt X & Effect(f) = p}
implies Y is_a_theory
proof
let X;
assume A1: Y = {p: ex f st f is_a_proof_wrt X & Effect(f) = p};
hence VERUM in Y by Lm4;
let p,q,r,s,x,y;
thus ('not' p => p) => p in Y by A1,Lm5;
thus p => ('not' p => q) in Y by A1,Lm6;
thus (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in Y by A1,Lm7;
thus p '&' q => q '&' p in Y by A1,Lm8;
thus p in Y & p => q in Y implies q in Y by A1,Lm9;
thus All(x,p) => p in Y by A1,Lm10;
thus p => q in Y & not x in still_not-bound_in p implies p => All(x,q) in Y
by A1,Lm11;
thus s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x in Y implies s.y in Y by A1,Lm12;
end;
Lm13: for X holds {p: ex f st f is_a_proof_wrt X & Effect(f) = p} c= Cn(X)
proof
let X; let a;
assume a in {p: ex f st f is_a_proof_wrt X & Effect(f) = p};
then ex q st q=a & ex f st f is_a_proof_wrt X & Effect(f) = q;
hence thesis by Th66;
end;
theorem Th69:
for X holds {p: ex f st f is_a_proof_wrt X & Effect(f) = p} = Cn(X)
proof
let X;
set PX = {p: ex f st f is_a_proof_wrt X & Effect(f) = p};
A1: PX c= Cn(X) by Lm13;
reconsider PX as Subset of CQC-WFF by Lm3;
X c= PX & PX is_a_theory by Th67,Th68;
then Cn(X) c= {p: ex f st f is_a_proof_wrt X & Effect(f) = p} by Th37;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th70: p in Cn(X) iff ex f st f is_a_proof_wrt X & Effect(f) = p
proof
thus p in Cn(X) implies ex f st f is_a_proof_wrt X & Effect(f) = p
proof
assume p in Cn(X);
then p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} by Th69;
then ex F st F=p & ex f st f is_a_proof_wrt X &
Effect(f) = F;
hence thesis;
end;
thus (ex f st f is_a_proof_wrt X & Effect(f) = p) implies p in Cn(X)
proof
given f such that A1: f is_a_proof_wrt X and A2: Effect(f) = p;
p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} by A1,A2;
hence thesis by Th69;
end;
end;
theorem p in Cn(X) implies ex Y st Y c= X & Y is finite & p in Cn(Y)
proof
assume p in Cn(X);
then consider f such that
A1: f is_a_proof_wrt X and A2: Effect(f) = p by Th70;
A3: f <> {} by A1,Def5;
rng f is finite & Proof_Step_Kinds is finite &
rng f c= [:CQC-WFF,Proof_Step_Kinds:] by Def3,Th12,FINSEQ_1:def 4;
then consider A being set such that A4: A is finite & A c= CQC-WFF &
rng f c= [:A,Proof_Step_Kinds:] by Th14;
reconsider Z=A as Subset of CQC-WFF by A4;
take Y = Z /\ X;
thus Y c= X by XBOOLE_1:17;
thus Y is finite by A4,FINSET_1:15;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt Y
proof
assume A5: 1 <= n & n <= len f;
then A6: f,n is_a_correct_step_wrt X by A1,Def5;
per cases by A5,Th45;
case (f.n)`2 = 0;
then A7: (f.n)`1 in X by A6,Def4;
n in Seg(len f) by A5,FINSEQ_1:3;
then n in dom f by FINSEQ_1:def 3;
then f.n in rng f by FUNCT_1:def 5;
then (f.n)`1 in A by A4,MCART_1:10;
hence (f.n)`1 in Y by A7,XBOOLE_0:def 3;
case (f.n)`2 = 1;
hence (f.n)`1 = VERUM by A6,Def4;
case (f.n)`2 = 2;
hence ex p st (f.n)`1 = ('not' p => p) => p by A6,Def4;
case (f.n)`2 = 3;
hence ex p,q st (f.n)`1 = p => ('not' p => q) by A6,Def4;
case (f.n)`2 = 4;
hence ex p,q,r st (f.n)`1 = (p => q) => ('not'(q '&' r) => 'not'
(p '&' r))
by A6,Def4;
case (f.n)`2 = 5;
hence ex p,q st (f.n)`1 = p '&' q => q '&' p by A6,Def4;
case (f.n)`2 = 6;
hence ex p,x st (f.n)`1 = All(x,p) => p by A6,Def4;
case (f.n)`2 = 7;
hence ex i,j,p,q st 1 <= i & i < n & 1 <= j & j < i & p = (f.j)`1 &
q = (f.n)`1 & (f.i)`1 = p => q by A6,Def4;
case (f.n)`2 = 8;
hence ex i,p,q,x st 1 <= i & i < n & (f.i)`1 = p => q &
not x in still_not-bound_in p & (f.n)`1 = p => All(x,q) by A6,Def4;
case (f.n)`2 = 9;
hence ex i,x,y,s st 1 <= i & i < n & s.x in CQC-WFF & s.y in CQC-WFF &
not x in still_not-bound_in s & s.x = (f.i)`1 & (f.n)`1 = s.y
by A6,Def4;
end;
then f is_a_proof_wrt Y by A3,Def5;
then p in {q: ex f st f is_a_proof_wrt Y & Effect(f) = q} by A2;
hence p in Cn(Y) by Th69;
end;
:: --------- TAUT - the set of all tautologies
definition
canceled;
func TAUT -> Subset of CQC-WFF equals
:Def8: Cn({}(CQC-WFF));
correctness;
end;
canceled 2;
theorem Th74: T is_a_theory implies TAUT c= T
proof
assume A1: T is_a_theory;
{}(CQC-WFF) c= T by XBOOLE_1:2;
then Cn({}(CQC-WFF)) c= Cn(T) by Th39;
hence thesis by A1,Def8,Th41;
end;
theorem Th75: TAUT c= Cn(X)
proof
Cn(X) is_a_theory by Th36;
hence thesis by Th74;
end;
theorem Th76: TAUT is_a_theory by Def8,Th36;
theorem Th77: VERUM in TAUT by Def1,Th76;
theorem ('not' p => p) =>p in TAUT by Def1,Th76;
theorem p => ('not' p => q) in TAUT by Def1,Th76;
theorem (p => q) => ('not'(q '&' r) => 'not'
(p '&' r)) in TAUT by Def1,Th76;
theorem p '&' q => q '&' p in TAUT by Def1,Th76;
theorem p in TAUT & p => q in TAUT implies q in TAUT by Def1,Th76;
theorem All(x,p) => p in TAUT by Def8,Th33;
theorem p => q in TAUT & not x in still_not-bound_in p implies
p => All(x,q) in TAUT by Def8,Th34;
theorem s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x in TAUT implies s.y in TAUT by Def8,Th35;
:: --------- Relation of consequence of a set of formulas
definition let X,s;
pred X|-s means
:Def9: s in Cn(X);
end;
canceled;
theorem X |- VERUM
proof
VERUM in Cn(X) by Th27;
hence thesis by Def9;
end;
theorem X |- ('not' p => p) => p
proof
('not' p => p) => p in Cn(X) by Th28;
hence thesis by Def9;
end;
theorem X |- p => ('not' p => q)
proof
p => ('not' p => q) in Cn(X) by Th29;
hence thesis by Def9;
end;
theorem X |- (p => q) => ('not'(q '&' r) => 'not'(p '&' r))
proof
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in Cn(X) by Th30;
hence thesis by Def9;
end;
theorem X |- p '&' q => q '&' p
proof
p '&' q => q '&' p in Cn(X) by Th31;
hence thesis by Def9;
end;
theorem X |- p & X |- p => q implies X |- q
proof
assume X |- p & X |- p => q;
then p in Cn(X) & p => q in Cn(X) by Def9;
then q in Cn(X) by Th32;
hence thesis by Def9;
end;
theorem X |- All(x,p) => p
proof
All(x,p) => p in Cn(X) by Th33;
hence thesis by Def9;
end;
theorem X |- p => q & not x in still_not-bound_in p implies
X |- p => All(x,q)
proof
assume X |- p => q & not x in still_not-bound_in p;
then p => q in Cn(X) & not x in still_not-bound_in p by Def9;
then p => All(x,q) in Cn(X) by Th34;
hence thesis by Def9;
end;
theorem s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
X |- s.x implies X |- s.y
proof
assume s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
X |- (s.x);
then s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s
& s.x in Cn(X) by Def9;
then s.y in Cn(X) by Th35;
hence thesis by Def9;
end;
definition let s;
attr s is valid means
:Def10: {}(CQC-WFF)|-s;
synonym |-s;
end;
Lm14: |-s iff s in TAUT
proof
|-s iff {}(CQC-WFF)|-s by Def10;
hence |-s iff s in TAUT by Def8,Def9;
end;
definition let s;
redefine attr s is valid means s in TAUT;
compatibility by Lm14;
end;
canceled 2;
theorem |- p implies X|- p
proof
assume |- p;
then p in TAUT & TAUT c= Cn(X) by Lm14,Th75;
hence thesis by Def9;
end;
theorem |- VERUM by Lm14,Th77;
theorem |- ('not' p => p) =>p
proof
('not' p => p) =>p in TAUT by Def1,Th76;
hence thesis by Lm14;
end;
theorem |- p => ('not' p => q)
proof
p => ('not' p => q) in TAUT by Def1,Th76;
hence thesis by Lm14;
end;
theorem |- (p => q) => ('not'(q '&' r) => 'not'(p '&' r))
proof
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in TAUT by Def1,Th76;
hence thesis by Lm14;
end;
theorem |- p '&' q => q '&' p
proof
p '&' q => q '&' p in TAUT by Def1,Th76;
hence thesis by Lm14;
end;
theorem |- p & |- p => q implies |- q
proof
assume |- p & |- p => q;
then p in TAUT & p => q in TAUT by Lm14;
then q in TAUT by Def1,Th76;
hence thesis by Lm14;
end;
theorem |- All(x,p) => p
proof
All(x,p) => p in TAUT by Def8,Th33;
hence thesis by Lm14;
end;
theorem |- p => q & not x in still_not-bound_in p implies |- p => All(x,q)
proof
assume |- p => q & not x in still_not-bound_in p;
then p => q in TAUT & not x in still_not-bound_in p by Lm14;
then p => All(x,q) in TAUT by Def8,Th34;
hence thesis by Lm14;
end;
theorem s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
|- s.x implies |- s.y
proof
assume s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
|- s.x;
then s.x in CQC-WFF & s.y in CQC-WFF & not x in still_not-bound_in s &
s.x in TAUT by Lm14;
then s.y in TAUT by Def8,Th35;
hence thesis by Lm14;
end;