:: Connectives and Subformulae of the First Order Language
:: by Grzegorz Bancerek
::
:: Received November 23, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: QC_LANG2:1
canceled;
theorem Th2: :: QC_LANG2:2
theorem Th3: :: QC_LANG2:3
theorem Th4: :: QC_LANG2:4
theorem Th5: :: QC_LANG2:5
theorem Th6: :: QC_LANG2:6
theorem Th7: :: QC_LANG2:7
theorem Th8: :: QC_LANG2:8
:: deftheorem defines FALSUM QC_LANG2:def 1 :
:: deftheorem defines => QC_LANG2:def 2 :
:: deftheorem defines 'or' QC_LANG2:def 3 :
:: deftheorem defines <=> QC_LANG2:def 4 :
:: deftheorem defines Ex QC_LANG2:def 5 :
theorem :: QC_LANG2:9
canceled;
theorem :: QC_LANG2:10
canceled;
theorem :: QC_LANG2:11
canceled;
theorem :: QC_LANG2:12
canceled;
theorem :: QC_LANG2:13
theorem :: QC_LANG2:14
theorem :: QC_LANG2:15
canceled;
theorem :: QC_LANG2:16
theorem Th17: :: QC_LANG2:17
theorem :: QC_LANG2:18
theorem Th19: :: QC_LANG2:19
definition
let x,
y be
bound_QC-variable;
let p be
Element of
QC-WFF ;
func All x,
y,
p -> QC-formula equals :: QC_LANG2:def 6
All x,
(All y,p);
correctness
coherence
All x,(All y,p) is QC-formula;
;
func Ex x,
y,
p -> QC-formula equals :: QC_LANG2:def 7
Ex x,
(Ex y,p);
correctness
coherence
Ex x,(Ex y,p) is QC-formula;
;
end;
:: deftheorem defines All QC_LANG2:def 6 :
:: deftheorem defines Ex QC_LANG2:def 7 :
theorem :: QC_LANG2:20
theorem Th21: :: QC_LANG2:21
theorem :: QC_LANG2:22
theorem Th23: :: QC_LANG2:23
theorem :: QC_LANG2:24
theorem :: QC_LANG2:25
definition
let x,
y,
z be
bound_QC-variable;
let 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);
correctness
coherence
All x,(All y,z,p) is QC-formula;
;
func Ex x,
y,
z,
p -> QC-formula equals :: QC_LANG2:def 9
Ex x,
(Ex y,z,p);
correctness
coherence
Ex x,(Ex y,z,p) is QC-formula;
;
end;
:: deftheorem defines All QC_LANG2:def 8 :
:: deftheorem defines Ex QC_LANG2:def 9 :
theorem :: QC_LANG2:26
for
x,
y,
z being
bound_QC-variable for
p being
Element of
QC-WFF holds
(
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
p1,
p2 being
Element of
QC-WFF 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 )
theorem :: QC_LANG2:28
theorem :: QC_LANG2:29
for
x,
y,
z being
bound_QC-variable for
p,
q being
Element of
QC-WFF for
t,
s being
bound_QC-variable st
All x,
y,
z,
p = All t,
s,
q holds
(
x = t &
y = s &
All z,
p = q )
theorem :: QC_LANG2:30
for
p1,
p2 being
Element of
QC-WFF 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
theorem :: QC_LANG2:32
for
x,
y,
z being
bound_QC-variable for
p,
q being
Element of
QC-WFF for
t,
s being
bound_QC-variable st
Ex x,
y,
z,
p = Ex t,
s,
q holds
(
x = t &
y = s &
Ex z,
p = q )
theorem :: QC_LANG2:33
for
x,
y,
z being
bound_QC-variable for
p being
Element of
QC-WFF holds
(
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 )
by Th8, QC_LANG1:def 20;
:: deftheorem defines disjunctive QC_LANG2:def 10 :
:: deftheorem Def11 defines conditional QC_LANG2:def 11 :
:: deftheorem defines biconditional QC_LANG2:def 12 :
:: deftheorem Def13 defines existential QC_LANG2:def 13 :
theorem :: QC_LANG2:34
canceled;
theorem :: QC_LANG2:35
canceled;
theorem :: QC_LANG2:36
canceled;
theorem :: QC_LANG2:37
canceled;
theorem :: QC_LANG2:38
:: deftheorem defines the_left_disjunct_of QC_LANG2:def 14 :
:: deftheorem defines the_right_disjunct_of QC_LANG2:def 15 :
:: deftheorem defines the_antecedent_of QC_LANG2:def 16 :
:: deftheorem QC_LANG2:def 17 :
canceled;
:: deftheorem defines the_left_side_of QC_LANG2:def 18 :
:: deftheorem defines the_right_side_of QC_LANG2:def 19 :
theorem :: QC_LANG2:39
canceled;
theorem :: QC_LANG2:40
canceled;
theorem :: QC_LANG2:41
canceled;
theorem :: QC_LANG2:42
canceled;
theorem :: QC_LANG2:43
canceled;
theorem :: QC_LANG2:44
canceled;
theorem Th45: :: QC_LANG2:45
theorem Th46: :: QC_LANG2:46
theorem Th47: :: QC_LANG2:47
theorem :: QC_LANG2:48
theorem :: QC_LANG2:49
theorem :: QC_LANG2:50
theorem :: QC_LANG2:51
theorem :: QC_LANG2:52
theorem :: QC_LANG2:53
theorem :: QC_LANG2:54
theorem :: QC_LANG2:55
theorem :: QC_LANG2:56
:: deftheorem Def20 defines is_immediate_constituent_of QC_LANG2:def 20 :
theorem :: QC_LANG2:57
canceled;
theorem Th58: :: QC_LANG2:58
theorem Th59: :: QC_LANG2:59
theorem Th60: :: QC_LANG2:60
theorem :: QC_LANG2:61
theorem Th62: :: QC_LANG2:62
theorem Th63: :: QC_LANG2:63
theorem Th64: :: QC_LANG2:64
theorem Th65: :: QC_LANG2:65
theorem Th66: :: QC_LANG2:66
theorem Th67: :: QC_LANG2:67
:: deftheorem Def21 defines is_subformula_of QC_LANG2:def 21 :
:: deftheorem Def22 defines is_proper_subformula_of QC_LANG2:def 22 :
theorem :: QC_LANG2:68
canceled;
theorem :: QC_LANG2:69
canceled;
theorem :: QC_LANG2:70
canceled;
theorem Th71: :: QC_LANG2:71
theorem Th72: :: QC_LANG2:72
theorem Th73: :: QC_LANG2:73
theorem Th74: :: QC_LANG2:74
theorem Th75: :: QC_LANG2:75
theorem Th76: :: QC_LANG2:76
theorem Th77: :: QC_LANG2:77
theorem Th78: :: QC_LANG2:78
theorem Th79: :: QC_LANG2:79
theorem :: QC_LANG2:80
theorem Th81: :: QC_LANG2:81
theorem Th82: :: QC_LANG2:82
theorem Th83: :: QC_LANG2:83
theorem :: QC_LANG2:84
theorem Th85: :: QC_LANG2:85
theorem Th86: :: QC_LANG2:86
theorem :: QC_LANG2:87
theorem :: QC_LANG2:88
theorem Th89: :: QC_LANG2:89
theorem :: QC_LANG2:90
theorem Th91: :: QC_LANG2:91
theorem :: QC_LANG2:92
theorem :: QC_LANG2:93
theorem :: QC_LANG2:94
theorem :: QC_LANG2:95
theorem :: QC_LANG2:96
theorem :: QC_LANG2:97
theorem :: QC_LANG2:98
theorem Th99: :: QC_LANG2:99
theorem Th100: :: QC_LANG2:100
theorem Th101: :: QC_LANG2:101
:: deftheorem Def23 defines Subformulae QC_LANG2:def 23 :
theorem :: QC_LANG2:102
canceled;
theorem Th103: :: QC_LANG2:103
theorem Th104: :: QC_LANG2:104
theorem :: QC_LANG2:105
theorem :: QC_LANG2:106
canceled;
theorem Th107: :: QC_LANG2:107
theorem Th108: :: QC_LANG2:108
theorem :: QC_LANG2:109
theorem Th110: :: QC_LANG2:110
theorem Th111: :: QC_LANG2:111
theorem Th112: :: QC_LANG2:112
theorem Th113: :: QC_LANG2:113
theorem :: QC_LANG2:114
theorem :: QC_LANG2:115
theorem :: QC_LANG2:116
theorem :: QC_LANG2:117
theorem :: QC_LANG2:118
theorem :: QC_LANG2:119
theorem :: QC_LANG2:120