:: Variables in Formulae of the First Order Language
::  by Czes{\l}aw Byli\'nski and Grzegorz Bancerek
::
:: Received November 23, 1989
:: 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 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;