2014 dxdy logo

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

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


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


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

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

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

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

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



Начать новую тему Ответить на тему
 
 Вывод теорем
Сообщение18.02.2016, 11:39 


03/08/15
114
Здравствуйте. Хочу задать небольшой вопрос относительно вывода теорем в заданной формализации логики высказываний.
К примеру, пусть задана следующая формализация:
Аксиома 1 (А1):
$(F\to (G\to F))$
Aксиома 2 (А2):
$(F\to (G\to H))\to ((F\to G)\to (F\to H))$
Ну третью аксиому я приводить не буду, она сейчас не нужна. Используется два знака: Отрицание и Импликация. Правило вывода: Modus Ponens.
Необходимо доказать (вывести) что $F\to F$.
В учебнике приводится такой пример вывода:
В Аксиоме 2 (А2) F и G заменяются на F. a G на $F\to F$. Схема вывода такая:
1.$(F\to ((F\to F)\to F))\to ((F\to (F\to F))\to (F\to F))$ (A2)
2.$F\to ((F\to F)\to F)$ (A1, где G заменена на $F\to F$)
3.$(F\to (F\to F))\to (F\to F)$ (Modus Ponens к п.1 и п.2)
4.$F\to (F\to F)$ (A1, G заменена на F)
5.$F\to F$ (Modus Ponens к 3, 4)
А можно ли сделать так:
Вариант 1.
1.$(F\to (F\to F))\to ((F\to F)\to (F\to F))$ (A2, G и H заменены на F)
2.$F\to (F\to F)$ (A1, где G заменена на F)
3.$(F\to F)\to (F\to F)$ (Modus Ponens к п.1 и п.2)
4.$F\to F$ (A1, где $(G\to F)$ заменено на F)
5.$F\to F$ (Modus Ponens к 3, 4)
Правда вот в пункте 4 аксиома совпадает с теоремой. Незнаю, можно ли так. И вот еще один вариант:
Вариант 2.
1.$F\to (F\to F)$ (A1, где G заменена на F)
2.F (просто формула в данной формализации)
3.$F\to F$ (Modus Ponens к 1, 2)
Вот вообще в рамках данной формализации хотелось бы узнать, может есть какие нибудь алгоритмы которые сразу позволяют сделать нужные замены чтобы получить из теоремы выводы. т.е не подгонять и проверять каждую аксиому , а как бы сразу по какому то правилу подставлять в нужные аксиомы нужные замены чтобы получить вывод)

 Профиль  
                  
 
 Re: Вывод теорем
Сообщение18.02.2016, 11:55 
Заслуженный участник
Аватара пользователя


19/12/10
1546
damir_777 в сообщении #1100337 писал(а):
4.$F\to F$ (A1, где $(G\to F)$ заменено на F)

:shock:
Тогда уж:
1.$F\to F$ (A1, где $(G\to F)$ заменено на $F$) :-)

Так нельзя. Вместо переменной можно подставить любую формулу, но вместо формулы — нет.

-- 18 фев 2016, 11:59 --

damir_777 в сообщении #1100337 писал(а):
2.F (просто формула в данной формализации)

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

 Профиль  
                  
 
 Re: Вывод теорем
Сообщение18.02.2016, 12:04 


03/08/15
114
Аа..ну насчет второго варианта понял. Я просто подумал что раз в аксиомах используется символ "F" и он принят в данной формализации, то значит его можно использовать

 Профиль  
                  
 
 Re: Вывод теорем
Сообщение18.02.2016, 12:15 
Заслуженный участник
Аватара пользователя


19/12/10
1546
Вообще-то, то, что вы называете аксиомами, на самом деле — схемы аксиом. И $F$ это "метасимвол" при замене которого произвольной формулой и получается собственно аксиома. Причём формула уже не должна содерать "метасимволы", а только переменные, которые, обычно, обозначают маленькими буквами, дабы отличать их от "метасимволов".

 Профиль  
                  
 
 Re: Вывод теорем
Сообщение18.02.2016, 12:18 


03/08/15
114
да. да. точно. Забыл совсем, что это схема)
а вот что насчет алгоритмов. Есть ли что нибудь что облегчает вывод теорем?

 Профиль  
                  
 
 Re: Вывод теорем
Сообщение18.02.2016, 12:31 
Заслуженный участник
Аватара пользователя


19/12/10
1546
Правило резолюций вам в помощь. :-)

-- 18 фев 2016, 12:36 --

Или почитайте:
Ч.Чень, Р.Ли Математическая логика и автоматическое доказательство теорем.

 Профиль  
                  
 
 Re: Вывод теорем
Сообщение18.02.2016, 17:06 
Заслуженный участник


27/04/09
28128

(Те, кто знают, знают, а кто не знает, не поймут, но вывод в конце для вторых примечателен.)

Вывести $A\to A$ из этих двух схем можно как угодно. При изоморфизме Карри—Говарда они соответствуют λ-комбинаторам $K, S$, а выводимая — комбинатору $I$, который можно выразить через них как $(SK)(\text{что угодно})$. Только для наших целей этому чему угодно должно быть можно приписать тип $a\to b$, а то выведется формула $\mathcal F\to\mathcal F$, где $\mathcal F$ — формула, не являющаяся переменной; λ-термов с таким типом из $S, K$ можно насобирать сколько угодно — годятся $SXY$, $KZ$ и $K$ для $X\colon a\to t\to u, Y\colon a\to t$, где $a$ — обязательно переменная, $Z$ любого типа. В частности, первое (и последнее) приведённое ТС классическое доказательство соответствует равенству $I = (SK)K$. Можно построить другое доказательство, соответствующее, скажем, $I = (SK)(KK)$ или $I = (SK)((S(KK))K)$, но они (и все остальные) будут длиннее. Пример с первым:

$\begin{array}{rll} 
1.& (A \to (B \to C \to B) \to A) \to (A \to B \to C \to B) \to A \to A & (S) \\ 
2.& A \to (B \to C \to B) \to A & (K) \\ 
3.& (A \to B \to C \to B) \to A \to A & (SK = \mathrm{MP}\, 1, 2) \\ 
4.& (B \to C \to B) \to A \to B \to C \to B & (K) \\ 
5.& B \to C \to B & (K) \\ 
6.& A \to B \to C \to B & (KK = \mathrm{MP}\, 4, 5) \\ 
7.& A \to A & ((SK)(KK) = \mathrm{MP}\, 3, 6) 
\end{array}$

Где-то недавно я писал, что можно взять $(SK)S$, и был неправ по причине, указанной выше. Надеюсь, читавшие простят.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 7 ] 

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



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

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


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

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