/
test.tex
286 lines (273 loc) · 9.75 KB
/
test.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
\documentclass[landscape]{article}
\usepackage[a4paper,margin=0.5in,landscape]{geometry}
\newcommand{\Tarrowintro}{$\rightarrow$I}
\newcommand{\Tarrowelim}{$\rightarrow$E}
\newcommand{\Tconjintro}{$\land$I}
\newcommand{\Tconjelim}{$\land$E}
\newcommand{\Tdisjintro}{$\lor$I}
\newcommand{\Tdisjelim}{$\lor$E}
\newcommand{\Tunivintro}{$\forall$I}
\newcommand{\Tunivelim}{$\forall$E}
\newcommand{\Texistintro}{$\exists$I}
\newcommand{\Texistelim}{$\exists$E}
\newcommand{\Tarrow}{\rightarrow}
\newcommand{\Tand}{\land}
\newcommand{\Tor}{\lor}
\newcommand{\Tforall}{\forall}
\newcommand{\Texists}{\exists}
\newcommand{\Tneg}{\lnot}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\Tneg{\Tneg{\left(A \Tor \Tneg{A}\right)}} \Tarrow \left(A \Tor \Tneg{A}\right)$}
\AxiomC{[$\Tneg{\left(A \Tor \Tneg{A}\right)}$]}
\AxiomC{[$\Tneg{\left(A \Tor \Tneg{A}\right)}$]}
\AxiomC{[$A$]}
\RightLabel{\Tdisjintro}
\UnaryInfC{$A \Tor \Tneg{A}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{A}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$A \Tor \Tneg{A}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tneg{\left(A \Tor \Tneg{A}\right)}}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$A \Tor \Tneg{A}$}
\end{prooftree}
\vspace{1cm}
\begin{prooftree}
\AxiomC{}
\RightLabel{DP}
\UnaryInfC{$\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)$}
\AxiomC{[$\Tneg{\Tforall_{x} P{x}}$]}
\AxiomC{[$P{x} \Tarrow \Tforall_{x} P{x}$]}
\AxiomC{[$P{x}$]}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\Tforall_{x} P{x}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{P{x}}$}
\RightLabel{\Texistintro}
\UnaryInfC{$\Texists_{x} \Tneg{P{x}}$}
\RightLabel{\Texistelim}
\BinaryInfC{$\Texists_{x} \Tneg{P{x}}$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tforall_{x} P{x}} \Tarrow \Texists_{x} \Tneg{P{x}}$}
\end{prooftree}
\vspace{1cm}
\begin{prooftree}
\AxiomC{}
\RightLabel{DP}
\UnaryInfC{$\Texists_{x} \left(\left(P{x} \Tarrow Q{x}\right) \Tarrow \Tforall_{x} \left(P{x} \Tarrow Q{x}\right)\right)$}
\AxiomC{[$\Tneg{\Tforall_{x} \left(P{x} \Tarrow Q{x}\right)}$]}
\AxiomC{[$\left(P{x} \Tarrow Q{x}\right) \Tarrow \Tforall_{x} \left(P{x} \Tarrow Q{x}\right)$]}
\AxiomC{[$P{x} \Tarrow Q{x}$]}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\Tforall_{x} \left(P{x} \Tarrow Q{x}\right)$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\left(P{x} \Tarrow Q{x}\right)}$}
\RightLabel{\Texistintro}
\UnaryInfC{$\Texists_{x} \Tneg{\left(P{x} \Tarrow Q{x}\right)}$}
\RightLabel{\Texistelim}
\BinaryInfC{$\Texists_{x} \Tneg{\left(P{x} \Tarrow Q{x}\right)}$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tforall_{x} \left(P{x} \Tarrow Q{x}\right)} \Tarrow \Texists_{x} \Tneg{\left(P{x} \Tarrow Q{x}\right)}$}
\end{prooftree}
\vspace{1cm}
\begin{prooftree}
\AxiomC{}
\RightLabel{DP}
\UnaryInfC{$\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)$}
\AxiomC{[$\Tforall_{x} \left(P{x} \Tor Q{x}\right)$]}
\RightLabel{\Tunivelim}
\UnaryInfC{$P{x} \Tor Q{x}$}
\AxiomC{[$P{x} \Tarrow \Tforall_{x} P{x}$]}
\AxiomC{[$P{x}$]}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\Tforall_{x} P{x}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$\Tforall_{x} P{x} \Tor \Texists_{x} Q{x}$}
\AxiomC{[$Q{x}$]}
\RightLabel{\Texistintro}
\UnaryInfC{$\Texists_{x} Q{x}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$\Tforall_{x} P{x} \Tor \Texists_{x} Q{x}$}
\RightLabel{\Tdisjelim}
\TrinaryInfC{$\Tforall_{x} P{x} \Tor \Texists_{x} Q{x}$}
\RightLabel{\Texistelim}
\BinaryInfC{$\Tforall_{x} P{x} \Tor \Texists_{x} Q{x}$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tforall_{x} \left(P{x} \Tor Q{x}\right) \Tarrow \left(\Tforall_{x} P{x} \Tor \Texists_{x} Q{x}\right)$}
\end{prooftree}
\clearpage
\begin{prooftree}
\AxiomC{}
\RightLabel{GLPO}
\UnaryInfC{$\Tforall_{x} \Tneg{A} \Tor \Texists_{x} A$}
\AxiomC{[$\Tforall_{x} \Tneg{A}$]}
\RightLabel{\Tunivelim}
\UnaryInfC{$\Tneg{A}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$A \Tor \Tneg{A}$}
\AxiomC{[$\Texists_{x} A$]}
\AxiomC{[$A$]}
\RightLabel{\Texistelim}
\BinaryInfC{$A$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$A \Tor \Tneg{A}$}
\RightLabel{\Tdisjelim}
\TrinaryInfC{$A \Tor \Tneg{A}$}
\end{prooftree}
\vspace{1cm}
\begin{prooftree}
\AxiomC{}
\RightLabel{GLPO}
\UnaryInfC{$\Tforall_{x} \Tneg{P{y}} \Tor \Texists_{x} P{y}$}
\AxiomC{[$\Tforall_{x} \Tneg{P{y}}$]}
\RightLabel{\Tunivelim}
\UnaryInfC{$\Tneg{P{y}}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$P{y} \Tor \Tneg{P{y}}$}
\AxiomC{[$\Texists_{x} P{y}$]}
\AxiomC{[$P{y}$]}
\RightLabel{\Texistelim}
\BinaryInfC{$P{y}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$P{y} \Tor \Tneg{P{y}}$}
\RightLabel{\Tdisjelim}
\TrinaryInfC{$P{y} \Tor \Tneg{P{y}}$}
\RightLabel{\Tunivintro}
\UnaryInfC{$\Tforall_{y} \left(P{y} \Tor \Tneg{P{y}}\right)$}
\RightLabel{\Tunivelim}
\UnaryInfC{$P{x} \Tor \Tneg{P{x}}$}
\end{prooftree}
\vspace{1cm}
\begin{prooftree}
\AxiomC{}
\RightLabel{GLPO}
\UnaryInfC{$\Tforall_{x} \Tneg{P{y}} \Tor \Texists_{x} P{y}$}
\AxiomC{[$\Tforall_{x} \Tneg{P{y}}$]}
\RightLabel{\Tunivelim}
\UnaryInfC{$\Tneg{P{y}}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$P{y} \Tor \Tneg{P{y}}$}
\AxiomC{[$\Texists_{x} P{y}$]}
\AxiomC{[$P{y}$]}
\RightLabel{\Texistelim}
\BinaryInfC{$P{y}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$P{y} \Tor \Tneg{P{y}}$}
\RightLabel{\Tdisjelim}
\TrinaryInfC{$P{y} \Tor \Tneg{P{y}}$}
\end{prooftree}
\vspace{1cm}
\begin{prooftree}
\AxiomC{}
\RightLabel{GLPO}
\UnaryInfC{$\Tforall_{x} \Tneg{\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)} \Tor \Texists_{x} \left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)$}
\AxiomC{[$\Tforall_{x} \Tneg{\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)}$]}
\RightLabel{\Tunivelim}
\UnaryInfC{$\Tneg{\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right) \Tor \Tneg{\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)}$}
\AxiomC{[$\Texists_{x} \left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)$]}
\AxiomC{[$P{y} \Tand \Tneg{\Tforall_{x} P{x}}$]}
\RightLabel{\Texistelim}
\BinaryInfC{$P{y} \Tand \Tneg{\Tforall_{x} P{x}}$}
\RightLabel{\Tdisjintro}
\UnaryInfC{$\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right) \Tor \Tneg{\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)}$}
\RightLabel{\Tdisjelim}
\TrinaryInfC{$\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right) \Tor \Tneg{\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)}$}
\RightLabel{\Tunivintro}
\UnaryInfC{$\Tforall_{y} \left(\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right) \Tor \Tneg{\left(P{y} \Tand \Tneg{\Tforall_{x} P{x}}\right)}\right)$}
\RightLabel{\Tunivelim}
\UnaryInfC{$\left(P{x} \Tand \Tneg{\Tforall_{x} P{x}}\right) \Tor \Tneg{\left(P{x} \Tand \Tneg{\Tforall_{x} P{x}}\right)}$}
\end{prooftree}
\clearpage
\begin{prooftree}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\Tneg{\Tneg{\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)}} \Tarrow \Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)$}
\AxiomC{[$\Tneg{\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)}$]}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\Tneg{\Tneg{P{x}}} \Tarrow P{x}$}
\AxiomC{[$\Tneg{\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)}$]}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\Tneg{\Tneg{\Tforall_{x} P{x}}} \Tarrow \Tforall_{x} P{x}$}
\AxiomC{[$\Tneg{P{x}}$]}
\AxiomC{[$P{x}$]}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tneg{\Tforall_{x} P{x}}}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\Tforall_{x} P{x}$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$P{x} \Tarrow \Tforall_{x} P{x}$}
\RightLabel{\Texistintro}
\UnaryInfC{$\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tneg{P{x}}}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$P{x}$}
\RightLabel{\Tunivintro}
\UnaryInfC{$\Tforall_{x} P{x}$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$P{x} \Tarrow \Tforall_{x} P{x}$}
\RightLabel{\Texistintro}
\UnaryInfC{$\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tneg{\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)}}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\Texists_{x} \left(P{x} \Tarrow \Tforall_{x} P{x}\right)$}
\end{prooftree}
\begin{prooftree}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\Tneg{\Tneg{\Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)}} \Tarrow \Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)$}
\AxiomC{[$\Tneg{\Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)}$]}
\AxiomC{}
\RightLabel{DNE}
\UnaryInfC{$\Tneg{\Tneg{P{x}}} \Tarrow P{x}$}
\AxiomC{[$\Texists_{x} P{x}$]}
\AxiomC{[$\Tneg{\Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)}$]}
\AxiomC{[$P{x}$]}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Texists_{x} P{x} \Tarrow P{x}$}
\RightLabel{\Texistintro}
\UnaryInfC{$\Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Texistelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tneg{P{x}}}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$P{x}$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Texists_{x} P{x} \Tarrow P{x}$}
\RightLabel{\Texistintro}
\UnaryInfC{$\Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\bot$}
\RightLabel{\Tarrowintro}
\UnaryInfC{$\Tneg{\Tneg{\Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)}}$}
\RightLabel{\Tarrowelim}
\BinaryInfC{$\Texists_{x} \left(\Texists_{x} P{x} \Tarrow P{x}\right)$}
\end{prooftree}
\end{document}