-
Notifications
You must be signed in to change notification settings - Fork 26
/
lection3.tex
510 lines (419 loc) · 31.7 KB
/
lection3.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
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
\section{Теорема о дедукции}
Соглашение об обозначениях. Будем обозначать буквами
$\Gamma, \Delta, \Sigma, \Pi$ списки формул (возможно, пустые).
\begin{definition}{Вывод из допущений.}
Пусть $\Gamma$ -- некоторый список высказываний, а $\alpha$ ---
некоторое высказывание.
Тогда мы будем говорить, что высказывание $\alpha$ \emph{выводимо} из $\Gamma$
(и записывать это как $\Gamma \vdash \alpha$), если существует такая
последовательность высказываний $\alpha_1, \alpha_2, \dots \alpha_{n-1}, \alpha$
(называемая \emph{выводом} $\alpha$ из $\Gamma$),
что каждое из высказываний $\alpha_i$ --- это
\begin{itemize}
\item либо аксиома,
\vspace{-0.2cm}
\item либо получается по правилу Modus Ponens из предыдущих высказываний,
\vspace{-0.2cm}
\item либо --- высказывание из списка $\Gamma$.
\end{itemize}
Элементы $\Gamma$ мы будем называть \emph{допущениями}. Также эти элементы
называют предположениями или гипотезами.
\end{definition}
В свете данного определения можно заметить, что доказательство --- это
вывод из пустого списка допущений.
\begin{theorem}\label{deduction_theorem}{Теорема о дедукции.}
Утверждение $\Gamma \vdash \alpha \rightarrow \beta$ справедливо тогда и
только тогда, когда справедливо, что $\Gamma, \alpha \vdash \beta$.
\end{theorem}
Для доказательства рассмотрим следующую лемму:
\begin{lemma}
$\vdash \alpha \rightarrow \alpha$
\end{lemma}
\begin{proof}\
\begin{tabular}{lll}
(1) & $\alpha \rightarrow (\alpha \rightarrow \alpha)$&Сх. акс. 1\\
(2) & $(\alpha \rightarrow (\alpha \rightarrow \alpha)) \rightarrow
(\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha)) \rightarrow
(\alpha \rightarrow \alpha)$&Сх. акс. 2\\
(3) & $(\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha)) \rightarrow
(\alpha \rightarrow \alpha)$&M.P. 1,2\\
(4) & $(\alpha \rightarrow ((\alpha \rightarrow \alpha) \rightarrow \alpha))$ & Сх. акс. 1\\
(5) & $\alpha \rightarrow \alpha$ & M.P. 4,3\\
\end{tabular}\
\end{proof}
\begin{proof}[Доказательство теоремы \ref{deduction_theorem}]
Сперва докажем прямое следствие. Для этого нам
достаточно научиться по любому выводу $\alpha \rightarrow \beta$ из $\Gamma$ строить
вывод $\beta$ из $\Gamma, \alpha$. Возьмем вывод
формулы $\alpha \rightarrow \beta$, то есть некоторую последовательность
формул $\delta_1 \dots \delta_{m-1}; \alpha \rightarrow \beta$.
Добавив к выводу 2 формулы, получаем требуемый вывод:
\vspace{0.2cm}
\begin{tabular}{lll}
$(1)$ & $\delta_1$\\
& \dots\\
$(m-1)$ & $\delta_{m-1}$\\
$(m)$ & $\alpha \rightarrow \beta$\\
$(m+1)$ & $\alpha$ & <<Свежедобавленная>> аксиома \\
$(m+2)$ & $\beta$ & M.P. $m$, $m+1$\\
\end{tabular}
\vspace{0.2cm}
Теперь докажем обратное. Нам необходимо построить вывод утверждения
$\Gamma \vdash \alpha \rightarrow \beta$ по имеющемуся выводу
$\delta_1 \dots \delta_{m-1}, \beta$.
Мы поступим так: сперва набросаем план вывода -- разместим по тексту
<<ключевые>> формулы, которые потом дополним до полноценного вывода
промежуточными формулами.
План вывода будет такой:
\begin{tabular}{ll}
$(1)$ & $\Gamma \vdash \alpha \rightarrow \delta_1$\\
\dots\\
$(m-1)$ & $\Gamma \vdash \alpha \rightarrow \delta_{m-1}$\\
$(m)$ & $\Gamma \vdash \alpha \rightarrow \beta$
\end{tabular}
Теперь надо дополнить его до полноценного вывода. Будем рассматривать
формулы подряд и перед каждой формулой добавлять некоторое количество
формул, обосновывающих соответствующий шаг доказательства.
Рассмотрим формулу номер $i$. Возможны следующие варианты:
\begin{enumerate}
\item $\delta_i$ --- это аксиома или предположение, входящее в $\Gamma$.
Тогда перед этой формулой вставим
формулы $\delta_i$ и $\delta_i \rightarrow (\alpha \rightarrow \delta_i)$,
и окажется, что $i$-я формула выводится из предыдущих двух формул
путем применения правила Modus Ponens.
\item $\delta_i$ совпадает с $\alpha$. Тогда мы вставим перед
ней 4 первые формулы из леммы, и $\delta_i \rightarrow \alpha$ будет получаться
по правилу Modus Ponens.
\item $\delta_i$ выводится по правилу Modus Ponens из каких-то других
утверждений $\delta_j$ и $\delta_k$ (при этом
$\delta_k \equiv \delta_j \rightarrow \delta_i$), где $j < i$ и $k < i$.
Покажем, что $\alpha \rightarrow \delta_i$ тоже может быть выведена
из утверждений $\alpha \rightarrow \delta_j$ и
$\alpha \rightarrow (\delta_j \rightarrow \delta_i)$.
Для этого добавим два высказывания:
\begin{tabular}{lll}
$(i - 0.4)$ & $(\alpha \rightarrow \delta_j) \rightarrow ((\alpha \rightarrow (\delta_j \rightarrow \delta_i)) \rightarrow (\alpha \rightarrow \delta_i))$ & Сх. акс. 2\\
$(i - 0.2)$ & $((\alpha \rightarrow (\delta_j \rightarrow \delta_i)) \rightarrow (\alpha \rightarrow \delta_i))$ & M.P. из $j$ и $i-0.4$\\
$i$ & $\alpha \rightarrow \delta_i$ & M.P. из $k$ и $i-0.2$\\
\end{tabular}
\end{enumerate}
\end{proof}
По аналогии мы можем рассмотреть отношение \emph{следования}.
Будем говорить, что высказывание $\alpha$ следует из высказываний $\Gamma$,
если при любой оценке пропозициональных переменных, входящих в высказывания
$\Gamma$ и $\alpha$, на которых все высказывания из $\Gamma$ истинны,
$\alpha$ также истинно.
Записывать, что $\alpha$ следует из $\Gamma$, будем так: $\Gamma \models \alpha$.
\section{Теорема о полноте исчисления высказываний}
\begin{definition}
Введем обозначение. Пусть $\alpha$ --- это некоторое высказывание, а $x$ --- некоторое
истинностное значение. Тогда обозначим за $_{[x]}\alpha$ высказывание
$\alpha$, если $x$ --- истина, и $\neg (\alpha)$, если $x$ --- ложь.
Также, если формула $\alpha$ --- это формула с $n$ пропозициональными переменными
$P_1 \dots P_n$, и $x_1 \dots x_n$ --- некоторые истинностные значения,
то за $\llbracket \alpha \rrbracket^{P_1 \coloneqq x_1, \dots P_n \coloneqq x_n}$ обозначим значение
формулы $\alpha$ при подстановке значений $x_1 \dots x_n$ вместо переменных $P_1 \dots P_n$.
\end{definition}
\begin{lemma}\label{prefix_transposition}
Если $\Gamma, \Sigma \vdash \alpha$, то $\Gamma, \Delta, \Sigma \vdash \alpha$.
Если $\Gamma, \Delta, \Sigma, \Pi \vdash \alpha$, то $\Gamma, \Sigma, \Delta, \Pi \vdash \alpha$.
\end{lemma}
\begin{proof}Упражнение\end{proof}
\begin{lemma}
Если справедливы 3 утверждения: $\Gamma \vdash \gamma$, $\Delta \vdash \delta$ и
$\gamma, \delta \vdash \alpha$, то справедливо и $\Gamma, \Delta \vdash \alpha$
\end{lemma}
\begin{proof}
%Поскольку $\gamma, \delta \vdash \alpha$, то по теореме о дедукции найдется
%доказательство $\gamma \rightarrow \delta \rightarrow \alpha$.
Мы получим требуемый вывод, просто последовательно соединив все три исходных
вывода. Первые два вывода будут (очевидно) корректными при допущениях $\Gamma$
и $\Delta$. В третьем же выводе могут использоваться высказывания $\gamma$ и $\delta$,
отсутствующие в предположениях.
Но поскольку эти высказывания доказаны в первых двух частях вывода, мы будем
иметь полное право их упоминать --- на тех же основаниях, на которых они указаны
в конце соответствующих доказательств.
%Следующая последовательность высказываний является выводом $\alpha$ из
%$\Gamma$ и $\Delta$:
%
%\begin{tabular}{lll}
%$(1) \dots (m)$ & $\gamma_1 \dots \gamma_{m-1}, \gamma$ & Вывод $\Gamma \vdash \gamma$\\
%$(m+1) \dots (n)$ & $\delta_1 \dots \delta_{n-m-1}, \delta$ & Вывод $\Delta \vdash \delta$\\
%$(n+1) \dots (s)$ & $\sigma_1 \dots \sigma_{s-n-1}, \gamma \rightarrow \delta \rightarrow \alpha$ & Вывод $\gamma, \delta \vdash \alpha$\\
%$(s+1)$ & $\delta \rightarrow \alpha$ & M.P. $m$, $s$\\
%$(s+2)$ & $\alpha$ & M.P. $n$, $s+1$\\
%\end{tabular}
\end{proof}
Возьмем некоторую связку исчисления высказываний, например конъюнкцию: $A \with B$.
Построим для нее таблицу истинности. По каждой строчке построим утверждение,
в котором отрицания появляются там, где в таблице истинности находится \emph{Л}:
\begin{tabular}{cccc}
$A$ & $B$ & $A \with B$ & утверждение\\
\hline
Л & Л & Л & $\neg A, \neg B \vdash \neg (A \with B)$\\
Л & И & Л & $\neg A, B \vdash \neg (A \with B)$\\
И & Л & Л & $A, \neg B \vdash \neg (A \with B)$\\
И & И & И & $A, B \vdash A \with B$
\end{tabular}
\begin{lemma}\label{valuation_formula}
Каждое из построенных по таблицам истинности утверждений доказуемо.
\end{lemma}
\begin{proof} Упражнение.
\end{proof}
\begin{lemma}[Правило контрапозиции]\label{contraposition}Каковы бы ни были формулы $\alpha$ и $\beta$, справедливо, что
$\vdash (\alpha \rightarrow \beta) \rightarrow (\neg\beta \rightarrow \neg\alpha)$
\end{lemma}
\begin{proof}
Сперва докажем, что $\alpha \rightarrow \beta, \neg\beta \vdash \neg\alpha$.
\begin{tabular}{lll}
(1) & $(\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \neg\beta) \rightarrow \neg\alpha$ & Сх. акс. 9\\
(2) & $\alpha \rightarrow \beta$ & Допущение\\
(3) & $(\alpha \rightarrow \neg\beta) \rightarrow \neg\alpha$ & M.P. 2,1\\
(4) & $\neg\beta \rightarrow (\alpha \rightarrow \neg\beta)$ & Сх. акс. 1\\
(5) & $\neg\beta$ & Допущение\\
(6) & $\alpha \rightarrow \neg\beta$ & M.P. 5,4\\
(7) & $\neg\alpha$ & M.P. 6,3
\end{tabular}
%\begin{tabular}{lll}
%(1) & $\alpha \rightarrow \neg\neg\beta, \alpha \vdash \alpha \rightarrow \neg\neg\beta$
%\end{tabular}
Тогда, применив 2 раза Теорему о дедукции, получим вывод требуемого утверждения.
\end{proof}
\begin{lemma}{Правило исключенного третьего.}\label{excluded_third} Какова бы ни была формула $\alpha$,
$\vdash \alpha\vee\neg\alpha$
\end{lemma}
\begin{proof}
Доказательство проведем в 3 этапа.
\begin{enumerate}
\item Для начала покажем $\vdash \neg(\alpha\vee\neg\alpha) \rightarrow \neg\alpha$:
\begin{tabular}{lll}
$(1)$ & $\alpha \rightarrow \alpha \vee \neg\alpha$ & Сх. акс. 6\\
% & доказательство из леммы \ref{contraposition} &\\
$(2)\dots(n+1)$ & $\gamma_1,\dots\gamma_{n-1},(\alpha \rightarrow \alpha \vee \neg\alpha) \rightarrow (\neg(\alpha\vee\neg\alpha) \rightarrow \neg\alpha)$ & Д-во из леммы \ref{contraposition}\\
$(n+2)$ & $\neg(\alpha\vee\neg\alpha) \rightarrow \neg\alpha$ & M.P. 1,$n+1$
\end{tabular}
\item
Затем докажем $\vdash \neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha$:
\begin{tabular}{lll}
$(1)$ & $\neg\alpha \rightarrow \alpha \vee \neg\alpha$ & Сх. акс. 7\\
% & доказательство из леммы \ref{contraposition} & \\
$(2)\dots(k+1)$ & $\delta_1, \dots \delta_{k-1}, (\neg\alpha \rightarrow \alpha\vee\neg\alpha) \rightarrow (\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha)$ & Д-во из леммы \ref{contraposition}\\
$(k+2)$ & $\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha$ & M.P. 1,$k+1$\\
\end{tabular}
%Применив теорему о дедукции, получим: $\neg(\alpha\vee\neg\alpha) \vdash \neg\neg\alpha$. Далее,
%в данном допущении, построим следующий вывод:
%
%\begin{tabular}{lll}
%$(1)$ & $\neg\neg\alpha \rightarrow \alpha$ & Сх. акс. 10\\
%$(2)\dots(l+1)$ & $\epsilon_1, \dots \epsilon_{l-1}, \neg\neg\alpha $ & По теореме о дедукции \\
%$(l+2)$ & $\alpha $ & M.P. $l+1$,1
%\end{tabular}
%
%И по теореме о дедукции из данного вывода мы можем получить доказательство
%утверждения $\vdash \neg(\alpha\vee\neg\alpha) \rightarrow \alpha$.
\item
Теперь докажем все вместе:
\begin{tabular}{lll}
%(1) & $\alpha \rightarrow \alpha \vee \neg\alpha$ & Сх. акс. 5\\
% & доказательство из леммы \ref{contraposition} &
%(2) & $(\alpha \rightarrow \alpha \vee \neg\alpha) \rightarrow (\neg(\alpha\vee\neg\alpha) \rightarrow \neg\alpha)$ & по лемме \ref{contraposition}\\
% & \dots сюда вставим доказательство из пункта 1 \dots\\
(1) & $\neg(\alpha\vee\neg\alpha) \rightarrow \neg\alpha$ & по пункту 1\\
%(4) & $\neg\alpha \rightarrow \alpha \vee \neg\alpha$ & Сх. акс. 6\\
% & доказательство из леммы \ref{contraposition} & \\
%(5) & $(\neg\alpha \rightarrow \alpha\vee\neg\alpha) \rightarrow (\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha) & по лемме \ref{contraposition}\\
%(2) & $\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha$ \\
%(7) & $(\neg\neg\alpha \rightarrow \alpha) \rightarrow \neg(\alpha\vee\neg\alpha) \rightarrow (\neg\neg\alpha \rightarrow \alpha)$ & Сх. акс. 1\\
%(8) & $(\neg\neg\alpha \rightarrow \alpha) & Сх. акс. 10\\
%(9) & $\neg(\alpha\vee\neg\alpha) \rightarrow (\neg\neg\alpha \rightarrow \alpha)$ & M.P. 8,7\\
%(10)& $(\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha) \rightarrow (\neg(\alpha\vee\neg\alpha) \rightarrow (\neg\neg\alpha \rightarrow \alpha)) \rightarrow \neg(\alpha\vee\neg\alpha \rightarrow \alpha)$
%(11) & $(\neg(\alpha\vee\neg\alpha) \rightarrow (\neg\neg\alpha \rightarrow \alpha)) \rightarrow \neg(\alpha\vee\neg\alpha \rightarrow \alpha)$ M.P. 6,10\\
%(12) & $\neg(\alpha\vee\neg\alpha \rightarrow \alpha)$
% & по обратной т. к т. о дедукции из (6) можно получить &\\
% & $\neg(\alpha\vee\neg\alpha) \vdash \neg\neg\alhpa$ &\\
% & а затем, применив акс. (10), modus ponens и т. о дедукции: &\\
% & \dots сюда вставим доказательство из пункта 2 dots\\
(2) & $\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha$& по пункту 2\\
(3) & $(\neg(\alpha\vee\neg\alpha) \rightarrow \neg\alpha) \rightarrow (\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha) \rightarrow (\neg\neg(\alpha\vee\neg\alpha))$ & Сх. акс. 9\\
(4) & $(\neg(\alpha\vee\neg\alpha) \rightarrow \neg\neg\alpha) \rightarrow \neg\neg(\alpha\vee\neg\alpha)$ & M.P. 1,3\\
(5) & $\neg\neg(\alpha\vee\neg\alpha)$ & M.P. 2,4\\
(6) & $\neg\neg(\alpha\vee\neg\alpha) \rightarrow (\alpha\vee\neg\alpha)$ & Сх. акс. 10\\
(7) & $\alpha\vee\neg\alpha$ & M.P. 5,6
\end{tabular}
\end{enumerate}
\end{proof}
\begin{lemma}{Об исключении допущения.}
Пусть справедливо $\Gamma, \rho \vdash \alpha$ и $\Gamma, \neg \rho \vdash \alpha$.
Тогда также справедливо $\Gamma \vdash \alpha$.
\end{lemma}
\begin{proof}
Применив теорему о дедукции к условиям теоремы получим следующее:
\begin{tabular}{l}
$\Gamma \vdash \rho \rightarrow \alpha$\\
$\Gamma \vdash \neg \rho \rightarrow \alpha$
\end{tabular}
Тогда следующий вывод покажет $\Gamma \vdash \alpha$:
\begin{tabular}{lll}
$(1) \dots (p)$ & $\gamma_1, \dots \gamma_{p-1}, \rho \rightarrow \alpha$ & Вывод $\Gamma \vdash \rho \rightarrow \alpha$\\
$(p+1) \dots (q)$ & $\delta_1, \dots \delta_{q-p-1}, \neg \rho \rightarrow \alpha$ & Вывод $\Gamma \vdash \neg \rho \rightarrow \alpha$\\
$(q+1) \dots (r)$ & $\epsilon_1, \dots \epsilon_{r-q-1}, \rho \vee \neg \rho$ & Лемма \ref{excluded_third}\\
$(r+1)$ & $(\rho \rightarrow \alpha) \rightarrow (\neg \rho \rightarrow \alpha) \rightarrow (\rho \vee \neg \rho) \rightarrow \alpha$ & Сх. аксиом 8\\
$(r+2)$ & $(\neg \rho \rightarrow \alpha) \rightarrow (\rho \vee \neg \rho \rightarrow \alpha)$ & M.P. $p$, $r+1$\\
$(r+3)$ & $\rho \vee \neg \rho \rightarrow \alpha$ & M.P. $q$, $r+2$\\
$(r+4)$ & $\alpha$ & M.P. $r$, $r+3$
\end{tabular}
\end{proof}
\begin{theorem}{О полноте исчисления высказываний.}
Пусть справедливо $\models \alpha$. Тогда также справедливо, что $\vdash \alpha$.
\end{theorem}
\begin{proof}
Для доказательства теоремы мы докажем чуть более сильное утверждение --- что
для любого $k$ от $0$ до $n$ и любой
оценки переменных $x_1, \dots x_k$ справедливо
$_{[x_1]} P_1, \dots _{[x_k]} P_k \vdash \alpha$.
Нетрудно заметить, что утверждение теоремы непосредственно следует из данного
утверждения для $k=0$.
Доказательство будет вестись индукцией по $n-k$.
База. Пусть $n-k=0$, то есть $k=n$.
$\models \alpha$ означает, что при любой оценке
$x_1, \dots x_n$ пропозициональных переменных $P_1, \dots P_n$
справедливо $\alpha [P_1 \coloneqq x_1, \dots P_n \coloneqq x_n] = \texttt{И}$.
Возьмем некоторую оценку переменных
$x_1, \dots x_n$. Тогда, по лемме \ref{valuation_formula},
$_{[x_1]} P_1, \dots _{[x_{n}]} P_{n} \vdash {_{\alpha [P_1 \coloneqq x_1, \dots P_n \coloneqq x_n]} \alpha}$,
то есть $_{[x_1]} P_1, \dots _{[x_{n}]} P_{n} \vdash \alpha$.
Переход. Пусть утверждение уже доказано для некоторого $n-k > 0$, покажем его
для $n-k+1$ (то есть доказано для $k < n$, покажем его для $k-1$).
Возьмем некоторую оценку переменных $x_1, \dots x_{k-1}$.
По предположению, $_{[x_1]} P_1, \dots _{[x_{k}]} P_{k} \vdash \alpha$, то есть
\begin{tabular}{rl}
$_{[x_1]} P_1, \dots _{[x_{k-1}]} P_{k-1}, \neg P_{k}$ & $\vdash \alpha$\\
$_{[x_1]} P_1, \dots _{[x_{k-1}]} P_{k-1}, P_{k}$ & $\vdash \alpha$
\end{tabular}
Тогда по лемме об исключении допущения справедливо
$_{[x_1]} P_1, \dots _{[x_{k-1}]} P_{k-1} \vdash \alpha$.
\end{proof}
%\begin{lemma}\label{formula_valuation}
%Пусть $\alpha$ --- высказывание от $n$ пропозициональных переменных
%$P_1 \dots P_n$ и пусть выбрана некоторая их оценка $x_1 \dots x_n$.
%Тогда если $_{[x_1]}P_1 \dots _{[x_n]}P_n \vdash _{[y]} \alpha$, то $y = \alpha [x_1, \dots x_n]$
%\end{lemma}
%
%\begin{proof}
%Будем доказывать утверждение индукцией по структуре.
%
%База. Пусть $\alpha$ --- некоторая пропозициональная переменная $P_1$.
%Тогда по условию теоремы $_{[x_1]}P_1 \vdash _{[y]}P_1$. Ясно, что так как
%$P_1 [x_1] = x_1$, то $x = y$.
%\end{proof}
\begin{theorem}{О корректности исчисления высказываний.}
Пусть справедливо $\vdash \alpha$. Тогда также справедливо, что $\models \alpha$.
\end{theorem}
\begin{proof}
По условию теоремы у нас есть доказательство высказывания $\alpha$, то есть
последовательность высказываний $\alpha_1, \dots \alpha_m$.
Каждое высказывание --- это либо аксиома, либо применение правила Modus Ponens.
Докажем, что для каждого $k$ все высказывания $\alpha_l$ при $l \le k$ --- тавтологии.
Доказательство будем вести индукцией по $k$.
База. Пусть $k=0$, тогда нет ни одного высказывания, про которое нужно доказать, что
оно --- тавтология, то есть утверждение автоматически верно.
Переход. Пусть для некоторого $k$ утверждение справедливо, докажем его для $k+1$.
Выберем некоторую оценку $x_1, \dots x_n$ пропозициональных
переменных $P_1, \dots P_n$, использованных в высказываниях $\alpha_1 \dots \alpha_{k+1}$.
Рассмотрим случаи.
Пусть $\alpha_{k+1}$ --- аксиома. В данную аксиому входят одна, две или три формулы
$\beta_1, \beta_2, \beta_3$. Подстановкой всех возможных истинностных значений
вместо данных формул, можно проверить, что все аксиомы являются тавтологиями,
значит, они будут истинны и на тех конкретных значениях, которые примут данные формулы
после подстановки значений $x_1, \dots x_n$.
Пусть $\alpha_{k+1}$ получается по правилу Modus Ponens из $\alpha_p$ и
$\alpha_q$, причем $\alpha_q \equiv \alpha_p \rightarrow \alpha_{k+1}$.
Тогда $\llbracket\alpha_p\rrbracket^{P_1 \coloneqq x_1, \dots P_n\coloneqq x_n} = \texttt{И}$ и
$\llbracket\alpha_p \rightarrow \alpha_{k+1}\rrbracket^{P_1\coloneqq x_1, \dots P_n\coloneqq x_n} = \texttt{И}$.
Из таблицы истинности импликации следует, что неизбежно
$\llbracket\alpha_{k+1}\rrbracket^{P_1\coloneqq x_1, \dots P_n\coloneqq x_n} = \texttt{И}$.
\end{proof}
Заметим, что вместе из этих двух теорем следует, что если неверно, что $\vdash \alpha$,
то неизбежно найдется контрпример.
%
%$\alpha [P_1 \coloneqq \texttt{И}] = \texttt{И}]$,
%и $\alpha [P_1 \coloneqq \texttt{Л}] = \texttt{И}]$.
%Тогда, по лемме ..., справедливо $P_1 \vdash \alpha$ и $\neg P_1 \vdash \alpha$.
%Тогда, по лемме об исключении предположения, справедливо и $\vdash \alpha$.
%
%Переход. Пусть для любой формулы от $n-1$ переменной из $\models \alpha$
%следует $\vdash \alpha$. Рассмотрим некоторую формулу от $n$ переменных $\alpha$,
%с пропозициональными переменными $P_1, \dots P_n$.
%Тогда (по лемме ...) справедливо следующее:
%
%Тогда, если при некотором $k$ и при любой оценке $x_1, \dots x_k$
%переменных $P_1, \dots P_k$
%выполнено $\alpha [P_1 \coloneqq x_1, \dots P_k \coloneqq x_k] = \texttt{И}$, то
%Тогда (по лемме ...) справедливо следующее:
%
%См. Стефан Клини, Математическая логика, М. <<Мир>>, 1973. Глава 1, параграф 12, стр. 61-64.
%
%Данное доказательство изложено не до конца формально, но дальнейшая его формализация
%усложнит изложение, при этом ничего не даст для понимания вопроса. Надеемся, что каждый
%без труда восстановит математическую индукцию, прячущуюся за данным рассуждением.
%Также заметим, что поскольку данное доказательство изложено на метаязыке, эта апелляция
%к интуиции и здравому смыслу не должна нас чрезмерно смущать.
%\end{proof}
\section{Интуиционистское исчисление высказываний}
Заменим аксиому устранения двойного отрицания
на $\phi \rightarrow \neg \phi \rightarrow \psi$.
Полученная система называется интуиционистским исчислением высказываний.
\begin{theorem}\label{no_third_excluded}
В интуиционистском исчислении высказываний невозможно доказать правило
исключенного третьего: $P \vee \neg P$.
\end{theorem}
Мы рассмотрим \emph{модельное} доказательство. То есть, мы построим некоторую модель для
исчисления высказываний --- так определим истинностные значения и связки,
что в нем правило исключенного третьего перестанет быть тавтологией, при этом построенная
нами модель останется корректной.
Пусть множество истинностных значений будет состоять из трех элементов: \texttt{И},
\texttt{Н} и \texttt{Л}. Определим отношение порядка, будем считать, что
$\texttt{И} > \texttt{Н} > \texttt{Л}$.
Все связки на истине и лжи действуют традиционно, необходимо описать только их
поведение с элементом \texttt{Н}.
Для двух операций дадим естественные обобщения.
$A \with B = \min(A,B)$, $A \vee B = \max(A,B)$.
Однако, положим $\neg \texttt{Н} = \texttt{Л}$.
Также, операцию $A \rightarrow B$ положим $\neg A \vee B$, за исключением
$\texttt{Н} \rightarrow \texttt{Н} = \texttt{И}$
Будем считать, что высказывание истинно на некоторой оценке, если оно на ней принимает
значение \texttt{И}. Общезначимость же ($\models \alpha$) означает, что
$\alpha[x_1, \dots x_n] = \texttt{И}$ для любой оценки переменных $x_1, \dots x_n$.
Нетрудно показать, что так определенная модель исчисления является корректной --- то есть
любое утверждение, имеющее доказательство, является тавтологией в смысле данной модели.
\begin{proof}[Доказательство теоремы \ref{no_third_excluded}]
Поскольку $\texttt{Н} \vee \neg \texttt{Н} = \texttt{Н}$, то в данной модели неверно
$\models P \vee \neg P$. Значит, если бы существовало доказательство этого утверждения,
то рассмотренная модель была бы некорректной.
Значит, для интуиционистского исчисления высказываний неверно $\vdash P \vee \neg P$.
\end{proof}
Однако, так построенная логика (с такой моделью) не является полной. Например,
высказывание $\neg P \vee \neg\neg P$, не являющееся доказуемым в интуиционистской
логике, тем не менее оказывается истинным. Сейчас мы рассмотрим другие модели,
обладающие свойством полноты.
\subsection{Топологическая интерпретация интуиционистского исчисления высказываний}
Пусть дано некоторое исчисление высказываний, для которого нам нужно
построить модель --- предложить способ оценки истинности выражений.
Начинаем мы с множества истинностных значений.
Возьмем в качестве этого множества все открытые множества некоторого
заранее выбранного топологического пространства.
Определим оценку для связок интуиционистского исчисления высказываний следующим образом:
\begin{tabular}{l}\\
$\llbracket A \with B \rrbracket = \llbracket A \rrbracket \cap \llbracket B \rrbracket$\\
$\llbracket A \vee B \rrbracket = \llbracket A \rrbracket \cup \llbracket B \rrbracket$\\
$\llbracket A \rightarrow B \rrbracket = (c\llbracket A \rrbracket \cup \llbracket B \rrbracket)^\circ$\\
$\llbracket \neg A \rrbracket = (c \llbracket A \rrbracket)^\circ$
\end{tabular}
Будем считать, что формула истинна в данной модели, если её значение оказалось равно
всему пространству.
Например, возьмем в качестве пространства $\mathbb{R}$, и вычислим значение формулы $A \vee \neg A$
при $A$ равном $(0,1)$: $\llbracket A \vee \neg A \rrbracket = (0,1) \cup \llbracket \neg A \rrbracket =
(0,1) \cup (c(0,1))^\circ = (0,1) \cup ((-\infty,0)\cup(1,\infty)) = (-\infty,0)\cup(0,1)\cup(1,\infty)$.
Нетрудно видеть, что данная формула оказалась не общезначимой в данной интерпретации.
\subsection{Модели Крипке}
См. Шень, Верещагин