:: 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-2021 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;