:: Substitution in First-Order Formulas -- Part II. {T}he Construction of
:: First-Order Formulas
:: 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, SUBSTUT1, MCART_1,
MARGREL1, REALSET1, FINSEQ_1, ORDINAL4, XBOOLEAN, CARD_1, ZFMISC_1,
RELAT_1, BVFUNC_2, XBOOLE_0, FUNCT_1, TARSKI, ZF_LANG, FUNCT_4, FUNCOP_1,
CLASSES2, SUBLEMMA, PARTFUN1, CQC_SIM1, ARYTM_3, XXREAL_0, ARYTM_1,
SUBSTUT2, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, ORDINAL1, SUBSET_1, FINSEQ_1,
FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, PARTFUN1, NUMBERS, XCMPLX_0,
XXREAL_0, NAT_1, CQC_LANG, FUNCOP_1, RELAT_1, FUNCT_4, FUNCT_2, CQC_SIM1,
DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA;
constructors PARTFUN1, DOMAIN_1, XXREAL_0, NAT_1, INT_1, QC_LANG3, CQC_SIM1,
SUBLEMMA, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
XREAL_0, NAT_1, INT_1, QC_LANG1, CQC_LANG, SUBSTUT1, SUBLEMMA, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Further Properties of Substitution
reserve Al for QC-alphabet;
reserve a,b,b1 for object,
i,j,k,n for Nat,
p,q,r,s for Element of CQC-WFF(Al),
x,y,y1 for bound_QC-variable of Al,
P for QC-pred_symbol of k,Al,
l,ll for CQC-variable_list of k,Al,
Sub,Sub1 for CQC_Substitution of Al,
S,S1,S2 for Element of CQC-Sub-WFF(Al),
P1,P2 for Element of QC-pred_symbols(Al);
theorem :: SUBSTUT2:1
for Sub holds ex S st S`1 = VERUM(Al) & S`2 = Sub;
theorem :: SUBSTUT2:2
for Sub holds ex S st S`1 = P!ll & S`2 = Sub;
theorem :: SUBSTUT2:3
for k,l being Nat st P is (QC-pred_symbol of k,Al) & P is (
QC-pred_symbol of l,Al) holds k = l;
theorem :: SUBSTUT2:4
(for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub holds
ex S st S`1 = 'not' p & S`2 = Sub;
theorem :: SUBSTUT2:5
(for Sub holds ex S st S`1 = p & S`2 = Sub) & (for Sub holds ex S
st S`1 = q & S`2 = Sub) implies for Sub holds ex S st S`1 = p '&' q & S`2 = Sub
;
definition
let Al, p, Sub;
redefine func [p,Sub] -> Element of [:QC-WFF(Al),vSUB(Al):];
end;
theorem :: SUBSTUT2:6
dom RestrictSub(x,All(x,p),Sub) misses {x};
theorem :: SUBSTUT2:7
x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p),
Sub]) = x.upVar(RestrictSub(x,All(x,p),Sub),p);
theorem :: SUBSTUT2:8
not x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p ),Sub]) = x
;
theorem :: SUBSTUT2:9
ExpandSub(x,p,RestrictSub(x,All(x,p),Sub)) = @RestrictSub(x,All(x
,p),Sub) +* (x|S_Bound([All(x,p),Sub]));
theorem :: SUBSTUT2:10
S`2 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub])
) & S`1 = p implies [S,x] is quantifiable & ex S1 st S1 = [All(x,p),Sub];
theorem :: SUBSTUT2:11
(for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub
holds ex S st S`1 = All(x,p) & S`2 = Sub;
theorem :: SUBSTUT2:12
for p, Sub holds ex S st S`1 = p & S`2 = Sub;
definition
let Al,p,Sub;
redefine func [p,Sub] -> Element of CQC-Sub-WFF(Al);
end;
notation
let Al,x,y;
synonym Sbst(x,y) for x .--> y;
end;
definition
let Al,x,y;
redefine func Sbst(x,y) -> CQC_Substitution of Al;
end;
begin :: Facts about Substitution and Quantifiers of a Formula
definition
let Al,p,x,y;
func p.(x,y) -> Element of CQC-WFF(Al) equals
:: SUBSTUT2:def 1
CQC_Sub([p,Sbst(x,y)]);
end;
scheme :: SUBSTUT2:sch 1
CQCInd1 { Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) holds P[p]
provided
for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p] and
for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k
holds P[p] holds for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k+1
holds P[p];
scheme :: SUBSTUT2:sch 2
CQCInd2 {Al() -> QC-alphabet, P[set]}:
for p being Element of CQC-WFF(Al()) holds P[p]
provided
for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= 0 holds P[p] and
for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= k
holds P[p] holds for p being Element of CQC-WFF(Al())
st QuantNbr(p) <= k+1 holds P[p];
theorem :: SUBSTUT2:13
VERUM(Al).(x,y) = VERUM(Al);
theorem :: SUBSTUT2:14
(P!l).(x,y) = P!CQC_Subst(l,Sbst(x,y)) & QuantNbr(P!l) = QuantNbr((P!l
).(x,y));
theorem :: SUBSTUT2:15
QuantNbr(P!l) = QuantNbr(CQC_Sub([P!l,Sub]));
definition
let Al;
let S be Element of QC-Sub-WFF(Al);
redefine func S`2 -> CQC_Substitution of Al;
end;
theorem :: SUBSTUT2:16
['not' p,Sub] = Sub_not [p,Sub];
theorem :: SUBSTUT2:17
'not' p.(x,y) = 'not' (p.(x,y)) & (QuantNbr(p) = QuantNbr(p.(x,y))
implies QuantNbr('not' p) = QuantNbr('not' p.(x,y)));
theorem :: SUBSTUT2:18
(for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
for Sub holds QuantNbr('not' p) = QuantNbr(CQC_Sub(['not' p,Sub]));
theorem :: SUBSTUT2:19
[p '&' q,Sub] = CQCSub_&([p,Sub],[q,Sub]);
theorem :: SUBSTUT2:20
(p '&' q).(x,y) = (p.(x,y)) '&' (q.(x,y)) & ( QuantNbr(p) = QuantNbr(p
.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y)) implies QuantNbr(p '&'q) = QuantNbr((
p '&' q).(x,y)));
theorem :: SUBSTUT2:21
(for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) & (for
Sub holds QuantNbr(q) = QuantNbr(CQC_Sub([q,Sub]))) implies for Sub holds
QuantNbr(p '&' q) = QuantNbr(CQC_Sub[p '&' q,Sub]);
definition
let Al;
func CFQ(Al) -> Function of CQC-Sub-WFF(Al),vSUB(Al) equals
:: SUBSTUT2:def 2
(QSub(Al))|CQC-Sub-WFF(Al);
end;
definition
let Al,p,x,Sub;
func QScope(p,x,Sub) -> CQC-WFF-like Element of [:QC-Sub-WFF(Al),
bound_QC-variables(Al):] equals
:: SUBSTUT2:def 3
[[p,(CFQ(Al)).[All(x,p),Sub]],x];
end;
definition
let Al,p,x,Sub;
func Qsc(p,x,Sub) -> second_Q_comp of QScope(p,x,Sub) equals
:: SUBSTUT2:def 4
Sub;
end;
theorem :: SUBSTUT2:22
[All(x,p),Sub] = CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) &
QScope(p,x,Sub) is quantifiable;
theorem :: SUBSTUT2:23
(for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
for Sub holds QuantNbr(All(x,p)) = QuantNbr(CQC_Sub([All(x,p),Sub]));
theorem :: SUBSTUT2:24
QuantNbr(VERUM(Al)) = QuantNbr(CQC_Sub([VERUM(Al),Sub]));
theorem :: SUBSTUT2:25
for p, Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]));
theorem :: SUBSTUT2:26
p is atomic implies ex k,P,ll st p = P!ll;
scheme :: SUBSTUT2:sch 3
CQCInd3 {Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p]
provided
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k,Al()
for P being QC-pred_symbol of k,Al()
holds P[VERUM(Al())] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]);
begin :: Results about the Construction of Formulas
reserve F1,F2,F3 for QC-formula of Al,
L for FinSequence;
definition
let Al;
let G,H be QC-formula of Al;
assume
G is_subformula_of H;
mode PATH of G,H -> FinSequence means
:: SUBSTUT2:def 5
1 <= len it & it.1 = G & it.(
len it) = H & for k st 1 <= k & k < len it ex G1,H1
being Element of QC-WFF(Al) st it.k = G1 & it.(k+1) = H1 &
G1 is_immediate_constituent_of H1;
end;
theorem :: SUBSTUT2:27
for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <=
len L holds ex F3 st F3 = L.i & F3 is_subformula_of F2;
theorem :: SUBSTUT2:28
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i
<= len L holds L.i is Element of CQC-WFF(Al);
theorem :: SUBSTUT2:29
for L being PATH of q,p st QuantNbr(p) <= n & q is_subformula_of
p & 1 <= i & i <= len L holds ex r st r = L.i & QuantNbr(r) <= n;
theorem :: SUBSTUT2:30
QuantNbr(p) = n & q is_subformula_of p implies QuantNbr(q) <= n;
theorem :: SUBSTUT2:31
for n,p st (for q st q is_subformula_of p holds QuantNbr(q) = n) holds n = 0;
theorem :: SUBSTUT2:32
for p st (for q st q is_subformula_of p holds for x,r holds q <> All(x
,r)) holds QuantNbr(p) = 0;
theorem :: SUBSTUT2:33
for p st for q st q is_subformula_of p holds QuantNbr(q) <> 1
holds QuantNbr(p) = 0;
theorem :: SUBSTUT2:34
1 <= QuantNbr(p) implies ex q st q is_subformula_of p & QuantNbr(q)=1;