Свойство дизъюнкции - проблема классической логики?

[epros]

Свойство дизъюнкции считается одной из отличительных характеристик, которыми должны обладать конструктивные теории. Оно означает, что если дизъюнкция является теоремой, то теоремой является хотя бы один из аргументов дизъюнкции. Или в формальной записи в мета-теории, рассматривающей теорию $T$:
$(T \vdash a \vee b) \to ((T \vdash a) \vee (T \vdash b))$.

Однако в классическом исчислении высказываний является тавтологией следующее утверждение:
$(c \to (a \vee b)) \to ((c \to a) \vee (c \to b))$.

Или, применив теорему дедукции (т.е. перейдя от импликаций к утверждениям о "выводимости"):
$(c \vdash (a \vee b)) \to ((c \vdash a) \vee (c \vdash b))$.

Получается, что если рассматривать утверждение $c$ как аксиоматику теории $T$ "в совокупности" (в этом есть некоторая натяжка, но вспомним, что аксиоматика теории может состоять и из единственной аксиомы), в классической логике теория должна обладать свойством дизъюнкции "автоматически", т.е. если $a \vee b$ теорема, то автоматически можно утверждать, что "либо $a$ теорема, либо $b$ теорема". Но очевидно, что существуют теории в классической логике, которые свойством дизъюнкции не обладают, т.е. некое $a \vee b$ может быть теоремой (и даже аксиомой), но ни $a$, ни $b$ теоремами не будут, а значит утверждение $(T \vdash a \vee b) \to ((T \vdash a) \vee (T \vdash b))$ ,будет ложным.

Противоречие? В чём подвох?

[arseniiv]

А чего, конкретных примеров (классических) теорий, не обладающих таким свойством, не известно?

-- Пн июн 11, 2018 01:29:01 --

epros в сообщении #1318828 писал(а):

Или, применив теорему дедукции (т.е. перейдя от импликаций к утверждениям о "выводимости"):
$(c \vdash (a \vee b)) \to ((c \vdash a) \vee (c \vdash b))$.

Как именно вы это сделали?

[mihaild]

epros в сообщении #1318828 писал(а):

т.е. перейдя от импликаций к утверждениям о "выводимости"

Нельзя делать такой переход внутри формулы: теорема о дедукции - из метатеории, а дизъюнкция справа - из теории.

[george66]

Пронести штопор через дизъюнкцию нельзя, теорема о дедукции позволяет из
$c\vdash(a\vee b)$
получить
$\vdash c\to(a\vee b)$
и дальше
$\vdash(c\to a)\vee(c\to b)$
и всё.

[epros]

Рассуждаем в мета-теории с применением исчисления высказываний (оно ведь в ней тоже работает).
1) Гипотеза первого уровня: $c \vdash (a \vee b)$.
2) Гипотеза второго уровня: $c$.
3) Применяем правило 1 к 2: $a \vee b$ (это даже не модус поненс, поскольку у нас есть правило вывода, преподнесённое на блюдечке в виде гипотезы).
4) Дедукция от 2 до 3: $c \to (a \vee b)$.
5) Дедукция от 1 до 4: $(c \vdash (a \vee b)) \to (c \to (a \vee b))$ (вывод, который нам и требовалось получить).

Далее остаётся применить полученный вывод к тавтологии $(c \to (a \vee b)) \to ((c \to a) \vee (c \to b))$ и получить $(c \vdash (a \vee b)) \to ((c \to a) \vee (c \to b))$. С заменой "$\to$" на "$\vdash$" в двух других местах тавтологии действуем похожим образом.

Что здесь не так?

-- Пн июн 11, 2018 12:47:29 --

Теперь про пронесение штопора через дизъюнкцию:
1) Гипотеза первого уровня: $c \to a$,
2) Гипотеза второго уровня: $c$.
3) Модус поненс из 2 и 1: $a$.
4) Констатируем вывод от 2 до 3: $c \vdash a$ (это даже не дедукция, поскольку нам импликация не нужна).
5) Дедукция от 1 до 4: $(c \to a) \to (c \vdash a)$.

Аналогично выводим $(c \to b) \to (c \vdash b)$.

Далее из дизъюнкции: $(c \to a) \vee (c \to b)$ с применением $(c \to a) \to (c \vdash a)$ получаем $(c \vdash a) \vee (c \to b)$, а с применением $(c \to b) \to (c \vdash b)$ получаем $(c \vdash a) \vee (c \vdash b)$.

[epros]

P.S. Я понял идею о том, что из $\vdash (c \to a) \vee (c \to b)$ не выводится $(\vdash c \to a) \vee (\vdash c \to b)$, но я не понял, почему мы вообще должны ставить штопор, когда применяем условный вывод. Допустим из некоторого $x$ выводится некоторый $y$:
1) Гипотеза $x$.
... шаги вывода ...
N) Так или иначе получаем $y$.
N+1) Дедукция от 1 до N: $x \to y$ или $\vdash x \to y$?

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

[arseniiv]

epros в сообщении #1318883 писал(а):

Но ведь в нашей теории действует аксиоматика того же исчисления высказываний и ничего более.

Может быть, например, менее. Как минимум, у нас может быть интуиционистская логика. Мы можем формализовать метатеорию и вообще иначе, какой-нибудь теорией типов.

-- Пн июн 11, 2018 15:13:48 --

И вообще одного исчисления высказываний, разумеется, мало для формализации вывода, и вы опять же в курсе. Наверно, вы хотели сказать, что достаточно классической системы, а не конкретно классического ИВ?

-- Пн июн 11, 2018 15:16:08 --

Потом вы там наверху смешиваете вещи наподобие

epros в сообщении #1318877 писал(а):

$(c \vdash (a \vee b)) \to (c \to (a \vee b))$

epros в сообщении #1318877 писал(а):

$(c \to a) \to (c \vdash a)$

Этого вообще не ожидал. Какую семантику вы таким конструкциям приписываете? Формула теории не есть формула метатеории.

[george66]

$\vdash$ вообще не является логической связкой и внутри формулы стоять не может. Если мы пишем что-то вроде
$(c\vdash a)\vee (c\vdash b)$
это уже не формула той теории, для которой мы доказывали теорему о дедукции. В той теории, для которой доказывали теорему о дедукции, выводятся выражения вида
$\varphi_1,\ldots,\varphi_n\vdash\psi$
где $n\geqslant 0$ (секвенции) и больше ничего.

[epros]

arseniiv в сообщении #1318914 писал(а):

Какую семантику вы таким конструкциям приписываете? Формула теории не есть формула метатеории.

Как я сказал, рассуждаем в мета-теории. В данном случае это такая теория, которая может говорить о выводимости чего-то из чего-то, для этого в её языке предусмотрен символ штопора. Но в остальном это обычная теория в классической логике, т.е. тавтологии классического исчисления высказываний для неё закон. И какие-то собственные выводы из чего-то она тоже может делать, как и любая теория. Об исчислении предикатов не говорю, ибо здесь ничего выходящего за пределы исчисления высказываний не используется.

george66 в сообщении #1318952 писал(а):

Если мы пишем что-то вроде
$(c\vdash a)\vee (c\vdash b)$
это уже не формула той теории, для которой мы доказывали теорему о дедукции.

Хм. Вот это интересно. $c \vdash a$ - это ведь законная формула теории, которая оперирует понятием "выводимости" и для этого в её языке предусмотрен символ штопора. Почему в ней вдруг станет незаконным применение теоремы дедукции? Насколько я знаю, теорема дедукции доказывается не для отдельных, а для всех теорий в исчислении (высказываний или предикатов). И вообще, сама теорема дедукции: Если $a \vdash b$ то $\vdash a \to b$ - записывается со штопором внутри формулы.

[george66]

epros в сообщении #1319104 писал(а):

george66 в сообщении #1318952 писал(а):

Если мы пишем что-то вроде
$(c\vdash a)\vee (c\vdash b)$
это уже не формула той теории, для которой мы доказывали теорему о дедукции.

Хм. Вот это интересно. $c \vdash a$ - это ведь законная формула теории, которая оперирует понятием "выводимости" и для этого в её языке предусмотрен символ штопора. Почему в ней вдруг станет незаконным применение теоремы дедукции? Насколько я знаю, теорема дедукции доказывается не для отдельных, а для всех теорий в исчислении (высказываний или предикатов). И вообще, сама теорема дедукции: Если $a \vdash b$ то $\vdash a \to b$ - записывается со штопором внутри формулы.

Допустим, у нас есть теория $T$ и штопор означает выводимость в $T$. Та теория, в которой мы можем выписывать формулы вроде $(c\vdash a)\vee(c\vdash b)$ -- это другая теория (метатеория) и к выводимости в ней этот штопор не имеет отношения.

[arseniiv]

epros в сообщении #1319104 писал(а):

Но в остальном это обычная теория в классической логике, т.е. тавтологии классического исчисления высказываний для неё закон. И какие-то собственные выводы из чего-то она тоже может делать, как и любая теория.

Но как понимать одно и то же $a$ в одном месте в контексте теории и в другом в контексте метатеории? Если нет ничего кроме штопора, надо хотя бы доставить его в нужных местах. (Или может лучше сразу в одну из модальных логик перейдём и будем нормальным $\square$ пользоваться?)

[epros]

epros в сообщении #1319104 писал(а):

ибо здесь ничего выходящего за пределы исчисления высказываний не используется

Мммм, здесь я был не совсем точен, ибо как раз выражения типа $c \vdash a$ в исчислении высказываний недопустимы по указанной george66 причине - штопор не является логической связкой, предусмотренной исчислением высказываний. На самом деле это символ бинарного отношения, а $a$ и $b$ - это, соответственно, предметные переменные (ибо то, что для теории является высказыванием, для мета-теории является объектом). Так что исчисление предикатов здесь всё же засветилось, хотя ни кванторы, ни специфичные для исчисления предикатов аксиомы и правила вывода не использовались.

[arseniiv]

В общем вы так и не разобрались, как ваша формализованная метатеория точно выглядит? Конечно всё будет смешиваться.

[epros]

george66 в сообщении #1319109 писал(а):

Допустим, у нас есть теория $T$ и штопор означает выводимость в $T$. Та теория, в которой мы можем выписывать формулы вроде $(c\vdash a)\vee(c\vdash b)$ -- это другая теория (метатеория) и к выводимости в ней этот штопор не имеет отношения.

Не понял. Я полагал, что штопор означает выводимость "в логике". А если мы хотим сказать про выводимость в конкретной теории, то должны слева от штопора в явной форме указать дополнительные (к логическим) аксиомы этой теории.

arseniiv в сообщении #1319110 писал(а):

Но как понимать одно и то же $a$ в одном месте в контексте теории и в другом в контексте метатеории?

Пока не вижу проблемы. Мета-теория использует ту же логику, что и теории, о выводимости в которых она рассуждает. Поэтому $a$ для неё с одной стороны - объект рассмотрения (как высказывание теории), а с другой стороны - её собственное предложение, которое она может утверждать или отрицать, или использовать в логической связке с другими предложениями.

[arseniiv]

epros в сообщении #1319115 писал(а):

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

Я даже честно не знаю как на это отвечать. Это неправильно. Ниоткуда не следует, что так должно быть хоть где-нибудь. Если вам нужна такая метатеория, даже гипотетической несуществующей неподвижной точки $\mu x.\text{мета}x$ не будет достаточно (я даже не буду пытаться придавать этой записи смысл).

Видимо, корень тут:

epros в сообщении #1319115 писал(а):

Мета-теория использует ту же логику, что и теории, о выводимости в которых она рассуждает.

Что значит «ту же логику»? Вон в теории нету никакого $\vdash$, а в метатеории есть. Теория у нас исчисление высказываний, а метатеория, как вы признали, предикатов.

(Оффтоп)

А я могу взять метатеорией типы. Пусть заранее заданы типы пропозициональных переменных $A$, типы унарных связок $O_1$ (один элемент $\neg$) и бинарных связок (элементы $\to,\wedge,\vee,\leftrightarrow$). Определим индуктивный тип пропозициональных формул $F$ с конструкторами $\mathsf{atom}: A\to F$, $\mathsf{unary}: O_1\times F\to F$, $\mathsf{binary}: O_2\times F\times F\to F$. Формула $a\wedge\neg b\to c$ будет, например, представлена элементом $\mathsf{binary}({\to},\mathsf{binary}({\wedge},\mathsf{atom}\,a,\mathsf{unary}({\neg},\mathsf{atom}\,b)),\mathsf{atom}\,c):F$. Впрочем, я мог ввести по конструктору на связку и по конструктору на переменную, и она бы представлялась прям как есть, не важно.

Теперь я могу взять какой-то элемент $f: F$, и он ни в коем разе не будет никак относиться ни к чему в этой метатеории. Утверждения этой метатеории вообще имеют вид лишь $e:T$ да $e_1\equiv e_2:T$.

Метатеория может быть много какой, а вы её связываете таким отождествлением. И вот метатеории с именно такими свойствами как вам надо вообще наверняка не существует.

-- Пн июн 11, 2018 22:22:54 --

Вам может быть интересна provability logic, но это всё равно не то, что вы делаете сейчас.