:: 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-2016 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;
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
:: CQC_THE1:def 1
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 :: CQC_THE1:5
T is being_a_theory & S is being_a_theory implies T /\ S is being_a_theory;
:: --------- The consequence operation
definition
let Al,X;
func Cn(X) -> Subset of CQC-WFF(Al) means
:: CQC_THE1:def 2
t in it iff for T st T is being_a_theory & X c= T holds t in T;
end;
theorem :: CQC_THE1:6
VERUM(Al) in Cn(X);
theorem :: CQC_THE1:7
('not' p => p) => p in Cn(X);
theorem :: CQC_THE1:8
p => ('not' p => q) in Cn(X);
theorem :: CQC_THE1:9
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) in Cn(X);
theorem :: CQC_THE1:10
p '&' q => q '&' p in Cn(X);
theorem :: CQC_THE1:11
p in Cn(X) & p => q in Cn(X) implies q in Cn(X);
theorem :: CQC_THE1:12
All(x,p) => p in Cn(X);
theorem :: CQC_THE1:13
p => q in Cn(X) & not x in still_not-bound_in p implies
p => All(x,q) in Cn(X);
theorem :: CQC_THE1:14
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);
theorem :: CQC_THE1:15
Cn(X) is being_a_theory;
theorem :: CQC_THE1:16
T is being_a_theory & X c= T implies Cn(X) c= T;
theorem :: CQC_THE1:17
X c= Cn(X);
theorem :: CQC_THE1:18
X c= Y implies Cn(X) c= Cn(Y);
theorem :: CQC_THE1:19
Cn(Cn(X)) = Cn(X);
theorem :: CQC_THE1:20
T is being_a_theory iff Cn(T) = T;
:: ---------- The notion of proof
definition
func Proof_Step_Kinds -> set equals
:: CQC_THE1:def 3
{k: k <= 9};
end;
theorem :: CQC_THE1:21
0 in Proof_Step_Kinds & ... & 9 in Proof_Step_Kinds;
registration
cluster Proof_Step_Kinds -> non empty;
end;
theorem :: CQC_THE1:22
Proof_Step_Kinds is finite;
reserve f,g for FinSequence of [:CQC-WFF(Al),Proof_Step_Kinds:];
theorem :: CQC_THE1:23
for n being Nat holds 1 <= n & n <= len f implies
(f.n)`2 = 0 or ... or (f.n)`2 = 9;
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
:: CQC_THE1:def 4
(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;
end;
definition
let Al,X,f;
pred f is_a_proof_wrt X means
:: CQC_THE1:def 5
f <> {} & for n st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt X;
end;
theorem :: CQC_THE1:24
f is_a_proof_wrt X implies rng f <> {};
theorem :: CQC_THE1:25
f is_a_proof_wrt X implies 1 <= len f;
theorem :: CQC_THE1:26
f is_a_proof_wrt X implies (f.1)`2 = 0 or ... or (f.1)`2 = 6;
theorem :: CQC_THE1:27
1 <= n & n <= len f implies
(f,n is_a_correct_step_wrt X iff f^g,n is_a_correct_step_wrt X);
theorem :: CQC_THE1:28
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;
theorem :: CQC_THE1:29
f is_a_proof_wrt X & g is_a_proof_wrt X implies f^g is_a_proof_wrt X;
theorem :: CQC_THE1:30
f is_a_proof_wrt X & X c= Y implies f is_a_proof_wrt Y;
theorem :: CQC_THE1:31
f is_a_proof_wrt X & 1 <= l & l <= len f implies (f.l)`1 in Cn(X);
definition
let Al,f;
assume
f <> {};
func Effect(f) -> Element of CQC-WFF(Al) equals
:: CQC_THE1:def 6
(f.(len f))`1;
end;
theorem :: CQC_THE1:32
f is_a_proof_wrt X implies Effect(f) in Cn(X);
theorem :: CQC_THE1:33
X c= {F: ex f st f is_a_proof_wrt X & Effect(f) = F};
theorem :: CQC_THE1:34
for X holds Y = {p: ex f st f is_a_proof_wrt X & Effect(f) = p}
implies Y is being_a_theory;
theorem :: CQC_THE1:35
for X holds {p: ex f st f is_a_proof_wrt X & Effect(f) = p} = Cn(X);
theorem :: CQC_THE1:36
p in Cn(X) iff ex f st f is_a_proof_wrt X & Effect(f) = p;
theorem :: CQC_THE1:37
p in Cn(X) implies ex Y st Y c= X & Y is finite & p in Cn(Y);
:: --------- TAUT(Al) - the set of all tautologies
definition
let Al;
func TAUT(Al) -> Subset of CQC-WFF(Al) equals
:: CQC_THE1:def 7
Cn({}(CQC-WFF(Al)));
end;
theorem :: CQC_THE1:38
T is being_a_theory implies TAUT(Al) c= T;
theorem :: CQC_THE1:39
TAUT(Al) c= Cn(X);
theorem :: CQC_THE1:40
TAUT(Al) is being_a_theory;
theorem :: CQC_THE1:41
VERUM(Al) in TAUT(Al);
theorem :: CQC_THE1:42
('not' p => p) =>p in TAUT(Al);
theorem :: CQC_THE1:43
p => ('not' p => q) in TAUT(Al);
theorem :: CQC_THE1:44
(p => q) => ('not'(q '&' r) => 'not' (p '&' r)) in TAUT(Al);
theorem :: CQC_THE1:45
p '&' q => q '&' p in TAUT(Al);
theorem :: CQC_THE1:46
p in TAUT(Al) & p => q in TAUT(Al) implies q in TAUT(Al);
theorem :: CQC_THE1:47
All(x,p) => p in TAUT(Al);
theorem :: CQC_THE1:48
p => q in TAUT(Al) & not x in still_not-bound_in p implies
p => All(x,q) in TAUT(Al);
theorem :: CQC_THE1:49
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);
:: --------- Relation of consequence of a set of formulas
definition
let Al,X,s;
pred X|-s means
:: CQC_THE1:def 8
s in Cn(X);
end;
theorem :: CQC_THE1:50
X |- VERUM(Al);
theorem :: CQC_THE1:51
X |- ('not' p => p) => p;
theorem :: CQC_THE1:52
X |- p => ('not' p => q);
theorem :: CQC_THE1:53
X |- (p => q) => ('not'(q '&' r) => 'not'(p '&' r));
theorem :: CQC_THE1:54
X |- p '&' q => q '&' p;
theorem :: CQC_THE1:55
X |- p & X |- p => q implies X |- q;
theorem :: CQC_THE1:56
X |- All(x,p) => p;
theorem :: CQC_THE1:57
X |- p => q & not x in still_not-bound_in p implies X |- p => All(x,q);
theorem :: CQC_THE1:58
s.y in CQC-WFF(Al) & not x in still_not-bound_in s &
X |- s.x implies X |- s.y;
definition
let Al,s;
attr s is valid means
:: CQC_THE1:def 9
{}(CQC-WFF(Al))|-s;
end;
definition
let Al,s;
redefine attr s is valid means
:: CQC_THE1:def 10
s in TAUT(Al);
end;
theorem :: CQC_THE1:59
p is valid implies X |- p;
theorem :: CQC_THE1:60
VERUM(Al) is valid;
theorem :: CQC_THE1:61
('not' p => p) =>p is valid;
theorem :: CQC_THE1:62
p => ('not' p => q) is valid;
theorem :: CQC_THE1:63
(p => q) => ('not'(q '&' r) => 'not'(p '&' r)) is valid;
theorem :: CQC_THE1:64
p '&' q => q '&' p is valid;
theorem :: CQC_THE1:65
p is valid & p => q is valid implies q is valid;
theorem :: CQC_THE1:66
All(x,p) => p is valid;
theorem :: CQC_THE1:67
p => q is valid & not x in still_not-bound_in p
implies p => All(x,q) is valid;
theorem :: CQC_THE1:68
s.y in CQC-WFF(Al) & not x in still_not-bound_in s &
s.x is valid implies s.y is valid;