:: A Sequent Calculus for First-Order Logic :: by Patrick Braselmann and Peter Koepke :: :: Received September 25, 2004 :: Copyright (c) 2004-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, CQC_LANG, QC_LANG1, XBOOLE_0, VALUAT_1, SUBSTUT1, FINSEQ_1, RELAT_1, ARYTM_3, XXREAL_0, CARD_1, NAT_1, TARSKI, FUNCT_1, ORDINAL4, FINSEQ_2, ZFMISC_1, CQC_THE1, MCART_1, XBOOLEAN, BVFUNC_2, ZF_MODEL, SUBSTUT2, SUBLEMMA, FUNCOP_1, FUNCT_4, FINSET_1, ORDINAL1, CALCUL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FINSEQ_1, RELAT_1, FUNCT_1, QC_LANG1, CARD_1, ORDINAL1, NUMBERS, FINSEQ_2, XXREAL_0, XCMPLX_0, NAT_1, FUNCOP_1, CQC_LANG, FINSET_1, VALUAT_1, CQC_THE1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, MCART_1, SUBSTUT1, SUBSTUT2, SUBLEMMA; constructors PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, CQC_THE1, SUBSTUT2, RELSET_1, XTUPLE_0, NUMBERS; registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, QC_LANG1, CQC_LANG, CARD_1, FINSEQ_2, RELAT_1, XTUPLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve Al for QC-alphabet; reserve a,b,c,d for object, i,j,k,m,n for Nat, p,q,r for Element of CQC-WFF(Al), x,y,y0 for bound_QC-variable of Al, X for Subset of CQC-WFF(Al), A for non empty set, J for interpretation of Al,A, v,w for Element of Valuations_in(Al,A), Sub for CQC_Substitution of Al, f,f1,g,h,h1 for FinSequence of CQC-WFF(Al); definition let D be non empty set, f be FinSequence of D; func Ant(f) -> FinSequence of D means :: CALCUL_1:def 1 for i st len f = i+1 holds it = f|(Seg i) if len f > 0 otherwise it = {}; end; definition let Al; let f be FinSequence of CQC-WFF(Al); func Suc(f) -> Element of CQC-WFF(Al) equals :: CALCUL_1:def 2 f.(len f) if len f > 0 otherwise VERUM(Al); end; definition let f be Relation, p be set; pred p is_tail_of f means :: CALCUL_1:def 3 p in rng f; end; definition let Al,f,g; pred f is_Subsequence_of g means :: CALCUL_1:def 4 ex N being Subset of NAT st f c= Seq (g|N); end; theorem :: CALCUL_1:1 f is_Subsequence_of g implies rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g|N); theorem :: CALCUL_1:2 len f > 0 implies len Ant(f)+1 = len f & len Ant(f) < len f; theorem :: CALCUL_1:3 len f > 0 implies f = Ant(f)^<*Suc(f)*> & rng f = rng Ant(f) \/ { Suc(f)}; theorem :: CALCUL_1:4 len f > 1 implies len Ant(f) > 0; theorem :: CALCUL_1:5 Suc(f^<*p*>) = p & Ant(f^<*p*>) = f; reserve fin,fin1 for FinSequence; theorem :: CALCUL_1:6 len fin <= len (fin^fin1) & len fin1 <= len (fin^fin1) & (fin <> {} implies 1 <= len fin & len fin1 < len (fin1^fin)); theorem :: CALCUL_1:7 Seq ((f^g)|dom f) = (f^g)|dom f; theorem :: CALCUL_1:8 f is_Subsequence_of f^g; theorem :: CALCUL_1:9 1 < len (fin^<*b*>^<*c*>); theorem :: CALCUL_1:10 1 <= len (fin^<*b*>) & len (fin^<*b*>) in dom (fin^<*b*>); theorem :: CALCUL_1:11 0 < m implies len (Sgm (Seg n \/ {n+m})) = n+1; theorem :: CALCUL_1:12 0 < m implies dom (Sgm (Seg n \/ {n+m})) = Seg (n+1); theorem :: CALCUL_1:13 0 < len f implies f is_Subsequence_of Ant(f)^g^<*Suc(f)*>; theorem :: CALCUL_1:14 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f^<*c,d*>).(len f + 1) = c & (f^<*c,d*>).(len f + 2) = d; begin :: A Sequent calculus definition let Al,f; func still_not-bound_in f -> Subset of bound_QC-variables(Al) means :: CALCUL_1:def 5 a in it iff ex i,p st i in dom f & p = f.i & a in still_not-bound_in p; end; definition let Al; func set_of_CQC-WFF-seq(Al) -> set means :: CALCUL_1:def 6 a in it iff a is FinSequence of CQC-WFF(Al); end; reserve PR,PR1 for FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:]; definition let Al,PR; let n be Nat; pred PR,n is_a_correct_step means :: CALCUL_1:def 7 ex f st Suc(f) is_tail_of Ant(f) & (PR.n)`1 = f if (PR.n)`2 = 0, ex f st (PR.n)`1 = f^<*VERUM(Al)*> if (PR.n)`2 = 1, ex i,f,g st 1 <= i & i < n & Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & (PR.i)`1 = f & (PR.n)`1 = g if (PR.n)`2 = 2, ex i,j,f,g st 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc( Ant(f)) = Suc(Ant(g)) & Suc(f) = Suc(g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(Ant (f))^<*Suc(f)*> = (PR.n)`1 if (PR.n)`2 = 3, ex i,j,f,g,p st 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc( f) = Suc(g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(Ant(f))^<*p*> = (PR.n)`1 if (PR .n)`2 = 4, ex i,j,f,g st 1 <= i & i < n & 1 <= j & j < i & Ant(f) = Ant(g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(f)^<*(Suc(f)) '&' (Suc(g))*> = (PR.n)`1 if (PR. n)`2 = 5, ex i,f,p,q st 1 <= i & i < n & p '&' q = Suc(f) & f = (PR.i)`1 & Ant( f)^<*p*> = (PR.n)`1 if (PR.n)`2 = 6, ex i,f,p,q st 1 <= i & i < n & p '&' q = Suc(f) & f = (PR.i)`1 & Ant(f)^<*q*>= (PR.n)`1 if (PR.n)`2 = 7, ex i,f,p,x,y st 1 <= i & i < n & Suc(f) = All(x,p) & f = (PR.i)`1 & Ant(f)^<*p.(x,y)*> = (PR.n) `1 if (PR.n)`2 = 8, ex i,f,p,x,y st 1 <= i & i < n & Suc(f) = p.(x,y) & not y in still_not-bound_in (Ant(f)) & not y in still_not-bound_in All(x,p) & f = (PR .i)`1 & Ant(f)^<*All(x,p)*> = (PR.n)`1 if (PR.n)`2 = 9; end; definition let Al,PR; attr PR is a_proof means :: CALCUL_1:def 8 PR <> {} & for n being Nat st 1 <= n & n <= len PR holds PR,n is_a_correct_step; end; definition let Al,f; pred |- f means :: CALCUL_1:def 9 ex PR st PR is a_proof & f = (PR.(len PR))`1; end; definition let Al,p,X; pred p is_formal_provable_from X means :: CALCUL_1:def 10 ex f st rng Ant(f) c= X & Suc (f) = p & |- f; end; definition let Al,X,A,J,v; pred J,v |= X means :: CALCUL_1:def 11 p in X implies J,v |= p; end; definition let Al,X,p; pred X |= p means :: CALCUL_1:def 12 J,v |= X implies J,v |= p; end; definition let Al,p; pred |= p means :: CALCUL_1:def 13 {}(CQC-WFF(Al)) |= p; end; definition let Al,f, A, J, v; pred J,v |= f means :: CALCUL_1:def 14 J,v |= rng(f); end; definition let Al, f, p; pred f |= p means :: CALCUL_1:def 15 J,v |= f implies J,v |= p; end; theorem :: CALCUL_1:15 Suc(f) is_tail_of Ant(f) implies Ant(f) |= Suc(f); theorem :: CALCUL_1:16 Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & Ant(f) |= Suc(f) implies Ant(g) |= Suc(g); theorem :: CALCUL_1:17 len f > 0 implies (J,v |= Ant(f) & J,v |= Suc(f) iff J,v |= f); theorem :: CALCUL_1:18 len f > 1 & len g > 1 & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc( Ant(f)) = Suc(Ant(g)) & Suc(f) = Suc(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g) implies Ant(Ant(f)) |= Suc(f); theorem :: CALCUL_1:19 len f > 1 & Ant(f) = Ant(g) & 'not' p = Suc(Ant(f)) & 'not' Suc( f) = Suc(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g) implies Ant(Ant(f)) |= p; theorem :: CALCUL_1:20 Ant(f) = Ant(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g) implies Ant(f) |= (Suc(f)) '&' (Suc(g)); theorem :: CALCUL_1:21 Ant(f) |= p '&' q implies Ant(f) |= p; theorem :: CALCUL_1:22 Ant(f) |= p '&' q implies Ant(f) |= q; theorem :: CALCUL_1:23 J,v |= [p,Sub] iff J,v |= p; reserve a for Element of A; theorem :: CALCUL_1:24 J,v |= p.(x,y) iff ex a st v.y = a & J,v.(x|a) |= p; theorem :: CALCUL_1:25 Suc(f) = All(x,p) & Ant(f) |= Suc(f) implies for y holds Ant(f) |= p.(x,y); theorem :: CALCUL_1:26 for X being set st X c= bound_QC-variables(Al) holds not x in X implies v.(x|a)|X = v|X; theorem :: CALCUL_1:27 for v,w holds v|still_not-bound_in f = w|still_not-bound_in f implies (J,v |= f implies J,w |= f); theorem :: CALCUL_1:28 not y in still_not-bound_in All(x,p) implies v.(y|a).(x|a)| still_not-bound_in p = v.(x|a)|still_not-bound_in p; theorem :: CALCUL_1:29 Suc(f) = p.(x,y) & Ant(f) |= Suc(f) & not y in still_not-bound_in Ant(f) & not y in still_not-bound_in All(x,p) implies Ant(f) |= All(x,p); theorem :: CALCUL_1:30 Ant(f^<*VERUM(Al)*>) |= Suc(f^<*VERUM(Al)*>); theorem :: CALCUL_1:31 for n being Nat holds 1 <= n & n <= len PR implies (PR.n)`2 = 0 or ... or (PR.n)`2 = 9; :: Theorem on the Correctness (Ebb et al, Chapter IV, Theorem 6.2) theorem :: CALCUL_1:32 p is_formal_provable_from X implies X |= p; begin :: Derived Rules theorem :: CALCUL_1:33 Suc(f) is_tail_of Ant(f) implies |- f; theorem :: CALCUL_1:34 for n being Nat holds 1 <= n & n <= len PR implies (PR,n is_a_correct_step iff PR^PR1,n is_a_correct_step); theorem :: CALCUL_1:35 1 <= n & n <= len PR1 & PR1,n is_a_correct_step implies (PR^PR1) ,(n+len PR) is_a_correct_step; theorem :: CALCUL_1:36 Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & |- f implies |- g; theorem :: CALCUL_1:37 1 < len f & 1 < len g & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc( Ant(f)) = Suc(Ant(g)) & Suc(f) = Suc(g) & |- f & |- g implies |- Ant(Ant(f))^<* Suc(f)*>; theorem :: CALCUL_1:38 len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc( f) = Suc(g) & |- f & |- g implies |- Ant(Ant(f))^<*p*>; theorem :: CALCUL_1:39 Ant(f) = Ant(g) & |- f & |- g implies |- Ant(f)^<*(Suc(f)) '&' ( Suc(g))*>; theorem :: CALCUL_1:40 p '&' q = Suc(f) & |- f implies |- Ant(f)^<*p*>; theorem :: CALCUL_1:41 p '&' q = Suc(f) & |- f implies |- Ant(f)^<*q*>; theorem :: CALCUL_1:42 Suc(f) = All(x,p) & |- f implies |- Ant(f)^<*p.(x,y)*>; theorem :: CALCUL_1:43 Suc(f) = p.(x,y) & not y in still_not-bound_in Ant(f) & not y in still_not-bound_in All(x,p) & |- f implies |- Ant(f)^<*All(x,p)*>; theorem :: CALCUL_1:44 |- f & |- Ant(f)^<*'not' Suc(f)*> implies |- Ant(f)^<*p*>; theorem :: CALCUL_1:45 1 <= len f & |- f & |- f^<*p*> implies |- Ant(f)^<*p*>; theorem :: CALCUL_1:46 |- f^<*p*>^<*q*> implies |- f^<*'not' q*>^<*'not' p*>; theorem :: CALCUL_1:47 |- f^<*'not' p*>^<*'not' q*> implies |- f^<*q*>^<*p*>; theorem :: CALCUL_1:48 |- f^<*'not' p*>^<*q*> implies |- f^<*'not' q*>^<*p*>; theorem :: CALCUL_1:49 |- f^<*p*>^<*'not' q*> implies |- f^<*q*>^<*'not' p*>; ::$CT theorem :: CALCUL_1:51 |- f^<*p*> implies |- f^<*p 'or' q*>; theorem :: CALCUL_1:52 |- f^<*q*> implies |- f^<*p 'or' q*>; theorem :: CALCUL_1:53 |- f^<*p*>^<*r*> & |- f^<*q*>^<*r*> implies |- f^<*p 'or' q*>^<* r*>; theorem :: CALCUL_1:54 |- f^<*p*> implies |- f^<*'not' 'not' p*>; theorem :: CALCUL_1:55 |- f^<*'not' 'not' p*> implies |- f^<*p*>; theorem :: CALCUL_1:56 |- f^<*p => q*> & |- f^<*p*> implies |- f^<*q*>; theorem :: CALCUL_1:57 ('not' p).(x,y) = 'not' (p.(x,y)); theorem :: CALCUL_1:58 (ex y st |- f^<*p.(x,y)*>) implies |- f^<*Ex(x,p)*>; theorem :: CALCUL_1:59 still_not-bound_in (f^g) = still_not-bound_in f \/ still_not-bound_in g; theorem :: CALCUL_1:60 still_not-bound_in <*p*> = still_not-bound_in p; theorem :: CALCUL_1:61 |- f^<*p.(x,y)*>^<*q*> & not y in still_not-bound_in (f^<*Ex(x,p)*>^<* q*>) implies |- f^<*Ex(x,p)*>^<*q*>; theorem :: CALCUL_1:62 still_not-bound_in f = union {still_not-bound_in p : ex i st i in dom f & p = f.i}; theorem :: CALCUL_1:63 still_not-bound_in f is finite; theorem :: CALCUL_1:64 card bound_QC-variables(Al) = card QC-symbols(Al) & not bound_QC-variables(Al) is finite; theorem :: CALCUL_1:65 ex x st not x in still_not-bound_in f; theorem :: CALCUL_1:66 |- f^<*All(x,p)*> implies |- f^<*All(x,'not' 'not' p)*>; theorem :: CALCUL_1:67 |- f^<*All(x,'not' 'not' p)*> implies |- f^<*All(x,p)*>; theorem :: CALCUL_1:68 |- f^<*All(x,p)*> iff |- f^<*'not' Ex(x,'not' p)*>; definition let f be FinSequence, p be set; redefine pred p is_tail_of f means :: CALCUL_1:def 16 ex i being Nat st i in dom f & f.i = p; end;