Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

The abstract of the Mizar article:

Variables in Formulae of the First Order Language

by
Czeslaw Bylinski, and
Grzegorz Bancerek

Received November 23, 1989

MML identifier: QC_LANG3
[ Mizar article, MML identifier index ]


environ

 vocabulary QC_LANG1, FINSEQ_1, FUNCT_1, ZF_LANG, BOOLE, QC_LANG2, PRE_TOPC,
      ZF_MODEL, QC_LANG3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      FUNCT_1, FUNCT_2, FINSEQ_1, QC_LANG1, QC_LANG2;
 constructors FUNCT_2, QC_LANG2, XREAL_0, XCMPLX_0, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, RELSET_1, QC_LANG1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS,
      ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET;


begin

 reserve i,j,k for Nat;
 reserve x for bound_QC-variable;
 reserve a for free_QC-variable;
 reserve p,q for Element of QC-WFF;
 reserve l for FinSequence of QC-variables;
 reserve P,Q for QC-pred_symbol;
 reserve V for non empty Subset of QC-variables;

scheme QC_Func_Uniq { D() -> non empty set,
                F1() -> (Function of QC-WFF, D()),
                F2() -> (Function of QC-WFF, D()),
                V() -> (Element of D()),
                A(set) -> (Element of D()),
                N(set) -> (Element of D()),
                C(set,set) -> (Element of D()),
                Q(set,set) -> Element of D()} :
 F1() = F2() provided
 for p for d1,d2 being Element of D() holds
      (p = VERUM 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 for d1,d2 being Element of D() holds
      (p = VERUM 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_Def_D
  { D() -> non empty set, V() -> (Element of D()),
    p() -> (Element of QC-WFF),
    A(Element of QC-WFF) -> (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), Element of D()) -> Element of D()} :

(ex d being (Element of D()), F being Function of QC-WFF, D() st
        d = F.p() &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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, D() st
        x1 = F.p() &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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, D() st
        x2 = F.p() &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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_D_Result'VERUM
  { D() -> non empty set,
    F(Element of QC-WFF) -> (Element of D()),
    V() -> (Element of D()),
    A(Element of QC-WFF) -> (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), Element of D()) -> Element of D()} :

  F(VERUM) = V()
provided
 for p being QC-formula, d being Element of D() holds
     d = F(p) iff
      ex F being Function of QC-WFF, D() st
        d = F.p &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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_D_Result'atomic
  { D() -> non empty set, V() -> (Element of D()),
    F(Element of QC-WFF) -> (Element of D()),
    p() -> QC-formula,
    A(Element of QC-WFF) -> (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), Element of D()) -> Element of D()} :

  F(p()) = A(p())
provided
 for p being QC-formula, d being Element of D() holds
     d = F(p) iff
      ex F being Function of QC-WFF, D() st
        d = F.p &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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_D_Result'negative
  { D() -> non empty set, V() -> (Element of D()),
    p() -> QC-formula,
    A(Element of QC-WFF) -> (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), Element of D()) -> (Element of D()),
    F(Element of QC-WFF) -> (Element of D()) } :

  F(p()) = N(F(the_argument_of p()))
provided
 for p being QC-formula, d being Element of D() holds
     d = F(p) iff
      ex F being Function of QC-WFF, D() st
        d = F.p &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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_D_Result'conjunctive
  { D() -> non empty set,
    V() -> (Element of D()),
    A(Element of QC-WFF) -> (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), Element of D()) -> (Element of D()),
    F(Element of QC-WFF) -> (Element of D()),
    p() -> QC-formula } :

 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, d being Element of D() holds
     d = F(p) iff
      ex F being Function of QC-WFF, D() st
        d = F.p &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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_D_Result'universal
  { D() -> non empty set,
    V() -> (Element of D()),
    p() -> QC-formula,
    A(Element of QC-WFF) -> (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), Element of D()) -> (Element of D()),
    F(Element of QC-WFF) -> (Element of D()) } :

  F(p()) = Q(p(),F(the_scope_of p()))
provided
 for p being QC-formula, d being Element of D() holds
     d = F(p) iff
      ex F being Function of QC-WFF, D() st
        d = F.p &
        for p being Element of QC-WFF
        for d1,d2 being Element of D() holds
        (p = VERUM 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;

canceled 2;

theorem :: QC_LANG3:3
     P is QC-pred_symbol of the_arity_of P;

 definition let l; let V;
 canceled;

  func variables_in(l,V) -> Element of bool V equals
:: QC_LANG3:def 2
 { l.k : 1 <= k & k <= len l & l.k in V };
 end;

canceled 2;

theorem :: QC_LANG3:6
     still_not-bound_in l = variables_in(l,bound_QC-variables);

theorem :: QC_LANG3:7
   still_not-bound_in VERUM = {};

theorem :: QC_LANG3:8
   for p being QC-formula st p is atomic holds
     still_not-bound_in p = still_not-bound_in the_arguments_of p;

theorem :: QC_LANG3:9
     for P being QC-pred_symbol of k for l being QC-variable_list of k
    holds still_not-bound_in (P!l) = still_not-bound_in l;

theorem :: QC_LANG3:10
   for p being QC-formula st p is negative holds
     still_not-bound_in p = still_not-bound_in the_argument_of p;

theorem :: QC_LANG3:11
   for p being QC-formula holds
     still_not-bound_in 'not' p = still_not-bound_in p;

theorem :: QC_LANG3:12
   still_not-bound_in FALSUM = {};

theorem :: QC_LANG3:13
   for p being QC-formula 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:14
   for p,q being QC-formula holds
     still_not-bound_in(p '&' q) =
       (still_not-bound_in p) \/ (still_not-bound_in q);

theorem :: QC_LANG3:15
   for p being QC-formula st p is universal holds
     still_not-bound_in p =
       (still_not-bound_in the_scope_of p) \ {bound_in p};

theorem :: QC_LANG3:16
   for p being QC-formula
    holds still_not-bound_in All(x,p) = (still_not-bound_in p) \ {x};

theorem :: QC_LANG3:17
   for p being QC-formula 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:18
     for p,q being QC-formula holds still_not-bound_in p 'or' q
     = (still_not-bound_in p) \/ (still_not-bound_in q);

theorem :: QC_LANG3:19
   for p being QC-formula 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:20
   for p,q being QC-formula holds still_not-bound_in p => q
     = (still_not-bound_in p) \/ (still_not-bound_in q);

theorem :: QC_LANG3:21
   for p being QC-formula 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:22
     for p,q being QC-formula holds still_not-bound_in p <=> q
     = (still_not-bound_in p) \/ (still_not-bound_in q);

theorem :: QC_LANG3:23
   for p being QC-formula holds
    still_not-bound_in Ex(x,p) = (still_not-bound_in p) \ {x};

theorem :: QC_LANG3:24
     VERUM is closed & FALSUM is closed;

theorem :: QC_LANG3:25
   for p being QC-formula holds p is closed iff 'not' p is closed;

theorem :: QC_LANG3:26
   for p,q being QC-formula holds
     p is closed & q is closed iff p '&' q is closed;

theorem :: QC_LANG3:27
   for p being QC-formula holds
    All(x,p) is closed iff still_not-bound_in p c= {x};

theorem :: QC_LANG3:28
     for p being QC-formula st p is closed holds All(x,p) is closed;

theorem :: QC_LANG3:29
     for p,q being QC-formula holds
     p is closed & q is closed iff p 'or' q is closed;

theorem :: QC_LANG3:30
   for p,q being QC-formula holds
     p is closed & q is closed iff p => q is closed;

theorem :: QC_LANG3:31
     for p,q being QC-formula holds
     p is closed & q is closed iff p <=> q is closed;

theorem :: QC_LANG3:32
   for p being QC-formula holds
    Ex(x,p) is closed iff still_not-bound_in p c= {x};

theorem :: QC_LANG3:33
     for p being QC-formula st p is closed holds Ex(x,p) is closed;

definition let k;
  func x.k -> bound_QC-variable equals
:: QC_LANG3:def 3
  [4,k];
end;

canceled;

theorem :: QC_LANG3:35
     x.i = x.j implies i = j;

theorem :: QC_LANG3:36
     ex i st x.i = x;

definition let k;
  func a.k -> free_QC-variable equals
:: QC_LANG3:def 4
  [6,k];
end;

canceled;

theorem :: QC_LANG3:38
     a.i = a.j implies i = j;

theorem :: QC_LANG3:39
     ex i st a.i = a;

theorem :: QC_LANG3:40
     for c being Element of fixed_QC-variables
    for a being Element of free_QC-variables holds c <> a;

theorem :: QC_LANG3:41
     for c being Element of fixed_QC-variables
    for x being Element of bound_QC-variables holds c <> x;

theorem :: QC_LANG3:42
     for a being Element of free_QC-variables
    for x being Element of bound_QC-variables holds a <> x;

definition let V; let V1,V2 be Element of bool V;
 redefine func V1 \/ V2 -> Element of bool V;
end;

 definition let V; let p;
  func Vars(p,V) -> Element of bool V means
:: QC_LANG3:def 5

   ex F being Function of QC-WFF, bool V st
    it = F.p &
    for p being Element of QC-WFF
     for d1,d2 being Element of bool V holds
      (p = VERUM 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;

canceled 3;

theorem :: QC_LANG3:46
    Vars(VERUM,V) = {};

theorem :: QC_LANG3:47
   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:48
   for P being QC-pred_symbol of k for l being QC-variable_list of k
    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:49
    p is negative implies Vars(p,V) = Vars(the_argument_of p,V);

theorem :: QC_LANG3:50
   Vars('not' p,V) = Vars(p,V);

theorem :: QC_LANG3:51
   Vars(FALSUM,V) = {};

theorem :: QC_LANG3:52
    p is conjunctive implies Vars(p,V) =
      Vars(the_left_argument_of p,V) \/ Vars(the_right_argument_of p,V);

theorem :: QC_LANG3:53
   Vars(p '&' q,V) = Vars(p,V) \/ Vars(q,V);

theorem :: QC_LANG3:54
    p is universal implies Vars(p,V) = Vars(the_scope_of p,V);

theorem :: QC_LANG3:55
   Vars(All(x,p),V) = Vars(p,V);

theorem :: QC_LANG3:56
   p is disjunctive implies Vars(p,V) =
      Vars(the_left_disjunct_of p,V) \/ Vars(the_right_disjunct_of p,V);

theorem :: QC_LANG3:57
     Vars(p 'or' q, V) = Vars(p,V) \/ Vars(q,V);

theorem :: QC_LANG3:58
   p is conditional implies Vars(p,V) =
      Vars(the_antecedent_of p,V) \/ Vars(the_consequent_of p,V);

theorem :: QC_LANG3:59
   Vars(p => q,V) = Vars(p,V) \/ Vars(q,V);

theorem :: QC_LANG3:60
   p is biconditional implies Vars(p,V) =
      Vars(the_left_side_of p,V) \/ Vars(the_right_side_of p,V);

theorem :: QC_LANG3:61
     Vars(p <=> q,V) = Vars(p,V) \/ Vars(q,V);

theorem :: QC_LANG3:62
     p is existential implies Vars(p,V) =
      Vars(the_argument_of the_scope_of the_argument_of p, V);

theorem :: QC_LANG3:63
     Vars(Ex(x,p), V) = Vars(p,V);

 definition let p;
  func Free p -> Element of bool free_QC-variables equals
:: QC_LANG3:def 6
  Vars(p,free_QC-variables);
 end;

canceled;

theorem :: QC_LANG3:65
     Free VERUM = {};

theorem :: QC_LANG3:66
     for P being QC-pred_symbol of k for l being QC-variable_list of k
    holds Free(P!l) = { l.i : 1 <= i & i <= len l & l.i in free_QC-variables };

theorem :: QC_LANG3:67
   Free 'not' p = Free p;

theorem :: QC_LANG3:68
     Free FALSUM = {};

theorem :: QC_LANG3:69
   Free(p '&' q) = Free p \/ Free q;

theorem :: QC_LANG3:70
   Free(All(x,p)) = Free(p);

theorem :: QC_LANG3:71
     Free(p 'or' q) = Free p \/ Free q;

theorem :: QC_LANG3:72
   Free(p => q) = Free p \/ Free q;

theorem :: QC_LANG3:73
     Free(p <=> q) = Free p \/ Free q;

theorem :: QC_LANG3:74
     Free Ex(x,p) = Free p;

 definition let p;
  func Fixed p -> Element of bool fixed_QC-variables equals
:: QC_LANG3:def 7
  Vars(p,fixed_QC-variables);
 end;

canceled;

theorem :: QC_LANG3:76
   Fixed VERUM = {};

theorem :: QC_LANG3:77
     for P being QC-pred_symbol of k for l being QC-variable_list of k
    holds Fixed(P!l) = { l.i : 1 <= i & i <= len l & l.i in
 fixed_QC-variables };

theorem :: QC_LANG3:78
   Fixed 'not' p = Fixed p;

theorem :: QC_LANG3:79
     Fixed FALSUM = {};

theorem :: QC_LANG3:80
   Fixed(p '&' q) = Fixed p \/ Fixed q;

theorem :: QC_LANG3:81
   Fixed(All(x,p)) = Fixed(p);

theorem :: QC_LANG3:82
     Fixed(p 'or' q) = Fixed p \/ Fixed q;

theorem :: QC_LANG3:83
   Fixed(p => q) = Fixed p \/ Fixed q;

theorem :: QC_LANG3:84
     Fixed(p <=> q) = Fixed p \/ Fixed q;

theorem :: QC_LANG3:85
     Fixed Ex(x,p) = Fixed p;

Back to top