2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему На страницу 1, 2  След.
 
 Свойство дизъюнкции - проблема классической логики?
Сообщение10.06.2018, 22:57 
Заслуженный участник
Аватара пользователя


28/09/06
10413
Свойство дизъюнкции считается одной из отличительных характеристик, которыми должны обладать конструктивные теории. Оно означает, что если дизъюнкция является теоремой, то теоремой является хотя бы один из аргументов дизъюнкции. Или в формальной записи в мета-теории, рассматривающей теорию $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))$ ,будет ложным.

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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение10.06.2018, 23:27 
Заслуженный участник


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

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

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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение10.06.2018, 23:52 
Заслуженный участник
Аватара пользователя


16/07/14
8337
Цюрих
epros в сообщении #1318828 писал(а):
т.е. перейдя от импликаций к утверждениям о "выводимости"
Нельзя делать такой переход внутри формулы: теорема о дедукции - из метатеории, а дизъюнкция справа - из теории.

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 07:12 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 11:10 
Заслуженный участник
Аватара пользователя


28/09/06
10413
Рассуждаем в мета-теории с применением исчисления высказываний (оно ведь в ней тоже работает).
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)$.

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 12:13 
Заслуженный участник
Аватара пользователя


28/09/06
10413
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$?

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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 13:12 
Заслуженный участник


27/04/09
28128
epros в сообщении #1318883 писал(а):
Но ведь в нашей теории действует аксиоматика того же исчисления высказываний и ничего более.
Может быть, например, менее. Как минимум, у нас может быть интуиционистская логика. Мы можем формализовать метатеорию и вообще иначе, какой-нибудь теорией типов.

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

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

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

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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 14:38 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 19:30 
Заслуженный участник
Аватара пользователя


28/09/06
10413
arseniiv в сообщении #1318914 писал(а):
Какую семантику вы таким конструкциям приписываете? Формула теории не есть формула метатеории.
Как я сказал, рассуждаем в мета-теории. В данном случае это такая теория, которая может говорить о выводимости чего-то из чего-то, для этого в её языке предусмотрен символ штопора. Но в остальном это обычная теория в классической логике, т.е. тавтологии классического исчисления высказываний для неё закон. И какие-то собственные выводы из чего-то она тоже может делать, как и любая теория. Об исчислении предикатов не говорю, ибо здесь ничего выходящего за пределы исчисления высказываний не используется.

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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 19:40 
Заслуженный участник


31/12/15
922
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)$ -- это другая теория (метатеория) и к выводимости в ней этот штопор не имеет отношения.

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 19:41 
Заслуженный участник


27/04/09
28128
epros в сообщении #1319104 писал(а):
Но в остальном это обычная теория в классической логике, т.е. тавтологии классического исчисления высказываний для неё закон. И какие-то собственные выводы из чего-то она тоже может делать, как и любая теория.
Но как понимать одно и то же $a$ в одном месте в контексте теории и в другом в контексте метатеории? Если нет ничего кроме штопора, надо хотя бы доставить его в нужных местах. (Или может лучше сразу в одну из модальных логик перейдём и будем нормальным $\square$ пользоваться?)

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 19:42 
Заслуженный участник
Аватара пользователя


28/09/06
10413
epros в сообщении #1319104 писал(а):
ибо здесь ничего выходящего за пределы исчисления высказываний не используется

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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 19:45 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 19:50 
Заслуженный участник
Аватара пользователя


28/09/06
10413
george66 в сообщении #1319109 писал(а):
Допустим, у нас есть теория $T$ и штопор означает выводимость в $T$. Та теория, в которой мы можем выписывать формулы вроде $(c\vdash a)\vee(c\vdash b)$ -- это другая теория (метатеория) и к выводимости в ней этот штопор не имеет отношения.
Не понял. Я полагал, что штопор означает выводимость "в логике". А если мы хотим сказать про выводимость в конкретной теории, то должны слева от штопора в явной форме указать дополнительные (к логическим) аксиомы этой теории.

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

 Профиль  
                  
 
 Re: Свойство дизъюнкции - проблема классической логики?
Сообщение11.06.2018, 20:18 
Заслуженный участник


27/04/09
28128
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, но это всё равно не то, что вы делаете сейчас.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 30 ]  На страницу 1, 2  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: dgwuqtj, Vladimir Pliassov


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group