2014 dxdy logo

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

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


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


В этом разделе нельзя создавать новые темы.

Если Вы хотите задать новый вопрос, то не дописывайте его в существующую тему, а создайте новую в корневом разделе "Помогите решить/разобраться (М)".

Если Вы зададите новый вопрос в существующей теме, то в случае нарушения оформления или других правил форума Ваше сообщение и все ответы на него могут быть удалены без предупреждения.

Не ищите на этом форуме халяву, правила запрещают участникам публиковать готовые решения стандартных учебных задач. Автор вопроса обязан привести свои попытки решения и указать конкретные затруднения.

Обязательно просмотрите тему Правила данного раздела, иначе Ваша тема может быть удалена или перемещена в Карантин, а Вы так и не узнаете, почему.



Начать новую тему Ответить на тему На страницу Пред.  1, 2
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение17.04.2015, 22:35 
Аватара пользователя


01/12/06
760
рм
Две строки имеет таблица формулы $A\supset A$. Всё равно меньше.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение17.04.2015, 22:37 
Заслуженный участник


27/04/09
28128
Спорить не стану, потому что так и не разобрался, какая таблица. Свой же вывод я так и не получил, и уже не собираюсь завершать.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение17.04.2015, 22:48 
Заслуженный участник
Аватара пользователя


20/08/14
8506
arseniiv в сообщении #1005083 писал(а):
так и не разобрался, какая таблица

Вероятно, таблица истинности. В обсуждаемой формуле три переменных - $A, B, C$. Таблица истинности задает значения этой формулы для всех возможных наборов значений $A, B, C$, каковых наборов $2^3 = 8$ ($A$ ложно, $B$ ложно, $C$ ложно; $A$ ложно, $B$ ложно, $C$ истинно;...). В формуле $A \subset A$ одна переменная, и в таблице две строки - значения формулы для истинного и ложного $A$.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение17.04.2015, 23:08 
Заслуженный участник


27/04/09
28128
А ведь точно, спасибо.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение18.04.2015, 10:53 
Аватара пользователя


07/01/14
119
arseniiv в сообщении #1005071 писал(а):
Что лень с людьми делает — увяз в попытках доказательства!

Я вообще не понимаю алгоритм подобных доказательств, поэтому и спрашиваю. Мне самому интересно, но никто чётко не может дать ответ.

arseniiv в сообщении #1005071 писал(а):
Между тем, глянул теперь упоминаемое в теме-прародительнице доказательство теоремы о дедукции и вижу, что искомая вами выводимость совершенно не нужна. Просто замените формулу $(\alpha+\beta+1)$ в том месте на формулу, соответствующую аксиоме Клини, и применяйте MP к ней не с формулой $(\alpha+\beta)$, а с формулой $(\alpha)$, а к результату применяйте MP, соответственно, с формулой $(\alpha+\beta)$, а не с формулой $(\alpha)$. Результирующая формула $(\alpha+\beta+3)$ получится та же самая. Доказательство поправлено для нашей аксиомы, всё.

Фантастика! Вроде работает - одним выстрелом двух зайцев! Спасибо!

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение18.04.2015, 20:02 
Заслуженный участник


27/04/09
28128
Не за что! Вот если бы я вчитался в тот ваш пост вовремя! :-)

Kosat в сообщении #1005181 писал(а):
Я вообще не понимаю алгоритм подобных доказательств, поэтому и спрашиваю. Мне самому интересно, но никто чётко не может дать ответ.
Построеня выводов в исчислении высказываний или вообще (включая результаты о выводимости типа теоремы о дедукции)? А что насчёт соображений, приведённых warlock66613? Другие соображения насчёт системы Клини и использования теоремы о дедукции (которая у нас теперь есть) я где-то приводил, но, наверно, действительно в туманной форме. Ещё о том же писал Xaositect, но не помню, насколько полно и где. :?

Построение вывода по шагам и построение вывода из других выводов с помощью теоремы о дедукции, теоремы о $F,\Gamma\vdash G,G,\Gamma\vdash H\Rightarrow F,\Gamma\vdash H$ и прочих «метатеорем» можно поставить в аналогию написанию программы в машинных кодах и её компиляции с какого-нибудь более человекопонятного языка высокого уровня. В обоих вторых случаях для получения конкретного вывода надо знать построения из доказательств теорем и алгоритмы компилятора, для получения же факта выводимости достаточно знать только утверждения теорем или иметь компилятор; обычно интересует только факт выводимости.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение18.04.2015, 20:20 
Аватара пользователя


07/01/14
119
Ага. :D

arseniiv в сообщении #1005354 писал(а):
Построения выводов в исчислении высказываний или вообще (включая результаты о выводимости типа теоремы о дедукции)?

Построение выводов в исчислении высказываний (из аксиом). Что на бумаге, что (затем) в ПК.

arseniiv в сообщении #1005354 писал(а):
А что насчёт соображений, приведённых warlock66613
А что насчёт соображений, приведённых warlock66613? Другие соображения насчёт системы Клини и использования теоремы о дедукции (которая у нас теперь есть) я где-то приводил, но, наверно, действительно в туманной форме. Ещё о том же писал Xaositect, но не помню, насколько полно и где. :?

Я не знаю, как сделать доказательства для каждой строки таблиц истинности, и даже если б знал, не понимаю, как именно "пошагово обрабатывать" наше синтаксическое дерево операций.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение18.04.2015, 21:39 
Заслуженный участник


27/04/09
28128
Хм, пока я особо в них не вглядывался…

Вот возьмём в пример доказательство $\vdash F\equiv\neg A\vee B\to(A\to B)$. Для этого покажем всяческие $[\neg]A,[\neg]B\vdash F$ и покажем, что из всех их это следует.

1‒2. $[\neg]A,B\vdash F$. Теоремой о дедукции получаем $[\neg]A,B,\neg A\vee B,A\vdash B$, что верно, потому что $B\vdash B$.

3. $A,\neg B\vdash F$. Теоремой о дедукции получаем $A,\neg B,\neg A\vee B\vdash B$. Тут так просто не отделаешься. Посмотрим на аксиому (8). С любезной помощью теоремы о дедукции она превращается в выводимость $M\to P,N\to P,M\vee N\vdash P$, так что если мы покажем $\Gamma\vdash M\to P$, $\Gamma\vdash N\to P$, то получим $\Gamma,M\vee N\vdash P$, то есть, через теорему о дедукции, $\Gamma,M\vdash P;\Gamma,N\vdash P\Rightarrow \Gamma,M\vee N\vdash P$. У нас есть способ доказательства с дизъюнкцией в гипотезах! Применим его.

(а) $A,\neg B,\neg A\vdash B$. Тут нам поможет факт $M,\neg M\vdash\text{что угодно}$ [*].

(б) $A,\neg B,B\vdash B$. Это верно уже ясно почему.

Раз (а) и (б), то и с 3 мы разобрались.

4. $\neg A,\neg B\vdash F$. Теоремой о дедукции получаем $\neg A,\neg B,\neg A\vee B, A\vdash B$. Почему это верно, уже разобрано.

Теперь нам надо показать, что 1‒4 вообще имеют какое-то отношение к $\vdash F$. Для этого сначала покажем $\Gamma,M\vdash P;\Gamma,\neg M\vdash P\Rightarrow\Gamma\vdash P$. Это можно показать, имея $\vdash M\vee\neg M$ [**] и ту штуку, которую мы получили в 3 из аксиомы (8).

Теперь ясно, что если мы можем показать $A\vdash P$ и $\neg A\vdash P$, то получим и $\vdash P$. Если $A$ — переменная, только и встречающаяся в $P$, этого достаточно (и, если доказать первые два в какой-то комбинации не получается, мы параллельно можем попытаться доказать $A\vdash\neg P$, $\neg A\vdash\neg P$, чтобы убедиться, что и не получится; но почему это должно быть убедительным, вопрос отдельный). Если же в $P$ встречается две переменные, тогда имеем $A,[\neg]B\vdash P;\neg A,[\neg]B\vdash P\Rightarrow[\neg]B\vdash P$ и, если все четыре вывода у нас есть, в конце мы получим $\vdash P$. Если переменных больше, «собираем» их аналогично до победного конца.

[*] и [**] сейчас доказвать не хочу, так что можете попробовать сами.

-- Сб апр 18, 2015 23:45:29 --

(Оффтоп)

Надеюсь, понятно, зачем я вообще полез за аксиомой (8). Если нет, стоит вообще приглядеться к аксиомам и добиться представления того, «о чём они»; что они не просто тождественно истинные формулы, но и отражают некоторые типы простых логических рассуждений.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение19.04.2015, 12:58 
Аватара пользователя


07/01/14
119
arseniiv в сообщении #1005401 писал(а):
3. $A,\neg B\vdash F$. Теоремой о дедукции получаем $A,\neg B,\neg A\vee B\vdash B$. Тут так просто не отделаешься. Посмотрим на аксиому (8). С любезной помощью теоремы о дедукции она превращается в выводимость $M\to P,N\to P,M\vee N\vdash P$, так что если мы покажем $\Gamma\vdash M\to P$, $\Gamma\vdash N\to P$, то получим $\Gamma,M\vee N\vdash P$, то есть, через теорему о дедукции, $\Gamma,M\vdash P;\Gamma,N\vdash P\Rightarrow \Gamma,M\vee N\vdash P$.

Сплошная теорема о дедукции. На уровне кругов Эйлера это понятно. Правильно ли я понял, что как только мы видим дизъюнкцию в гипотезах, мы запускаєм эту последовательность? Похоже на метод резолюций.

arseniiv в сообщении #1005401 писал(а):
У нас есть способ доказательства с дизъюнкцией в гипотезах! Применим его.

Как это вообще записать?.. У меня против каждой строки должен слоять номер схемы аксиом или modus ponens. Здесь так всё включено одно в другое...

Извините за глупые вопросы.

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение19.04.2015, 20:41 
Заслуженный участник


27/04/09
28128
Kosat в сообщении #1005542 писал(а):
Правильно ли я понял, что как только мы видим дизъюнкцию в гипотезах, мы запускаєм эту последовательность?
Видимо, да. Особо не задумывался и подводных камней не нашёл.

Kosat в сообщении #1005542 писал(а):
Похоже на метод резолюций.
И не только! Упомянутые мной ни к селу ни к городу выше analytic tableaux тоже чем-то похожи. Правда, там ещё эквивалентности применяются для избавления от $\to,\leftrightarrow$ и протаскивания отрицаний к переменным. Этот метод основан чисто на значениях формул — без вывода из аксиом и MP, потому тут я его описывать не буду. :-)

Kosat в сообщении #1005542 писал(а):
Как это вообще записать?.. У меня против каждой строки должен слоять номер схемы аксиом или modus ponens. Здесь так всё включено одно в другое...
Да, как я и говорил, тут мы получаем не вывод, а «программу построения вывода». Сам вывод получится, если смотреть, что там теорема о дедукции, применённая к конкретным выводам, даёт, начиная с упомянутых очевидных выводов в три/одну строку.

Kosat в сообщении #1005542 писал(а):
Извините за глупые вопросы.
Уверяю, вполне нормальные вопросы. Скорее, у меня нет нормальных (точных) ответов — я особо автоматическим построением вывода в исчислении высказываний/исчислении предикатов не интересовался. (Надеюсь, от текущих какая-то польза есть?)

 Профиль  
                  
 
 Re: Как из схем аксиом Клини вывести схему аксиом Гильберта №2?
Сообщение20.04.2015, 08:20 
Аватара пользователя


07/01/14
119
arseniiv в сообщении #1005682 писал(а):
Уверяю, вполне нормальные вопросы. Скорее, у меня нет нормальных (точных) ответов — я особо автоматическим построением вывода в исчислении высказываний/исчислении предикатов не интересовался. (Надеюсь, от текущих какая-то польза есть?)

Есть (хотя повсеместная замена импликации через теорему о дедукции (?) и применение к дизъюнктам недо-метода резолюций (??) и вызывают у меня определённые сомнения). Но учитывая то, что мне нужно решить любые три из первых четырёх задач, я наверно решу четвёртую, а не третью (с самого начала склонялся к этому же).

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

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



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

Сейчас этот форум просматривают: нет зарегистрированных пользователей


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

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