The abstract of the Mizar article:

Connectives and Subformulae of the First Order Language

by

Grzegorz Bancerek

Received November 23, 1989

MML identifier: QC_LANG2

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, QC_LANG1, ZF_LANG, FUNCT_1, MCART_1, RELAT_1, ARYTM_1,
      BOOLE, QC_LANG2;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XCMPLX_0, XREAL_0, RELAT_1,
      FUNCT_1, NAT_1, FINSEQ_1, MCART_1, QC_LANG1;
 constructors ENUMSET1, NAT_1, QC_LANG1, XREAL_0, XBOOLE_0;
 clusters RELSET_1, FINSEQ_1, XREAL_0, ARYTM_3, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;


begin

 reserve sq for FinSequence,
         x,y,z for bound_QC-variable,
         p,q,p1,p2,q1 for Element of QC-WFF;

theorem :: QC_LANG2:1
  'not' p = 'not' q implies p = q;

theorem :: QC_LANG2:2
  the_argument_of 'not' p = p;

theorem :: QC_LANG2:3
  p '&' q = p1 '&' q1 implies p = p1 & q = q1;

theorem :: QC_LANG2:4
  p is conjunctive implies
   p = (the_left_argument_of p) '&' the_right_argument_of p;

theorem :: QC_LANG2:5
 the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q;

theorem :: QC_LANG2:6
  All(x,p) = All(y,q) implies x = y & p = q;

theorem :: QC_LANG2:7
  p is universal implies p = All(bound_in p, the_scope_of p);

theorem :: QC_LANG2:8
  bound_in All(x,p) = x & the_scope_of All(x,p) = p;

 definition
  func FALSUM -> QC-formula equals
:: QC_LANG2:def 1
  'not' VERUM;
  let p,q be Element of QC-WFF;
  func p => q -> QC-formula equals
:: QC_LANG2:def 2
  'not' (p '&' 'not' q);
  func p 'or' q -> QC-formula equals
:: QC_LANG2:def 3
  'not' ('not' p '&' 'not' q);
 end;

 definition let p,q be Element of QC-WFF;
  func p <=> q -> QC-formula equals
:: QC_LANG2:def 4
  (p => q) '&' (q => p);
 end;

 definition let x be bound_QC-variable, p be Element of QC-WFF;
  func Ex(x,p) -> QC-formula equals
:: QC_LANG2:def 5
  'not' All(x,'not' p);
 end;

canceled 4;

theorem :: QC_LANG2:13
   FALSUM is negative & the_argument_of FALSUM = VERUM;

theorem :: QC_LANG2:14
  p 'or' q = 'not' p => q;

canceled;

theorem :: QC_LANG2:16
    p 'or' q = p1 'or' q1 implies p = p1 & q = q1;

theorem :: QC_LANG2:17
  p => q = p1 => q1 implies p = p1 & q = q1;

theorem :: QC_LANG2:18
    p <=> q = p1 <=> q1 implies p = p1 & q = q1;

theorem :: QC_LANG2:19
  Ex(x,p) = Ex(y,q) implies x = y & p = q;

 definition let x,y be bound_QC-variable, p be Element of QC-WFF;
  func All(x,y,p) -> QC-formula equals
:: QC_LANG2:def 6
  All(x,All(y,p));
  func Ex(x,y,p) -> QC-formula equals
:: QC_LANG2:def 7
  Ex(x,Ex(y,p));
 end;

theorem :: QC_LANG2:20
   All(x,y,p) = All(x,All(y,p)) & Ex(x,y,p) = Ex(x,Ex(y,p));

theorem :: QC_LANG2:21
  for x1,x2,y1,y2 being bound_QC-variable st
   All(x1,y1,p1) = All(x2,y2,p2) holds x1 = x2 & y1 = y2 & p1 = p2;

theorem :: QC_LANG2:22
  All(x,y,p) = All(z,q) implies x = z & All(y,p) = q;

theorem :: QC_LANG2:23
  for x1,x2,y1,y2 being bound_QC-variable st
   Ex(x1,y1,p1) = Ex(x2,y2,p2) holds x1 = x2 & y1 = y2 & p1 = p2;

theorem :: QC_LANG2:24
  Ex(x,y,p) = Ex(z,q) implies x = z & Ex(y,p) = q;

theorem :: QC_LANG2:25
   All(x,y,p) is universal &
   bound_in All(x,y,p) = x & the_scope_of All(x,y,p) = All(y,p);

 definition let x,y,z be bound_QC-variable, p be Element of QC-WFF;
  func All(x,y,z,p) -> QC-formula equals
:: QC_LANG2:def 8
  All(x,All(y,z,p));
  func Ex(x,y,z,p) -> QC-formula equals
:: QC_LANG2:def 9
  Ex(x,Ex(y,z,p));
 end;

theorem :: QC_LANG2:26
   All(x,y,z,p) = All(x,All(y,z,p)) & Ex(x,y,z,p) = Ex(x,Ex(y,z,p))
;

theorem :: QC_LANG2:27
   for x1,x2,y1,y2,z1,z2 being bound_QC-variable st
   All(x1,y1,z1,p1) = All(x2,y2,z2,p2) holds
    x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2;

 reserve s,t for bound_QC-variable;

theorem :: QC_LANG2:28
   All(x,y,z,p) = All(t,q) implies x = t & All(y,z,p) = q;

theorem :: QC_LANG2:29
   All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q;

theorem :: QC_LANG2:30
   for x1,x2,y1,y2,z1,z2 being bound_QC-variable st
   Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2) holds
    x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2;

theorem :: QC_LANG2:31
   Ex(x,y,z,p) = Ex(t,q) implies x = t & Ex(y,z,p) = q;

theorem :: QC_LANG2:32
   Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q;

theorem :: QC_LANG2:33
   All(x,y,z,p) is universal &
   bound_in All(x,y,z,p) = x & the_scope_of All(x,y,z,p) = All(y,z,p);

 definition let H be Element of QC-WFF;
  attr H is disjunctive
 means
:: QC_LANG2:def 10
ex p,q being Element of QC-WFF st H = p 'or' q;
  attr H is conditional means
:: QC_LANG2:def 11
  ex p,q being Element of QC-WFF st H = p => q;
  attr H is biconditional
 means
:: QC_LANG2:def 12
ex p,q being Element of QC-WFF st H = p <=> q;
  attr H is existential means
:: QC_LANG2:def 13
  ex x being bound_QC-variable, p being Element of QC-WFF st H = Ex(x,p);
 end;

canceled 4;

theorem :: QC_LANG2:38
   Ex(x,y,p) is existential & Ex(x,y,z,p) is existential;

 definition let H be Element of QC-WFF;
  func the_left_disjunct_of H -> QC-formula equals
:: QC_LANG2:def 14
  the_argument_of the_left_argument_of the_argument_of H;
  func the_right_disjunct_of H -> QC-formula equals
:: QC_LANG2:def 15
  the_argument_of the_right_argument_of the_argument_of H;
   synonym the_consequent_of H;
  func the_antecedent_of H -> QC-formula equals
:: QC_LANG2:def 16
  the_left_argument_of the_argument_of H;
 end;

 definition let H be Element of QC-WFF;
 canceled;

  func the_left_side_of H -> QC-formula equals
:: QC_LANG2:def 18
  the_antecedent_of the_left_argument_of H;
  func the_right_side_of H -> QC-formula equals
:: QC_LANG2:def 19
  the_consequent_of the_left_argument_of H;
 end;

 reserve F,G,H,H1 for Element of QC-WFF;

canceled 6;

theorem :: QC_LANG2:45
 the_left_disjunct_of(F 'or' G) = F & the_right_disjunct_of(F 'or' G) = G &
   the_argument_of F 'or' G = 'not' F '&' 'not' G;

theorem :: QC_LANG2:46
  the_antecedent_of(F => G) = F & the_consequent_of(F => G) = G &
   the_argument_of F => G = F '&' 'not' G;

theorem :: QC_LANG2:47
  the_left_side_of(F <=> G) = F & the_right_side_of(F <=> G) = G &
   the_left_argument_of(F <=> G) = F => G &
    the_right_argument_of(F <=> G) = G => F;

theorem :: QC_LANG2:48
   the_argument_of Ex(x,H) = All(x,'not' H);

theorem :: QC_LANG2:49
   H is disjunctive implies H is conditional &
  H is negative & the_argument_of H is conjunctive &
   the_left_argument_of the_argument_of H is negative &
    the_right_argument_of the_argument_of H is negative;

theorem :: QC_LANG2:50
   H is conditional implies
  H is negative & the_argument_of H is conjunctive &
   the_right_argument_of the_argument_of H is negative;

theorem :: QC_LANG2:51
   H is biconditional implies
  H is conjunctive & the_left_argument_of H is conditional &
   the_right_argument_of H is conditional;

theorem :: QC_LANG2:52
   H is existential implies H is negative & the_argument_of H is universal &
   the_scope_of the_argument_of H is negative;

theorem :: QC_LANG2:53
   H is disjunctive implies
   H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H);

theorem :: QC_LANG2:54
   H is conditional implies
   H = (the_antecedent_of H) => (the_consequent_of H);

theorem :: QC_LANG2:55
   H is biconditional implies
   H = (the_left_side_of H) <=> (the_right_side_of H);

theorem :: QC_LANG2:56
   H is existential implies
  H = Ex(bound_in the_argument_of H,
         the_argument_of the_scope_of the_argument_of H);

::
::  Immediate constituents of QC-formulae
::

 definition let G,H be Element of QC-WFF;
  pred G is_immediate_constituent_of H means
:: QC_LANG2:def 20
  H = 'not' G or
   (ex F being Element of QC-WFF st H = G '&' F or H = F '&' G) or
    ex x being bound_QC-variable st H = All(x,G);
 end;

 reserve x,y,z for bound_QC-variable,
         k,n,m for Nat,
         P for (QC-pred_symbol of k),
         V for QC-variable_list of k;

canceled;

theorem :: QC_LANG2:58
  not H is_immediate_constituent_of VERUM;

theorem :: QC_LANG2:59
  not H is_immediate_constituent_of P!V;

theorem :: QC_LANG2:60
  F is_immediate_constituent_of 'not' H iff F = H;

theorem :: QC_LANG2:61
    H is_immediate_constituent_of FALSUM iff H = VERUM;

theorem :: QC_LANG2:62
  F is_immediate_constituent_of G '&' H iff F = G or F = H;

theorem :: QC_LANG2:63
  F is_immediate_constituent_of All(x,H) iff F = H;

theorem :: QC_LANG2:64
  H is atomic implies not F is_immediate_constituent_of H;

theorem :: QC_LANG2:65
  H is negative implies
   (F is_immediate_constituent_of H iff F = the_argument_of H);

theorem :: QC_LANG2:66
  H is conjunctive implies
  (F is_immediate_constituent_of H iff
   F = the_left_argument_of H or F = the_right_argument_of H);

theorem :: QC_LANG2:67
  H is universal implies
   (F is_immediate_constituent_of H iff F = the_scope_of H);


::
:: Subformulae of QC-formulae
::

 reserve L,L' for FinSequence;


 definition let G,H;
  pred G is_subformula_of H means
:: QC_LANG2:def 21
  ex n,L st 1 <= n & len L = n & L.1 = G & L.n = H &
    for k st 1 <= k & k < n
     ex G1,H1 being Element of QC-WFF st L.k = G1 & L.(k+1) = H1 &
      G1 is_immediate_constituent_of H1;
  reflexivity;
 end;

 definition let H,F;
  pred H is_proper_subformula_of F means
:: QC_LANG2:def 22
  H is_subformula_of F & H <> F;
  irreflexivity;
 end;

canceled 3;

theorem :: QC_LANG2:71
  H is_immediate_constituent_of F implies len @H < len @F;

theorem :: QC_LANG2:72
  H is_immediate_constituent_of F implies H is_subformula_of F;

theorem :: QC_LANG2:73
  H is_immediate_constituent_of F implies H is_proper_subformula_of F;

theorem :: QC_LANG2:74
  H is_proper_subformula_of F implies len @H < len @F;

theorem :: QC_LANG2:75
  H is_proper_subformula_of F implies
   ex G st G is_immediate_constituent_of F;

theorem :: QC_LANG2:76
  F is_proper_subformula_of G & G is_proper_subformula_of H implies
   F is_proper_subformula_of H;

theorem :: QC_LANG2:77
  F is_subformula_of G & G is_subformula_of H implies
   F is_subformula_of H;

theorem :: QC_LANG2:78
  G is_subformula_of H & H is_subformula_of G implies G = H;

theorem :: QC_LANG2:79
  not (G is_proper_subformula_of H & H is_subformula_of G);

theorem :: QC_LANG2:80
    not (G is_proper_subformula_of H & H is_proper_subformula_of G);

theorem :: QC_LANG2:81
  not (G is_subformula_of H & H is_immediate_constituent_of G);

theorem :: QC_LANG2:82
  not (G is_proper_subformula_of H & H is_immediate_constituent_of G);

theorem :: QC_LANG2:83
 F is_proper_subformula_of G & G is_subformula_of H or
  F is_subformula_of G & G is_proper_subformula_of H or
   F is_subformula_of G & G is_immediate_constituent_of H or
    F is_immediate_constituent_of G & G is_subformula_of H or
     F is_proper_subformula_of G & G is_immediate_constituent_of H or
      F is_immediate_constituent_of G & G is_proper_subformula_of H implies
   F is_proper_subformula_of H;

theorem :: QC_LANG2:84
    not F is_proper_subformula_of VERUM;

theorem :: QC_LANG2:85
  not F is_proper_subformula_of P!V;

theorem :: QC_LANG2:86
  F is_subformula_of H iff F is_proper_subformula_of 'not' H;

theorem :: QC_LANG2:87
   'not' F is_subformula_of H implies F is_proper_subformula_of H;

theorem :: QC_LANG2:88
   F is_proper_subformula_of FALSUM iff F is_subformula_of VERUM;

theorem :: QC_LANG2:89
  F is_subformula_of G or F is_subformula_of H iff
   F is_proper_subformula_of G '&' H;

theorem :: QC_LANG2:90
   F '&' G is_subformula_of H implies
   F is_proper_subformula_of H & G is_proper_subformula_of H;

theorem :: QC_LANG2:91
  F is_subformula_of H iff F is_proper_subformula_of All(x,H);

theorem :: QC_LANG2:92
   All(x,H) is_subformula_of F implies H is_proper_subformula_of F;

theorem :: QC_LANG2:93
   F '&' 'not' G is_proper_subformula_of F => G &
  F is_proper_subformula_of F => G &
   'not' G is_proper_subformula_of F => G &
    G is_proper_subformula_of F => G;

theorem :: QC_LANG2:94
   'not' F '&' 'not' G is_proper_subformula_of F 'or' G &
  'not' F is_proper_subformula_of F 'or' G &
   'not' G is_proper_subformula_of F 'or' G &
    F is_proper_subformula_of F 'or' G &
     G is_proper_subformula_of F 'or' G;

theorem :: QC_LANG2:95
    H is atomic implies not F is_proper_subformula_of H;

theorem :: QC_LANG2:96
    H is negative implies the_argument_of H is_proper_subformula_of H;

theorem :: QC_LANG2:97
    H is conjunctive implies
   the_left_argument_of H is_proper_subformula_of H &
    the_right_argument_of H is_proper_subformula_of H;

theorem :: QC_LANG2:98
    H is universal implies the_scope_of H is_proper_subformula_of H;

theorem :: QC_LANG2:99
  H is_subformula_of VERUM iff H = VERUM;

theorem :: QC_LANG2:100
  H is_subformula_of P!V iff H = P!V;

theorem :: QC_LANG2:101
  H is_subformula_of FALSUM iff H = FALSUM or H = VERUM;

::
::   Set of subformulae of QC-formulae
::

 definition let H;
  func Subformulae H -> set means
:: QC_LANG2:def 23
  for a being set holds a in it iff ex F st F = a & F is_subformula_of H;
 end;

canceled;

theorem :: QC_LANG2:103
  G in Subformulae H implies G is_subformula_of H;

theorem :: QC_LANG2:104
  F is_subformula_of H implies Subformulae F c= Subformulae H;

theorem :: QC_LANG2:105
   G in Subformulae H implies Subformulae G c= Subformulae H;

canceled;

theorem :: QC_LANG2:107
  Subformulae(VERUM) = { VERUM };

theorem :: QC_LANG2:108
  Subformulae(P!V) = { P!V };

theorem :: QC_LANG2:109
   Subformulae(FALSUM) = { VERUM, FALSUM };

theorem :: QC_LANG2:110
  Subformulae 'not' H = Subformulae H \/ { 'not' H };

theorem :: QC_LANG2:111
  Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F };

theorem :: QC_LANG2:112
  Subformulae All(x,H) = Subformulae H \/ { All(x,H) };

theorem :: QC_LANG2:113
 Subformulae (F => G) =
   Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G };

theorem :: QC_LANG2:114
   Subformulae (F 'or' G) =
   Subformulae F \/ Subformulae G \/ {'not' G, 'not' F, 'not' F '&' 'not'
G, F 'or' G};

theorem :: QC_LANG2:115
   Subformulae (F <=> G) =
  Subformulae F \/ Subformulae G \/
   { 'not' G, F '&' 'not' G, F => G, 'not' F, G '&' 'not' F, G => F, F <=> G };

theorem :: QC_LANG2:116
    H = VERUM or H is atomic iff Subformulae H = { H };

theorem :: QC_LANG2:117
    H is negative implies
   Subformulae H = Subformulae the_argument_of H \/ { H };

theorem :: QC_LANG2:118
    H is conjunctive implies
   Subformulae H = Subformulae the_left_argument_of H \/
    Subformulae the_right_argument_of H \/ { H };

theorem :: QC_LANG2:119
    H is universal implies
   Subformulae H = Subformulae the_scope_of H \/ { H };

theorem :: QC_LANG2:120
    (H is_immediate_constituent_of G or H is_proper_subformula_of G or
   H is_subformula_of G) & G in Subformulae F implies H in Subformulae F;