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

### Connectives and Subformulae of the First Order Language

by
Grzegorz Bancerek

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;
```