:: A First-Order Predicate Calculus.
:: Axiomatics, the Consequence Operation and a Concept of Proof
:: by Agata Darmochwa{\l}
::
:: Received May 25, 1990
:: Copyright (c) 1990-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, XXREAL_0, ARYTM_3, XBOOLE_0, TARSKI, FINSET_1,
CARD_1, MCART_1, ZFMISC_1, CQC_LANG, XBOOLEAN, BVFUNC_2, QC_LANG1,
FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, ORDINAL4, ARYTM_1, CQC_THE1, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, XCMPLX_0,
FUNCT_1, NUMBERS, NAT_1, FINSET_1, FINSEQ_1, MCART_1, QC_LANG1, CQC_LANG,
XXREAL_0;
constructors XXREAL_0, XREAL_0, NAT_1, CQC_LANG, XTUPLE_0, NUMBERS;
registrations SUBSET_1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, FINSEQ_1,
CQC_LANG, ORDINAL1, CARD_1, NAT_1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FINSET_1, FINSEQ_1, MCART_1, FUNCT_1, NAT_1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, RELAT_1;
schemes NAT_1, FRAENKEL, XBOOLE_0;
begin
reserve Al for QC-alphabet;
reserve i,j,n,k,l for Nat;
reserve a for set;
:: --------- The axiomatic of a first-order calculus
reserve T,S,X,Y for Subset of CQC-WFF(Al);
reserve p,q,r,t,F,H,G for Element of CQC-WFF(Al);
reserve s for QC-formula of Al;
reserve x,y for bound_QC-variable of Al;
definition
let Al,T;
attr T is being_a_theory means
VERUM(Al) 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(Al) & s.y in CQC-WFF(Al) & not x in still_not-bound_in s
&
s.x in T implies s.y in T);
end;
::$CT 4
theorem
T is being_a_theory & S is being_a_theory implies T /\ S is being_a_theory
proof
assume that
A1: T is being_a_theory and
A2: S is being_a_theory;
VERUM(Al) in T & VERUM(Al) in S by A1,A2;
hence VERUM(Al) in T /\ S by XBOOLE_0:def 4;
let p,q,r,s,x,y;
('not' p => p) => p in T & ('not' p => p) => p in S by A1,A2;
hence ('not' p => p) => p in T /\ S by XBOOLE_0:def 4;
p => ('not' p => q) in T & p => ('not' p => q) in S by A1,A2;
hence p => ('not' p => q) in T /\ S by XBOOLE_0:def 4;
(
p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in T & (p => q) => ('not'(q
'&' r) => 'not'(p '&' r)) in S by A1,A2;
hence (p => q) => ('not'(q '&' r) => 'not'
(p '&' r)) in T /\ S by XBOOLE_0:def 4;
p '&' q => q '&' p in T & p '&' q => q '&' p in S by A1,A2;
hence p '&' q => q '&' p in T /\ S by XBOOLE_0:def 4;
A3: p in T & p => q in T implies q in T by A1;
p in S & p => q in S implies q in S by A2;
hence p in T /\ S & p => q in T /\ S implies q in T /\ S by A3,XBOOLE_0:def 4
;
All(x,p) => p in T & All(x,p) => p in S by A1,A2;
hence All(x,p) => p in T /\ S by XBOOLE_0:def 4;
A4: p => q in T & not x in still_not-bound_in p implies p => All(x,q) in T
by A1;
p => q in S & not x in still_not-bound_in p implies p => All(x,q) in S
by A2;
hence p => q in T /\ S & not x in still_not-bound_in p implies
p => All(x,q) in T /\ S by A4,XBOOLE_0:def 4;
A5: s.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & not x in still_not-bound_in s &
s.x in T implies s.y in T by A1;
s.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & not x in still_not-bound_in s & s.x
in S implies s.y in S by A2;
hence thesis by A5,XBOOLE_0:def 4;
end;
:: --------- The consequence operation
definition
let Al,X;
func Cn(X) -> Subset of CQC-WFF(Al) means
:Def2:
t in it iff for T st T is being_a_theory & X c= T holds t in T;
existence
proof
defpred P[object] means
for T st T is being_a_theory & X c= T holds $1 in T;
consider Y being set such that
A1: for a being object holds a in Y iff a in CQC-WFF(Al) & P[a]
from XBOOLE_0:sch 1;
Y c= CQC-WFF(Al)
by A1;
then reconsider Z=Y as Subset of CQC-WFF(Al);
take Z;
thus thesis by A1;
end;
uniqueness
proof
let Y,Z be Subset of CQC-WFF(Al) such that
A2: t in Y iff for T st T is being_a_theory & X c= T holds t in T and
A3: t in Z iff for T st T is being_a_theory & X c= T holds t in T;
for a being object holds a in Y iff a in Z
proof let a be object;
thus a in Y implies a in Z
proof
assume
A4: a in Y;
then reconsider t=a as Element of CQC-WFF(Al);
for T st T is being_a_theory & X c= T holds t in T by A2,A4;
hence thesis 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(Al);
for T st T is being_a_theory & X c= T holds t in T by A3,A5;
hence thesis by A2;
end;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th2:
VERUM(Al) in Cn(X)
proof
T is being_a_theory & X c= T implies VERUM(Al) in T;
hence thesis by Def2;
end;
theorem Th3:
('not' p => p) => p in Cn(X)
proof
T is being_a_theory & X c= T implies ('not' p => p) => p in T;
hence thesis by Def2;
end;
theorem Th4:
p => ('not' p => q) in Cn(X)
proof
T is being_a_theory & X c= T implies p => ('not' p => q) in T;
hence thesis by Def2;
end;
theorem Th5:
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in Cn(X)
proof
T is being_a_theory & X c= T implies
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in T;
hence thesis by Def2;
end;
theorem Th6:
p '&' q => q '&' p in Cn(X)
proof
T is being_a_theory & X c= T implies p '&' q => q '&' p in T;
hence thesis by Def2;
end;
theorem Th7:
p in Cn(X) & p => q in Cn(X) implies q in Cn(X)
proof
assume
A1: p in Cn(X) & p => q in Cn(X);
T is being_a_theory & X c= T implies q in T
proof
assume that
A2: T is being_a_theory and
A3: X c= T;
p in T & p => q in T by A1,A2,A3,Def2;
hence thesis by A2;
end;
hence thesis by Def2;
end;
theorem Th8:
All(x,p) => p in Cn(X)
proof
T is being_a_theory & X c= T implies All(x,p) => p in T;
hence thesis by Def2;
end;
theorem Th9:
p => q in Cn(X) & not x in still_not-bound_in p implies
p => All(x,q) in Cn(X)
proof
assume that
A1: p => q in Cn(X) and
A2: not x in still_not-bound_in p;
T is being_a_theory & X c= T implies p => All(x,q) in T
proof
assume that
A3: T is being_a_theory and
A4: X c= T;
p => q in T by A1,A3,A4,Def2;
hence thesis by A2,A3;
end;
hence thesis by Def2;
end;
theorem Th10:
s.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & not x in still_not-bound_in s &
s.x in Cn(X) implies s.y in Cn(X)
proof
assume that
A1: s.x in CQC-WFF(Al) and
A2: s.y in CQC-WFF(Al) and
A3: not x in still_not-bound_in s and
A4: s.x in Cn(X);
reconsider s1 = s.x as Element of CQC-WFF(Al) by A1;
reconsider q = s.y as Element of CQC-WFF(Al) by A2;
T is being_a_theory & X c= T implies q in T
proof
assume that
A5: T is being_a_theory and
A6: X c= T;
s1 in T by A4,A5,A6,Def2;
hence thesis by A3,A5;
end;
hence thesis by Def2;
end;
theorem Th11:
Cn(X) is being_a_theory
by Th2,Th3,Th4,Th5,Th6,Th7,Th8,Th9,Th10;
theorem Th12:
T is being_a_theory & X c= T implies Cn(X) c= T
by Def2;
theorem Th13:
X c= Cn(X)
proof
let a be object;
assume
A1: a in X;
then reconsider t=a as Element of CQC-WFF(Al);
for T st T is being_a_theory & X c= T holds t in T by A1;
hence thesis by Def2;
end;
theorem Th14:
X c= Y implies Cn(X) c= Cn(Y)
proof
assume
A1: X c= Y;
thus Cn(X) c= Cn(Y)
proof
let a be object;
assume
A2: a in Cn(X);
then reconsider t=a as Element of CQC-WFF(Al);
for T st T is being_a_theory & Y c= T holds t in T
proof
let T such that
A3: T is being_a_theory and
A4: Y c= T;
X c= T by A1,A4;
hence thesis by A2,A3,Def2;
end;
hence thesis by Def2;
end;
end;
Lm1: Cn(Cn(X)) c= Cn(X)
proof
let a be object;
assume
A1: a in Cn(Cn(X));
then reconsider t=a as Element of CQC-WFF(Al);
for T st T is being_a_theory & X c= T holds t in T
proof
let T;
assume that
A2: T is being_a_theory and
A3: X c= T;
Cn(X) c= T by A2,A3,Th12;
hence thesis by A1,A2,Def2;
end;
hence thesis by Def2;
end;
theorem
Cn(Cn(X)) = Cn(X)
by Lm1,Th13;
theorem Th16:
T is being_a_theory iff Cn(T) = T
proof
thus T is being_a_theory implies Cn(T) = T
proof
assume
A1: T is being_a_theory;
A2: T c= Cn(T) by Th13;
Cn(T) c= T
by A1,Def2;
hence thesis by A2;
end;
thus thesis by Th11;
end;
:: ---------- The notion of proof
definition
func Proof_Step_Kinds -> set equals
{k: k <= 9};
coherence;
end;
theorem Th17:
0 in Proof_Step_Kinds & ... & 9 in Proof_Step_Kinds;
registration
cluster Proof_Step_Kinds -> non empty;
coherence by Th17;
end;
theorem
Proof_Step_Kinds is finite
proof
Proof_Step_Kinds = succ Segm 9 by NAT_1:54;
hence thesis;
end;
reserve f,g for FinSequence of [:CQC-WFF(Al),Proof_Step_Kinds:];
theorem Th19:
for n being Nat holds 1 <= n & n <= len f implies
(f.n)`2 = 0 or ... or (f.n)`2 = 9
proof
let n be Nat;
assume
A1: 1 <= n & n <= len f;
dom f = Seg len f by FINSEQ_1:def 3;
then n in dom f by A1,FINSEQ_1:1;
then
rng f c= [:CQC-WFF(Al),Proof_Step_Kinds:] & f.n in rng f by FINSEQ_1:def 4
,FUNCT_1:def 3;
then (f.n)`2 in Proof_Step_Kinds by MCART_1:10;
then ex k st k = (f.n)`2 & k <= 9;
hence thesis;
end;
definition
let Al;
let PR be (FinSequence of [:CQC-WFF(Al),Proof_Step_Kinds:]),n be Nat,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(Al) 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(Al) & s.y in CQC-WFF(Al) &
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 Al,X,f;
pred f is_a_proof_wrt X means
f <> {} & for n st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt X;
end;
theorem
f is_a_proof_wrt X implies rng f <> {}
by RELAT_1:41;
theorem Th21:
f is_a_proof_wrt X implies 1 <= len f
proof
assume
f is_a_proof_wrt X;
then A1: f <> {};
0+1 <= len f by A1,NAT_1:13;
hence thesis;
end;
theorem
f is_a_proof_wrt X implies (f.1)`2 = 0 or ... or (f.1)`2 = 6
proof
assume
A1: f is_a_proof_wrt X;
then A2: 1 <= len f by Th21;
then A3: f,1 is_a_correct_step_wrt X by A1;
assume
A4: (f.1)`2 <> 0 & ... & (f.1)`2 <> 6;
(f.1)`2 = 0 or ... or (f.1)`2 = 9 by A2,Th19;
then per cases by A4;
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;
end;
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;
end;
suppose
(f.1)`2 = 9;
then ex i,x,y,s st 1 <= i & i < 1 &
s.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & not x in still_not-bound_in s &
s.x = (f.i)`1 & (f.1)`1 = s.y by A3,Def4;
hence contradiction;
end;
end;
theorem Th23:
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 that
A1: 1 <= n and
A2: n <= len f;
n in Seg(len f) by A1,A2,FINSEQ_1:1;
then n in dom f by FINSEQ_1:def 3;
then A3: (f^g).n = f.n by FINSEQ_1:def 7;
len(f^g) = len f + len g by FINSEQ_1:22;
then len f <= len(f^g) by NAT_1:11;
then A4: n <= len(f^g) by A2,XXREAL_0:2;
thus f,n is_a_correct_step_wrt X implies f^g,n is_a_correct_step_wrt X
proof
assume
A5: f,n is_a_correct_step_wrt X;
((f^g).n)`2 = 0 or ... or ((f^g).n)`2 = 9 by A1,A4,Th19;
then per cases;
case
((f^g).n)`2 = 0;
hence thesis by A3,A5,Def4;
end;
case
((f^g).n)`2 = 1;
hence thesis by A3,A5,Def4;
end;
case
((f^g).n)`2 = 2;
hence thesis by A3,A5,Def4;
end;
case
((f^g).n)`2 = 3;
hence thesis by A3,A5,Def4;
end;
case
((f^g).n)`2 = 4;
hence thesis by A3,A5,Def4;
end;
case
((f^g).n)`2 = 5;
hence thesis by A3,A5,Def4;
end;
case
((f^g).n)`2 = 6;
hence thesis by A3,A5,Def4;
end;
case
((f^g).n)`2 = 7;
then consider i,j,r,t such that
A6: 1 <= i and
A7: i < n and
A8: 1 <= j and
A9: j < i and
A10: r = (f.j)`1 & t = (f.n)`1 & (f.i)`1 = r => t by A3,A5,Def4;
A11: i <= len f by A2,A7,XXREAL_0:2;
then A12: j <= len f by A9,XXREAL_0:2;
A13: i in Seg(len f) by A6,A11,FINSEQ_1:1;
A14: j in Seg(len f) by A8,A12,FINSEQ_1:1;
A15: i in dom f by A13,FINSEQ_1:def 3;
A16: j in dom f by A14,FINSEQ_1:def 3;
A17: f.i = (f^g).i by A15,FINSEQ_1:def 7;
f.j = (f^g).j by A16,FINSEQ_1:def 7;
hence thesis by A3,A6,A7,A8,A9,A10,A17;
end;
case
((f^g).n)`2 = 8;
then consider i,r,t,x such that
A18: 1 <= i and
A19: i < n and
A20: (
f.i)`1 = r => t & not x in still_not-bound_in r & (f.n)`1 = r => All(x,
t)
by A3,A5,Def4;
i <= len f by A2,A19,XXREAL_0:2;
then i in Seg(len f) by A18,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A3,A18,A19,A20;
end;
case
((f^g).n)`2 = 9;
then consider i,x,y,s such that
A21: 1 <= i and
A22: i < n and
A23: s
.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & ( not x in still_not-bound_in s)&
s.x = (f.i)`1 & (f.n)`1 = s.y by A3,A5,Def4;
i <= len f by A2,A22,XXREAL_0:2;
then i in Seg(len f) by A21,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A3,A21,A22,A23;
end;
end;
assume
A24: f^g,n is_a_correct_step_wrt X;
(f.n)`2 = 0 or ... or (f.n)`2 = 9 by A1,A2,Th19;
then per cases;
case
(f.n)`2 = 0;
hence thesis by A3,A24,Def4;
end;
case
(f.n)`2 = 1;
hence thesis by A3,A24,Def4;
end;
case
(f.n)`2 = 2;
hence thesis by A3,A24,Def4;
end;
case
(f.n)`2 = 3;
hence thesis by A3,A24,Def4;
end;
case
(f.n)`2 = 4;
hence thesis by A3,A24,Def4;
end;
case
(f.n)`2 = 5;
hence thesis by A3,A24,Def4;
end;
case
(f.n)`2 = 6;
hence thesis by A3,A24,Def4;
end;
case
(f.n)`2 = 7;
then consider i,j,r,t such that
A25: 1 <= i and
A26: i < n and
A27: 1 <= j and
A28: j < i and
A29: r = ((f^g).j)`1 & t = ((f^g).n)`1 & ((f^g).i)`1 = r => t
by A3,A24,Def4;
A30: i <= len f by A2,A26,XXREAL_0:2;
then A31: j <= len f by A28,XXREAL_0:2;
A32: i in Seg(len f) by A25,A30,FINSEQ_1:1;
A33: j in Seg(len f) by A27,A31,FINSEQ_1:1;
A34: i in dom f by A32,FINSEQ_1:def 3;
A35: j in dom f by A33,FINSEQ_1:def 3;
A36: f.i = (f^g).i by A34,FINSEQ_1:def 7;
f.j = (f^g).j by A35,FINSEQ_1:def 7;
hence thesis by A3,A25,A26,A27,A28,A29,A36;
end;
case
(f.n)`2 = 8;
then consider i,r,t,x such that
A37: 1 <= i and
A38: i < n and
A39: ((f^g).i)`1 = r => t & not x in still_not-bound_in r & ((f^g).n)`1 = r
=> All(x,t)
by A3,A24,Def4;
i <= len f by A2,A38,XXREAL_0:2;
then i in Seg(len f) by A37,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A3,A37,A38,A39;
end;
case
(f.n)`2 = 9;
then consider i,x,y,s such that
A40: 1 <= i and
A41: i < n and
A42: s
.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & ( not x in still_not-bound_in s)&
s.x = ((f^g).i)`1 & ((f^g).n)`1 = s.y by A3,A24,Def4;
i <= len f by A2,A41,XXREAL_0:2;
then i in Seg(len f) by A40,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then f.i = (f^g).i by FINSEQ_1:def 7;
hence thesis by A3,A40,A41,A42;
end;
end;
theorem Th24:
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 and
A2: n <= len g and
A3: g,n is_a_correct_step_wrt X;
n in Seg(len g) by A1,A2,FINSEQ_1:1;
then n in dom g by FINSEQ_1:def 3;
then
A4: g.n = (f^g).(n+len f) by FINSEQ_1:def 7;
n + len f <= len f + len g by A2,XREAL_1:6;
then n+len f <= len(f^g) by FINSEQ_1:22;
then ((f^g).(n+len f))`2 = 0 or ... or ((f^g).(n+len f))`2 = 9
by A1,Th19,NAT_1:12;
then per cases;
case
((f^g).(n+len f))`2 = 0;
hence thesis by A3,A4,Def4;
end;
case
((f^g).(n+len f))`2 = 1;
hence thesis by A3,A4,Def4;
end;
case
((f^g).(n+len f))`2 = 2;
hence thesis by A3,A4,Def4;
end;
case
((f^g).(n+len f))`2 = 3;
hence thesis by A3,A4,Def4;
end;
case
((f^g).(n+len f))`2 = 4;
hence thesis by A3,A4,Def4;
end;
case
((f^g).(n+len f))`2 = 5;
hence thesis by A3,A4,Def4;
end;
case
((f^g).(n+len f))`2 = 6;
hence thesis by A3,A4,Def4;
end;
case
((f^g).(n+len f))`2 = 7;
then consider i,j,r,t such that
A5: 1 <= i and
A6: i < n and
A7: 1 <= j and
A8: j < i and
A9: r = (g.j)`1 & t = (g.n)`1 & (g.i)`1 = r => t by A3,A4,Def4;
A10: 1 <= i+len f & i+len f < n+len f by A5,A6,NAT_1:12,XREAL_1:6;
A11: 1 <= j+len f & j+len f < i+len f by A7,A8,NAT_1:12,XREAL_1:6;
A12: i <= len g by A2,A6,XXREAL_0:2;
then A13: j <= len g by A8,XXREAL_0:2;
A14: i in Seg(len g) by A5,A12,FINSEQ_1:1;
A15: j in Seg(len g) by A7,A13,FINSEQ_1:1;
A16: i in dom g by A14,FINSEQ_1:def 3;
A17: j in dom g by A15,FINSEQ_1:def 3;
A18: g.i = (f^g).(i+len f) by A16,FINSEQ_1:def 7;
g.j = (f^g).(j+len f) by A17,FINSEQ_1:def 7;
hence thesis by A4,A9,A10,A11,A18;
end;
case
((f^g).(n+len f))`2 = 8;
then consider i,r,t,x such that
A19: 1 <= i and
A20: i < n and
A21: (g.i)`1 = r => t & not x in still_not-bound_in r &
(g.n)`1 = r => All(x,t)
by A3,A4,Def4;
A22: 1 <= len f+i & len f+i < n+len f by A19,A20,NAT_1:12,XREAL_1:6;
i <= len g by A2,A20,XXREAL_0:2;
then i in Seg(len g) by A19,FINSEQ_1:1;
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 A4,A21,A22;
end;
case
((f^g).(n+len f))`2 = 9;
then consider i,x,y,s such that
A23: 1 <= i and
A24: i < n and
A25: s
.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & ( not x in still_not-bound_in s)&
s.x = (g.i)`1 & (g.n)`1 = s.y by A3,A4,Def4;
A26: 1 <= len f+i & len f+i < n+len f by A23,A24,NAT_1:12,XREAL_1:6;
i <= len g by A2,A24,XXREAL_0:2;
then i in Seg(len g) by A23,FINSEQ_1:1;
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 A4,A25,A26;
end;
end;
theorem Th25:
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;
hence f^g <> {};
let n such that
A3: 1 <= n and
A4: n <= len(f^g);
now per cases;
suppose
A5: n <= len f;
then f,n is_a_correct_step_wrt X by A1,A3;
hence thesis by A3,A5,Th23;
end;
suppose
A6: len f < n;
then reconsider k=n - len f as Element of NAT by NAT_1:21;
A7: k + len f <= len g + len f by A4,FINSEQ_1:22;
len f + 1 <= k + len f by A6,NAT_1:13;
then A8: 1 <= k by XREAL_1:6;
A9: k <= len g by A7,XREAL_1:6;
then k + len f = n & g,k is_a_correct_step_wrt X by A2,A8;
hence thesis by A8,A9,Th24;
end;
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;
let n;
assume
A3: 1 <= n & n <= len f;
then A4: f,n is_a_correct_step_wrt X by A1;
(f.n)`2 = 0 or ... or (f.n)`2 = 9 by A3,Th19;
then per cases;
case
(f.n)`2 = 0;
then (f.n)`1 in X by A4,Def4;
hence thesis by A2;
end;
case
(f.n)`2 = 1;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 2;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 3;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 4;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 5;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 6;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 7;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 8;
hence thesis by A4,Def4;
end;
case
(f.n)`2 = 9;
hence thesis by A4,Def4;
end;
end;
theorem Th27:
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 being Nat st for k being Nat st k < n holds P[k] holds P[n]
proof
let n be Nat;
assume
A4: for k being Nat st k < n holds P[k];
assume that
A5: 1 <= n and
A6: n <= len f;
A7: f,n is_a_correct_step_wrt X by A1,A5,A6;
now
(f.n)`2 = 0 or ... or (f.n)`2 = 9 by A5,A6,Th19;
then per cases;
suppose
(f.n)`2 = 0;
then A8: (f.n)`1 in X by A7,Def4;
X c= Cn(X) by Th13;
hence thesis by A8;
end;
suppose
(f.n)`2 = 1;
then (f.n)`1 = VERUM(Al) by A7,Def4;
hence thesis by Th2;
end;
suppose
(f.n)`2 = 2;
then ex p st (f.n)`1 = ('not' p => p) => p by A7,Def4;
hence thesis by Th3;
end;
suppose
(f.n)`2 = 3;
then ex p,q st (f.n)`1 = p => ('not' p => q) by A7,Def4;
hence thesis by Th4;
end;
suppose
(f.n)`2 = 4;
then ex p,q,r st (f.n)`1 = (p => q) => ('not'(q '&' r) => 'not'
(p '&' r)) by A7,Def4;
hence thesis by Th5;
end;
suppose
(f.n)`2 = 5;
then ex p,q st (f.n)`1 = p '&' q => q '&' p by A7,Def4;
hence thesis by Th6;
end;
suppose
(f.n)`2 = 6;
then ex p,x st (f.n)`1 = All(x,p) => p by A7,Def4;
hence thesis by Th8;
end;
suppose
(f.n)`2 = 7;
then consider i,j,p,q such that
A9: 1 <= i and
A10: i < n and
A11: 1 <= j and
A12: j < i and
A13: p = (f.j)`1 & q = (f.n)`1 & (f.i)`1 = p => q by A7,Def4;
A14: j < n by A10,A12,XXREAL_0:2;
A15: i <= len f by A6,A10,XXREAL_0:2;
then j <= len f by A12,XXREAL_0:2;
then A16: (f.j)`1 in Cn(X) by A4,A11,A14;
(f.i)`1 in Cn(X) by A4,A9,A10,A15;
hence thesis by A13,A16,Th7;
end;
suppose
(f.n)`2 = 8;
then consider i,p,q,x such that
A17: 1 <= i and
A18: i < n and
A19: (
f.i)`1 = p => q & not x in still_not-bound_in p & (f.n)`1 = p => All(x,
q)
by A7,Def4;
i <= len f by A6,A18,XXREAL_0:2;
hence thesis by A4,A17,A18,A19,Th9;
end;
suppose
(f.n)`2 = 9;
then consider i,x,y,s such that
A20: 1 <= i and
A21: i < n and
A22: s
.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & ( not x in still_not-bound_in s)&
s.x = (f.i)`1 & (f.n)`1 = s.y by A7,Def4;
i <= len f by A6,A21,XXREAL_0:2;
hence thesis by A4,A20,A21,A22,Th10;
end;
end;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 4(A3);
hence thesis;
end;
hence thesis by A2;
end;
definition
let Al,f;
assume
A1: f <> {};
func Effect(f) -> Element of CQC-WFF(Al) equals
:Def6:
(f.(len f))`1;
coherence
proof
0+1 <= len f by A1,NAT_1:13;
then A2: len f in Seg len f by FINSEQ_1:1;
Seg len f = dom f by FINSEQ_1:def 3;
then A3: f.(len f) in rng f by A2,FUNCT_1:def 3;
rng f c= [:CQC-WFF(Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
hence thesis by A3,MCART_1:10;
end;
end;
theorem Th28:
f is_a_proof_wrt X implies Effect(f) in Cn(X)
proof
assume
A1: f is_a_proof_wrt X;
then A2: 1 <= len f by Th21;
then A3: (f.(len f))`1 in Cn(X) by A1,Th27;
f <> {} by A2;
hence thesis by A3,Def6;
end;
:: ---------- A consequence as a set of all provable formulas
Lm2: for X holds {p: ex f st f is_a_proof_wrt X & Effect(f) = p} c= CQC-WFF(Al)
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(Al) from FRAENKEL:sch 10;
end;
theorem Th29:
X c= {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let a be object;
assume
A1: a in X;
then reconsider p=a as Element of CQC-WFF(Al);
reconsider pp=[p,0] as Element of [:CQC-WFF(Al),Proof_Step_Kinds:] by Th17,
ZFMISC_1:87;
set f=<*pp*>;
A2: len f = 1 by FINSEQ_1:40;
(f.len f)`1 = p by A2;
then A4: Effect(f) = p by 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 A2,XXREAL_0:1;
A6: (f.1)`2 = 0;
(f.n)`1 in X by A1,A5;
hence thesis by A5,A6,Def4;
end;
then f is_a_proof_wrt X;
hence thesis by A4;
end;
Lm3: for X holds VERUM(Al) in {F: ex f st f is_a_proof_wrt X & Effect(f) = F}
proof
let X;
reconsider pp=[VERUM(Al),1] as Element of [:CQC-WFF(Al),Proof_Step_Kinds:]
by Th17,ZFMISC_1:87;
set f=<*pp*>;
A1: len f = 1 by FINSEQ_1:40;
(f.len f)`1 = VERUM(Al) by A1;
then A3: Effect(f) = VERUM(Al) by 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 A1,XXREAL_0:1;
A5: (f.1)`2 = 1;
(f.n)`1 = VERUM(Al) by A4;
hence thesis by A4,A5,Def4;
end;
then f is_a_proof_wrt X;
hence thesis by A3;
end;
Lm4: 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(Al),Proof_Step_Kinds:] by Th17,ZFMISC_1:87;
set f=<*pp*>;
A1: len f = 1 by FINSEQ_1:40;
(f.len f)`1 = ('not' p => p) => p by A1;
then A3: Effect(f) = ('not' p => p) => p by 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 A1,XXREAL_0:1;
A5: (f.1)`2 = 2;
(f.n)`1 = ('not' p => p) => p by A4;
hence thesis by A4,A5,Def4;
end;
then f is_a_proof_wrt X;
hence thesis by A3;
end;
Lm5: 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(Al),Proof_Step_Kinds:] by Th17,ZFMISC_1:87;
set f=<*pp*>;
A1: len f = 1 by FINSEQ_1:40;
(f.len f)`1 = p => ('not' p => q) by A1;
then A3: Effect(f) = p => ('not' p => q) by 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 A1,XXREAL_0:1;
A5: (f.1)`2 = 3;
(f.n)`1 = p => ('not' p => q) by A4;
hence thesis by A4,A5,Def4;
end;
then f is_a_proof_wrt X;
hence thesis by A3;
end;
Lm6: 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(Al),Proof_Step_Kinds:] by Th17,ZFMISC_1:87;
set f=<*pp*>;
A1: len f = 1 by FINSEQ_1:40;
(f.len f)`1 = (p => q) => ('not'(q '&' r) => 'not'
(p '&' r)) by A1;
then A3: Effect(f) = (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) by 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 A1,XXREAL_0:1;
A5: (f.1)`2 = 4;
(f.n)`1 = (p => q) => ('not'(q '&' r) => 'not' (p '&' r)) by A4;
hence thesis by A4,A5,Def4;
end;
then f is_a_proof_wrt X;
hence thesis by A3;
end;
Lm7: 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(Al),Proof_Step_Kinds:] by Th17,ZFMISC_1:87;
set f=<*pp*>;
A1: len f = 1 by FINSEQ_1:40;
(f.len f)`1 = p '&' q => q '&' p by A1;
then A3: Effect(f) = p '&' q => q '&' p by 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 A1,XXREAL_0:1;
A5: (f.1)`2 = 5;
(f.n)`1 = p '&' q => q '&' p by A4;
hence thesis by A4,A5,Def4;
end;
then f is_a_proof_wrt X;
hence thesis by A3;
end;
Lm8: 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 and
A4: 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
A5: g is_a_proof_wrt X and
A6: Effect(g) = p => q;
reconsider qq=[q,7] as Element of [:CQC-WFF(Al),Proof_Step_Kinds:] by Th17,
ZFMISC_1:87;
set h=f^g^<*qq*>;
A7: len h = len(f^g) + len(<*qq*>) by FINSEQ_1:22
.= len(f^g) + 1 by FINSEQ_1:40;
then A8: len h = len f + len g + 1 by FINSEQ_1:22;
h.(len h) = qq by A7,FINSEQ_1:42;
then (h.(len h))`1 = q;
then A9: Effect(h) = q by Def6;
1 <= n & n <= len h implies h,n is_a_correct_step_wrt X
proof
assume that
A10: 1 <= n and
A11: n <= len h;
now per cases by A8,A11,NAT_1:8;
suppose
n <= len f + len g;
then A12: n <= len(f^g) by FINSEQ_1:22;
f^g is_a_proof_wrt X by A3,A5,Th25;
then f^g,n is_a_correct_step_wrt X by A10,A12;
hence thesis by A10,A12,Th23;
end;
suppose
A13: n = len h;
then h.n = qq by A7,FINSEQ_1:42;
then A14: (h.n)`2 = 7 & (h.n)`1 = q;
len f <> 0 by A3;
then len f in Seg(len f) by FINSEQ_1:3;
then A15: len f in dom f by FINSEQ_1:def 3;
h = f^(g^<*qq*>) by FINSEQ_1:32;
then A16: (h.len f)`1 = (f.len f)`1 by A15,FINSEQ_1:def 7
.= p by A4,A3,Def6;
dom g = Seg(len g) & len g <> 0 by A5,FINSEQ_1:def 3;
then A17: len g in dom g by FINSEQ_1:3;
1 <= len f & len f <= len f + len g by A3,Th21,NAT_1:11;
then len f + len g in Seg(len f + len g) by FINSEQ_1:3;
then len f + len g in Seg(len(f^g)) by FINSEQ_1:22;
then len f + len g in dom(f^g) by FINSEQ_1:def 3;
then A18: (h.(len f + len g))`1 = ((f^g).(len f + len g))`1 by
FINSEQ_1:def 7
.= (g.len g)`1 by A17,FINSEQ_1:def 7
.= p => q by A6,A5,Def6;
1 <= len g by A5,Th21;
then len f + 1 <= len f + len g by XREAL_1:7;
then A19: len f < len f + len g by NAT_1:13;
A20: 1 <= len f & 1 <= len f + len g by A3,Th21,NAT_1:12;
len f + len g < n by A8,A13,NAT_1:13;
hence thesis by A14,A16,A18,A19,A20,Def4;
end;
end;
hence thesis;
end;
then h is_a_proof_wrt X;
hence thesis by A9;
end;
Lm9: 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(Al),Proof_Step_Kinds:] by Th17,ZFMISC_1:87;
set f=<*pp*>;
A1: len f = 1 by FINSEQ_1:40;
(f.len f)`1 = All(x,p) => p by A1;
then A3: Effect(f) = All(x,p) => p by 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 A1,XXREAL_0:1;
A5: (f.1)`2 = 6;
(f.n)`1 = All(x,p) => p by A4;
hence thesis by A4,A5,Def4;
end;
then f is_a_proof_wrt X;
hence thesis by A3;
end;
Lm10: 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 and
A4: Effect(f) = p => q;
reconsider qq=[p => All(x,q),8] as
Element of [:CQC-WFF(Al),Proof_Step_Kinds:] by Th17,ZFMISC_1:87;
set h = f^<*qq*>;
A5: len h = len f + len <*qq*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
1 <= n & n <= len h implies h,n is_a_correct_step_wrt X
proof
assume that
A6: 1 <= n and
A7: n <= len h;
now per cases by A5,A7,NAT_1:8;
suppose
A8: n <= len f;
then f,n is_a_correct_step_wrt X by A3,A6;
hence thesis by A6,A8,Th23;
end;
suppose
A9: n = len h;
then h.n = qq by A5,FINSEQ_1:42;
then A10: (h.n)`2 = 8 & (h.n)`1 = p => All(x,q);
len f <> 0 by A3;
then len f in Seg(len f) by FINSEQ_1:3;
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 A4,A3,Def6;
A12: 1 <= len f by A3,Th21;
len f < n by A5,A9,NAT_1:13;
hence thesis by A2,A10,A11,A12,Def4;
end;
end;
hence thesis;
end;
then A13: h is_a_proof_wrt X;
Effect(h) = (h.(len f + 1))`1 by A5,Def6
.= qq`1 by FINSEQ_1:42
.= p => All(x,q);
hence thesis by A13;
end;
Lm11: for X holds s.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) &
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(Al) & s.y in CQC-WFF(Al) 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 and
A5: Effect(f) = s.x;
reconsider qq=[s.y,9] as Element of [:CQC-WFF(Al),Proof_Step_Kinds:]
by A1,Th17,ZFMISC_1:87;
set h = f^<*qq*>;
A6: len h = len f + len <*qq*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
1 <= n & n <= len h implies h,n is_a_correct_step_wrt X
proof
assume that
A7: 1 <= n and
A8: n <= len h;
now per cases by A6,A8,NAT_1:8;
suppose
A9: n <= len f;
then f,n is_a_correct_step_wrt X by A4,A7;
hence thesis by A7,A9,Th23;
end;
suppose
A10: n = len h;
then h.n = qq by A6,FINSEQ_1:42;
then A11: (h.n)`2 = 9 & (h.n)`1 = s.y;
len f <> 0 by A4;
then len f in Seg(len f) by FINSEQ_1:3;
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 A5,A4,Def6;
A13: 1 <= len f by A4,Th21;
len f < n by A6,A10,NAT_1:13;
hence thesis by A1,A2,A11,A12,A13,Def4;
end;
end;
hence thesis;
end;
then A14: h is_a_proof_wrt X;
Effect(h) = (h.(len f + 1))`1 by A6,Def6
.= qq`1 by FINSEQ_1:42
.= s.y;
hence thesis by A14;
end;
theorem Th30:
for X holds Y = {p: ex f st f is_a_proof_wrt X & Effect(f) = p}
implies Y is being_a_theory
by Lm3,Lm4,Lm5,Lm6,Lm7,Lm8,Lm9,Lm10,Lm11;
Lm12: for X holds {p: ex f st f is_a_proof_wrt X & Effect(f) = p} c= Cn(X)
proof
let X;
let a be object;
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 Th28;
end;
theorem Th31:
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 Lm12;
reconsider PX as Subset of CQC-WFF(Al) by Lm2;
X c= PX by Th29;
then
Cn(X) c= {p: ex f st f is_a_proof_wrt X & Effect(f) = p} by Th12,Th30;
hence thesis by A1;
end;
theorem Th32:
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 Th31;
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 & Effect(f) = p;
p in {F: ex f st f is_a_proof_wrt X & Effect(f) = F} by A1;
hence thesis by Th31;
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 Th32;
A3: f <> {} by A1;
consider A being set such that
A4: A is finite and
A5: A c= CQC-WFF(Al) and
A6: rng f c= [:A,Proof_Step_Kinds:] by FINSEQ_1:def 4,FINSET_1:14;
reconsider Z=A as Subset of CQC-WFF(Al) by A5;
take Y = Z /\ X;
thus Y c= X by XBOOLE_1:17;
thus Y is finite by A4;
1 <= n & n <= len f implies f,n is_a_correct_step_wrt Y
proof
assume
A7: 1 <= n & n <= len f;
then A8: f,n is_a_correct_step_wrt X by A1;
(f.n)`2 = 0 or ... or (f.n)`2 = 9 by A7,Th19;
then per cases;
case
(f.n)`2 = 0;
then A9: (f.n)`1 in X by A8,Def4;
n in Seg(len f) by A7,FINSEQ_1:1;
then n in dom f by FINSEQ_1:def 3;
then f.n in rng f by FUNCT_1:def 3;
then (f.n)`1 in A by A6,MCART_1:10;
hence thesis by A9,XBOOLE_0:def 4;
end;
case
(f.n)`2 = 1;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 2;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 3;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 4;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 5;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 6;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 7;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 8;
hence thesis by A8,Def4;
end;
case
(f.n)`2 = 9;
hence thesis by A8,Def4;
end;
end;
then f is_a_proof_wrt Y by A3;
then p in {q: ex f st f is_a_proof_wrt Y & Effect(f) = q} by A2;
hence thesis by Th31;
end;
:: --------- TAUT(Al) - the set of all tautologies
definition
let Al;
func TAUT(Al) -> Subset of CQC-WFF(Al) equals
Cn({}(CQC-WFF(Al)));
correctness;
end;
theorem Th34:
T is being_a_theory implies TAUT(Al) c= T
proof
assume
A1: T is being_a_theory;
Cn({}(CQC-WFF(Al))) c= Cn(T) by Th14,XBOOLE_1:2;
hence thesis by A1,Th16;
end;
theorem
TAUT(Al) c= Cn(X) by Th11,Th34;
theorem
TAUT(Al) is being_a_theory by Th11;
theorem Th37:
VERUM(Al) in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
theorem
('not' p => p) =>p in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
theorem
p => ('not' p => q) in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
theorem
(p => q) => ('not'(q '&' r) => 'not' (p '&' r)) in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
theorem
p '&' q => q '&' p in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
theorem
p in TAUT(Al) & p => q in TAUT(Al) implies q in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
theorem
All(x,p) => p in TAUT(Al) by Th8;
theorem
p => q in TAUT(Al) & not x in still_not-bound_in p implies
p => All(x,q) in TAUT(Al) by Th9;
theorem
s.x in CQC-WFF(Al) & s.y in CQC-WFF(Al) & not x in still_not-bound_in s
&
s.x in TAUT(Al) implies s.y in TAUT(Al) by Th10;
:: --------- Relation of consequence of a set of formulas
definition
let Al,X,s;
pred X|-s means
:Def8:
s in Cn(X);
end;
theorem
X |- VERUM(Al)
by Th2;
theorem
X |- ('not' p => p) => p
by Th3;
theorem
X |- p => ('not' p => q)
by Th4;
theorem
X |- (p => q) => ('not'(q '&' r) => 'not'(p '&' r))
by Th5;
theorem
X |- p '&' q => q '&' p
by Th6;
theorem
X |- p & X |- p => q implies X |- q
by Th7;
theorem
X |- All(x,p) => p
by Th8;
theorem
X |- p => q & not x in still_not-bound_in p implies X |- p => All(x,q)
by Th9;
theorem
s.y in CQC-WFF(Al) & not x in still_not-bound_in s &
X |- s.x implies X |- s.y
by Th10;
definition
let Al,s;
attr s is valid means
{}(CQC-WFF(Al))|-s;
end;
definition
let Al,s;
redefine attr s is valid means :: redefines valid (CQC_THE1, definition)
s in TAUT(Al);
compatibility by Def8;
end;
theorem
p is valid implies X |- p
proof
assume p is valid;
then A1: p in TAUT(Al);
TAUT(Al) c= Cn(X) by Th11,Th34;
hence thesis by A1;
end;
theorem
VERUM(Al) is valid
by Th37;
theorem
('not' p => p) =>p is valid
proof
('not' p => p) =>p in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
hence thesis;
end;
theorem
p => ('not' p => q) is valid
proof
p => ('not' p => q) in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
hence thesis;
end;
theorem
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) is valid
proof
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
hence thesis;
end;
theorem
p '&' q => q '&' p is valid
proof
p '&' q => q '&' p in TAUT(Al)
proof
TAUT(Al) is being_a_theory by Th11;
hence thesis;
end;
hence thesis;
end;
theorem
p is valid & p => q is valid implies q is valid
proof
A1: TAUT(Al) is being_a_theory by Th11;
assume p is valid & p => q is valid;
then p in TAUT(Al) & p => q in TAUT(Al);
then q in TAUT(Al) by A1;
hence thesis;
end;
theorem
All(x,p) => p is valid
by Th8;
theorem
p => q is valid & not x in still_not-bound_in p
implies p => All(x,q) is valid
by Th9;
theorem
s.y in CQC-WFF(Al) & not x in still_not-bound_in s &
s.x is valid implies s.y is valid
by Th10;