Метатеоремы: оффтоп

[Batrak]

Меня всегда изумляла эта противоестественность между "или" строгим, т.е. исключающим, как в языках программирования, и этим "сопливым "или" (т.е. импликацией) в логике. Когда доказательство - это последовательность строк (алгоритмически в них только XOR), а вывод - некая строка, которая "выводима" (посредством "сопливого "или"), т.е. импликации, из этого естественно растут противоречия между доказуемостью ($\vdash$) и истинностью ($\to$).

Lia: Оффтоп из «Метатеоремы»

[epros]

Batrak в сообщении #1429002 писал(а):

Меня всегда изумляла эта противоестественность между "или" строгим, т.е. исключающим, как в языках программирования, и этим "сопливым "или" (т.е. импликацией) в логике.

"Или", "исключающее или" (оно же - "не равносильно") и импликация - это три разные логические связки.

Batrak в сообщении #1429002 писал(а):

(алгоритмически в них только XOR)

Что бы это значило?

Логический вывод и доказательство - это одно и то же, а именно, конечная последовательность предложений. Последнее предложение в доказательстве выводимо вовсе не "посредством импликации". Но в силу теоремы дедукции если первым предложением доказательства является гипотеза (это называется "условное доказательство"), то безусловно доказана импликация с первым предложением в антецеденте и последним предложением в консеквенте.