:: Transition of Consistency and Satisfiability under Language Extensions :: by Julian J. Schl\"oder and Peter Koepke :: :: Received May 7, 2012 :: Copyright (c) 2012-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, QC_LANG1, CQC_LANG, XBOOLE_0, VALUAT_1, FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4, CALCUL_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, REALSET1, SUBSTUT1, SUBSTUT2, ZF_LANG, ARYTM_1, CARD_3, ZFMISC_1, FINSET_1, MCART_1, NAT_1, MARGREL1, FUNCT_2, FUNCOP_1, QC_TRANS, FUNCT_4, CLASSES2, SUBLEMMA; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, NAT_1, ORDINAL1, CARD_3, FINSEQ_1, FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, NUMBERS, CQC_LANG, RELAT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2, CQC_SIM1, DOMAIN_1, XTUPLE_0, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2, CALCUL_1, CQC_THE1, GOEDELCP, MARGREL1, FUNCT_4, FUNCOP_1, HENMODEL; constructors SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG1, CQC_THE1, CQC_SIM1, SUBLEMMA, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1, CARD_1, WELLORD2, GOEDELCP, VALUAT_1, MARGREL1, CQC_LANG, QC_LANG3, FUNCT_4, FUNCOP_1, SUBSTUT1, PARTFUN1; registrations SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, HENMODEL, FINSEQ_1, FINSET_1, CARD_3, XBOOLE_0, QC_LANG1, CQC_LANG, MARGREL1, CARD_1, GOEDELCP, FUNCOP_1, SUBLEMMA, SUBSTUT1, XTUPLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Language Extensions reserve Al for QC-alphabet; reserve PHI for Consistent Subset of CQC-WFF(Al), p,q,r,s for Element of CQC-WFF(Al), A for non empty set, J for interpretation of Al,A, v for Element of Valuations_in(Al,A), m,n,i,j,k for Nat, l for CQC-variable_list of k,Al, P for QC-pred_symbol of k,Al, x,y,z for bound_QC-variable of Al, b for QC-symbol of Al, PR for FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:]; definition let Al; let Al2 be QC-alphabet; attr Al2 is Al-expanding means :: QC_TRANS:def 1 Al c= Al2; end; registration let Al; cluster Al-expanding for QC-alphabet; end; registration let Al1,Al2 be countable QC-alphabet; cluster countable Al1-expanding Al2-expanding for QC-alphabet; end; definition let Al,Al2 be QC-alphabet; let P be Subset of CQC-WFF(Al); attr P is Al2-Consistent means :: QC_TRANS:def 2 for S being Subset of CQC-WFF(Al2) st P=S holds S is Consistent; end; registration let Al; cluster non empty Consistent for Subset of CQC-WFF(Al); end; registration let Al; cluster Consistent -> Al-Consistent for Subset of CQC-WFF(Al); cluster Al-Consistent -> Consistent for Subset of CQC-WFF(Al); end; reserve Al2 for Al-expanding QC-alphabet, J2 for interpretation of Al2,A, Jp for interpretation of Al,A, v2 for Element of Valuations_in(Al2,A), vp for Element of Valuations_in(Al,A); theorem :: QC_TRANS:1 the_arity_of P = len l; theorem :: QC_TRANS:2 QC-symbols(Al) c= QC-symbols(Al2); theorem :: QC_TRANS:3 QC-pred_symbols(Al) c= QC-pred_symbols(Al2); theorem :: QC_TRANS:4 bound_QC-variables(Al) c= bound_QC-variables(Al2); theorem :: QC_TRANS:5 for k,l holds l is CQC-variable_list of k,Al2; theorem :: QC_TRANS:6 P is QC-pred_symbol of k,Al2; theorem :: QC_TRANS:7 for Al2 being Al-expanding QC-alphabet for p holds p is Element of CQC-WFF(Al2); definition let Al; let Al2 be Al-expanding QC-alphabet; let p be Element of CQC-WFF(Al); func Al2-Cast(p) -> Element of CQC-WFF(Al2) equals :: QC_TRANS:def 3 p; end; definition let Al; let Al2 be Al-expanding QC-alphabet; let x be bound_QC-variable of Al; func Al2-Cast(x) -> bound_QC-variable of Al2 equals :: QC_TRANS:def 4 x; end; definition let Al; let Al2 be Al-expanding QC-alphabet; let k; let P be QC-pred_symbol of k,Al; func Al2-Cast(P) -> QC-pred_symbol of k,Al2 equals :: QC_TRANS:def 5 P; end; definition let Al; let Al2 be Al-expanding QC-alphabet; let k; let l be CQC-variable_list of k,Al; func Al2-Cast(l) -> CQC-variable_list of k,Al2 equals :: QC_TRANS:def 6 l; end; theorem :: QC_TRANS:8 for p,r,x,P,l for Al2 being Al-expanding QC-alphabet holds Al2-Cast(VERUM(Al)) = VERUM(Al2) & Al2-Cast(P!l) = Al2-Cast(P)!Al2-Cast(l) & Al2-Cast('not' p) = 'not' (Al2-Cast(p)) & Al2-Cast(p '&' r) = (Al2-Cast(p)) '&' (Al2-Cast(r)) & Al2-Cast(All(x,p)) = All(Al2-Cast(x),Al2-Cast(p)); begin :: Downward Transfer of Consistency and Satisfiability theorem :: QC_TRANS:9 Jp = J2|QC-pred_symbols(Al) & vp = v2|bound_QC-variables(Al) implies (J2,v2 |= Al2-Cast(r) iff Jp,vp |= r); theorem :: QC_TRANS:10 for Al2 being Al-expanding QC-alphabet, THETA being Subset of CQC-WFF(Al2) st PHI c= THETA holds for A2 being non empty set, J2 being interpretation of Al2,A2, v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds ex A,J,v st J,v |= PHI; theorem :: QC_TRANS:11 for f being FinSequence of CQC-WFF(Al2),g being FinSequence of CQC-WFF(Al) st f=g holds Ant f = Ant g & Suc f = Suc g; theorem :: QC_TRANS:12 for p holds still_not-bound_in p = still_not-bound_in (Al2-Cast(p)); theorem :: QC_TRANS:13 for p2 being Element of CQC-WFF(Al2), S being CQC_Substitution of Al, S2 being CQC_Substitution of Al2, x2 being bound_QC-variable of Al2, x, p st p = p2 & S = S2 & x = x2 holds RestrictSub(x,p,S) = RestrictSub(x2,p2,S2); theorem :: QC_TRANS:14 for p2 being Element of CQC-WFF(Al2), S being finite CQC_Substitution of Al, S2 being finite CQC_Substitution of Al2, p st S = S2 & p = p2 holds upVar(S,p) = upVar(S2,p2); theorem :: QC_TRANS:15 for p2 being Element of CQC-WFF(Al2), S being CQC_Substitution of Al, S2 being CQC_Substitution of Al2, x2 being bound_QC-variable of Al2, x, p st p = p2 & S = S2 & x = x2 holds ExpandSub(x,p,RestrictSub(x,All(x,p),S)) = ExpandSub(x2,p2,RestrictSub(x2,All(x2,p2),S2)); theorem :: QC_TRANS:16 for Z being Element of CQC-Sub-WFF(Al), Z2 being Element of CQC-Sub-WFF(Al2) st Z`1 is universal & Z2`1 is universal & bound_in Z`1 = bound_in Z2`1 & the_scope_of Z`1 = the_scope_of Z2`1 & Z = Z2 holds S_Bound(@Z) = S_Bound(@Z2) ; theorem :: QC_TRANS:17 for p2 being Element of CQC-WFF(Al2),x2,y2 being bound_QC-variable of Al2, p,x,y st p=p2 & x=x2 & y=y2 holds p.(x,y) = p2.(x2,y2); theorem :: QC_TRANS:18 for PHI being Consistent Subset of CQC-WFF(Al2) st PHI is Subset of CQC-WFF(Al) holds PHI is Al-Consistent; begin :: Upward Transfer of Consistency and Satisfiability theorem :: QC_TRANS:19 for p ex Al1 being countable QC-alphabet st p is Element of CQC-WFF(Al1) & Al is Al1-expanding; theorem :: QC_TRANS:20 for PHI being finite Subset of CQC-WFF(Al) ex Al1 being countable QC-alphabet st PHI is finite Subset of CQC-WFF(Al1) & Al is Al1-expanding; registration let Al; let PHI be finite Subset of CQC-WFF(Al); cluster still_not-bound_in PHI -> finite; end; theorem :: QC_TRANS:21 for THETA being Subset of CQC-WFF(Al2) st PHI = THETA holds for A,J,v st J,v |= PHI ex A2 being non empty set, J2 being interpretation of Al2,A2, v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA; theorem :: QC_TRANS:22 for CHI being Subset of CQC-WFF(Al) st CHI c= PHI holds CHI is Consistent; theorem :: QC_TRANS:23 PHI is Al2-Consistent;