:: Variables in Formulae of the First Order Language
:: by Czes{\l}aw Byli\'nski and Grzegorz Bancerek
::
:: Received November 23, 1989
:: 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 SUBSET_1, NUMBERS, QC_LANG1, FINSEQ_1, XBOOLE_0, FUNCT_1,
ZF_LANG, XXREAL_0, CLASSES2, REALSET1, BVFUNC_2, XBOOLEAN, MARGREL1,
ZF_LANG1, TARSKI, ZFMISC_1, QC_LANG2, RCOMP_1, ZF_MODEL, QC_LANG3, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1,
FUNCT_2, FINSEQ_1, QC_LANG1, QC_LANG2, XXREAL_0;
constructors FUNCT_2, XXREAL_0, MEMBERED, QC_LANG2, RELSET_1;
registrations SUBSET_1, ORDINAL1, RELSET_1, QC_LANG1, XXREAL_0;
requirements NUMERALS, BOOLE, SUBSET;
begin
reserve i,k for Nat;
scheme :: QC_LANG3:sch 1
QCFuncUniq { Al() -> QC-alphabet, D() -> non empty set,
F1,F2() -> (Function of QC-WFF(Al()), D()),
V() -> (Element of D()),
A,N(set) -> (Element of D()),
C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()}
:
F1() = F2()
provided
for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
(p = VERUM(Al()) implies F1().p = V()) &
(p is atomic implies F1().p = A(p)) & (p is negative &
d1 = F1().the_argument_of p implies F1().p = N(d1)) &
(p is conjunctive & d1 = F1().the_left_argument_of p &
d2 = F1().the_right_argument_of p implies F1().p = C(
d1, d2)) & (p is universal & d1 = F1().the_scope_of p implies
F1().p = Q(p, d1)) and
for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
(p = VERUM(Al()) implies F2().p = V()) & (p is atomic implies F2().p = A(p)) &
(p is negative & d1 = F2().the_argument_of p implies F2().p = N(d1)) &
(p is conjunctive & d1 = F2().the_left_argument_of p &
d2 = F2().the_right_argument_of p implies F2().p = C(d1, d2)) &
(p is universal & d1 = F2().the_scope_of p implies F2().p = Q(p, d1));
scheme :: QC_LANG3:sch 2
QCDefD { Al() -> QC-alphabet,
D() -> non empty set,
V() -> (Element of D()),
p() -> (Element of QC-WFF(Al())),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()),Element of D()) -> (Element of D()),
Q((Element of QC-WFF(Al())),
Element of D()) -> Element of D()}
:
(ex d being (Element of D()), F being Function of QC-WFF(Al()),
D() st d = F.p() & for p being Element of QC-WFF(Al())
for d1,d2 being Element of D() holds
(p = VERUM(Al()) implies F.p = V()) & (p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) &
(p is conjunctive & d1 = F.the_left_argument_of p &
d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) &
for x1,x2 being Element of D() st (ex F being Function of QC-WFF(Al()),
D() st x1 = F.p() & for p being Element of QC-WFF(Al())
for d1,d2 being Element of D() holds
(p = VERUM(Al()) implies F.p = V()) & (p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) &
(p is conjunctive & d1 = F.the_left_argument_of p &
d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) &
(ex F being Function of QC-WFF(Al()), D() st x2 = F.p() &
for p being Element of QC-WFF(Al()) for d1,d2 being Element of D()
holds (p = VERUM(Al()) implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) &
(p is conjunctive & d1 = F.the_left_argument_of p &
d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) )
holds x1 = x2;
scheme :: QC_LANG3:sch 3
QCDResult9VERUM { Al() -> QC-alphabet, D() -> non empty set,
F(Element of QC-WFF(Al())) -> (Element of D()), V() -> (Element of D()),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> Element of D()} : F(VERUM(Al())) = V()
provided
for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al())
implies F.p = V()) & (p is atomic
implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N
(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.
the_scope_of p implies F.p = Q(p, d1));
scheme :: QC_LANG3:sch 4
QCDResult9atomic { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), F(Element of QC-WFF(Al())) -> (Element of D()),
p() -> QC-formula of Al(), A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()),
Q((Element of QC-WFF(Al())), Element of D()) -> Element of D()}
:
F(p()) = A(p())
provided
for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) implies F.p = V()) &
(p is atomic implies F.p = A(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N(d1)) &
(p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and
p() is atomic;
scheme :: QC_LANG3:sch 5
QCDResult9negative { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), p() -> QC-formula of Al(),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> (Element of D()), F(Element of QC-WFF(Al()))
-> (Element of D()) }
:
F(p()) = N(F(the_argument_of p()))
provided
for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p
& for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) implies F.p = V())
& (p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p implies F.p = N (d1)) &
(p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and
p() is negative;
scheme :: QC_LANG3:sch 6
QCDResult9conjunctive { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> (Element of D()),
F(Element of QC-WFF(Al())) -> (Element of D()),
p() -> QC-formula of Al() } : for d1,d2 being Element of D() st d1 = F(
the_left_argument_of p()) & d2 = F(the_right_argument_of p())
holds F(p()) = C(d1,d2)
provided
for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p implies F.p = N
(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.
the_scope_of p implies F.p = Q(p, d1)) and
p() is conjunctive;
scheme :: QC_LANG3:sch 7
QCDResult9universal { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), p() -> QC-formula of Al(),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> (Element of D()),
F(Element of QC-WFF(Al())) -> (Element of D()) }
:
F(p()) = Q(p(),F(the_scope_of p()))
provided
for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) implies F.p = V()) &
(p is atomic implies F.p = A(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies
F.p = C(d1, d2)) & (p is universal &
d1 = F.the_scope_of p implies F.p = Q(p, d1)) and
p() is universal;
reserve A for QC-alphabet;
reserve x for bound_QC-variable of A;
reserve a for free_QC-variable of A;
reserve p,q for Element of QC-WFF(A);
reserve l for FinSequence of QC-variables(A);
reserve P,Q for QC-pred_symbol of A;
reserve V for non empty Subset of QC-variables(A);
reserve s,t for QC-symbol of A;
theorem :: QC_LANG3:1
P is QC-pred_symbol of the_arity_of P, A;
definition
let A,l,V;
func variables_in(l,V) -> Subset of V equals
:: QC_LANG3:def 1
{ l.k : 1 <= k & k <= len l & l.k in V };
end;
theorem :: QC_LANG3:2
still_not-bound_in l = variables_in(l,bound_QC-variables(A));
theorem :: QC_LANG3:3
still_not-bound_in VERUM(A) = {};
theorem :: QC_LANG3:4
for p being QC-formula of A st p is atomic holds still_not-bound_in p
= still_not-bound_in the_arguments_of p;
theorem :: QC_LANG3:5
for P being QC-pred_symbol of k,A for l being QC-variable_list of k, A
holds still_not-bound_in (P!l) = still_not-bound_in l;
theorem :: QC_LANG3:6
for p being QC-formula of A st p is negative holds still_not-bound_in
p = still_not-bound_in the_argument_of p;
theorem :: QC_LANG3:7
for p being QC-formula of A holds still_not-bound_in 'not' p =
still_not-bound_in p;
theorem :: QC_LANG3:8
still_not-bound_in FALSUM(A) = {};
theorem :: QC_LANG3:9
for p being QC-formula of A st p is conjunctive holds
still_not-bound_in p = (still_not-bound_in the_left_argument_of p) \/ (
still_not-bound_in the_right_argument_of p);
theorem :: QC_LANG3:10
for p,q being QC-formula of A holds still_not-bound_in(p '&' q) = (
still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:11
for p being QC-formula of A st p is universal holds
still_not-bound_in p = (still_not-bound_in the_scope_of p) \ {bound_in p};
theorem :: QC_LANG3:12
for p being QC-formula of A holds still_not-bound_in All(x,p) = (
still_not-bound_in p) \ {x};
theorem :: QC_LANG3:13
for p being QC-formula of A st p is disjunctive holds
still_not-bound_in p = (still_not-bound_in the_left_disjunct_of p) \/ (
still_not-bound_in the_right_disjunct_of p);
theorem :: QC_LANG3:14
for p,q being QC-formula of A holds still_not-bound_in p 'or' q = (
still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:15
for p being QC-formula of A st p is conditional holds
still_not-bound_in p = (still_not-bound_in the_antecedent_of p) \/ (
still_not-bound_in the_consequent_of p);
theorem :: QC_LANG3:16
for p,q being QC-formula of A holds still_not-bound_in p => q = (
still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:17
for p being QC-formula of A st p is biconditional holds
still_not-bound_in p = (still_not-bound_in the_left_side_of p) \/ (
still_not-bound_in the_right_side_of p);
theorem :: QC_LANG3:18
for p,q being QC-formula of A holds still_not-bound_in p <=> q = (
still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:19
for p being QC-formula of A holds still_not-bound_in Ex(x,p) = (
still_not-bound_in p) \ {x};
theorem :: QC_LANG3:20
VERUM(A) is closed & FALSUM(A) is closed;
theorem :: QC_LANG3:21
for p being QC-formula of A holds p is closed iff 'not' p is closed;
theorem :: QC_LANG3:22
for p,q being QC-formula of A holds p is closed & q is closed iff p
'&' q is closed;
theorem :: QC_LANG3:23
for p being QC-formula of A holds All(x,p) is closed iff
still_not-bound_in p c= {x};
theorem :: QC_LANG3:24
for p being QC-formula of A st p is closed holds All(x,p) is closed;
theorem :: QC_LANG3:25
for p,q being QC-formula of A holds p is closed & q is closed iff p 'or' q
is closed;
theorem :: QC_LANG3:26
for p,q being QC-formula of A holds p is closed &
q is closed iff p => q is closed;
theorem :: QC_LANG3:27
for p,q being QC-formula of A holds p is closed & q is closed iff p <=> q
is closed;
theorem :: QC_LANG3:28
for p being QC-formula of A holds Ex(x,p) is closed iff
still_not-bound_in p c= {x};
theorem :: QC_LANG3:29
for p being QC-formula of A st p is closed holds Ex(x,p) is closed;
definition
let A,s;
func x.s -> bound_QC-variable of A equals
:: QC_LANG3:def 2
[4,s];
end;
theorem :: QC_LANG3:30
ex t st x.t = x;
definition
let A,k;
func (A)a.k -> free_QC-variable of A equals
:: QC_LANG3:def 3
[6,k];
end;
theorem :: QC_LANG3:31
ex i st (A)a.i = a;
theorem :: QC_LANG3:32
for c being Element of fixed_QC-variables(A) for a being Element of
free_QC-variables(A) holds c <> a;
theorem :: QC_LANG3:33
for c being Element of fixed_QC-variables(A) for x being Element of
bound_QC-variables(A) holds c <> x;
theorem :: QC_LANG3:34
for a being Element of free_QC-variables(A) for x being Element of
bound_QC-variables(A) holds a <> x;
definition
let A,V,p;
func Vars(p,V) -> Subset of V means
:: QC_LANG3:def 4
ex F being Function of QC-WFF(A),
bool V st it = F.p & for p being Element of QC-WFF(A)
for d1,d2 being Subset of V
holds (p = VERUM(A) implies F.p = {}(V)) &
(p is atomic implies F.p = variables_in
(the_arguments_of p,V)) & (p is negative & d1 = F.the_argument_of p implies F.p
= d1) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = d1 \/ d2) & (p is universal & d1 = F.
the_scope_of p implies F.p = d1);
end;
theorem :: QC_LANG3:35
Vars(VERUM(A),V) = {};
theorem :: QC_LANG3:36
p is atomic implies Vars(p,V) = variables_in(the_arguments_of p,
V) & Vars(p,V) = { (the_arguments_of p).k : 1 <= k & k <= len (the_arguments_of
p) & (the_arguments_of p).k in V };
theorem :: QC_LANG3:37
for P being QC-pred_symbol of k, A for l being QC-variable_list of
k, A holds Vars(P!l,V) = variables_in(l, V) &
Vars((P!l),V) = { l.i : 1 <= i & i
<= len l & l.i in V };
theorem :: QC_LANG3:38
p is negative implies Vars(p,V) = Vars(the_argument_of p,V);
theorem :: QC_LANG3:39
Vars('not' p,V) = Vars(p,V);
theorem :: QC_LANG3:40
Vars(FALSUM(A),V) = {};
theorem :: QC_LANG3:41
p is conjunctive implies Vars(p,V) = Vars(the_left_argument_of p,V) \/
Vars(the_right_argument_of p,V);
theorem :: QC_LANG3:42
Vars(p '&' q,V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:43
p is universal implies Vars(p,V) = Vars(the_scope_of p,V);
theorem :: QC_LANG3:44
Vars(All(x,p),V) = Vars(p,V);
theorem :: QC_LANG3:45
p is disjunctive implies Vars(p,V) = Vars(the_left_disjunct_of p
,V) \/ Vars(the_right_disjunct_of p,V);
theorem :: QC_LANG3:46
Vars(p 'or' q, V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:47
p is conditional implies Vars(p,V) = Vars(the_antecedent_of p,V)
\/ Vars(the_consequent_of p,V);
theorem :: QC_LANG3:48
Vars(p => q,V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:49
p is biconditional implies Vars(p,V) = Vars(the_left_side_of p,V
) \/ Vars(the_right_side_of p,V);
theorem :: QC_LANG3:50
Vars(p <=> q,V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:51
p is existential implies Vars(p,V) = Vars(the_argument_of the_scope_of
the_argument_of p, V);
theorem :: QC_LANG3:52
Vars(Ex(x,p), V) = Vars(p,V);
definition
let A,p;
func Free p -> Subset of free_QC-variables(A) equals
:: QC_LANG3:def 5
Vars(p,free_QC-variables(A));
end;
theorem :: QC_LANG3:53
Free VERUM(A) = {};
theorem :: QC_LANG3:54
for P being QC-pred_symbol of k, A for l being QC-variable_list of k, A
holds Free(P!l) = { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A)};
theorem :: QC_LANG3:55
Free 'not' p = Free p;
theorem :: QC_LANG3:56
Free FALSUM(A) = {};
theorem :: QC_LANG3:57
Free(p '&' q) = Free p \/ Free q;
theorem :: QC_LANG3:58
Free(All(x,p)) = Free(p);
theorem :: QC_LANG3:59
Free(p 'or' q) = Free p \/ Free q;
theorem :: QC_LANG3:60
Free(p => q) = Free p \/ Free q;
theorem :: QC_LANG3:61
Free(p <=> q) = Free p \/ Free q;
theorem :: QC_LANG3:62
Free Ex(x,p) = Free p;
definition
let A,p;
func Fixed p -> Subset of fixed_QC-variables(A) equals
:: QC_LANG3:def 6
Vars(p,fixed_QC-variables(A));
end;
theorem :: QC_LANG3:63
Fixed VERUM(A) = {};
theorem :: QC_LANG3:64
for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A
holds Fixed(P!l) = { l.i : 1 <= i & i <= len l & l.i in fixed_QC-variables(A)};
theorem :: QC_LANG3:65
Fixed 'not' p = Fixed p;
theorem :: QC_LANG3:66
Fixed FALSUM(A) = {};
theorem :: QC_LANG3:67
Fixed(p '&' q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:68
Fixed(All(x,p)) = Fixed(p);
theorem :: QC_LANG3:69
Fixed(p 'or' q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:70
Fixed(p => q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:71
Fixed(p <=> q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:72
Fixed Ex(x,p) = Fixed p;