2014 dxdy logo

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

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


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


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

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

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

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

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



Начать новую тему Ответить на тему
 
 Исчисление высказываний. Вывод формулы.
Сообщение08.02.2016, 20:26 


08/02/16
2
Здравствуйте. Давно являюсь читателем форума, а сейчас наконец зарегистрировался, чтобы совета спросить.
Свой диплом получил много лет назад, а сейчас племянница попросила помочь с заданием по математической логике. Разобрался со всеми пунктами, застрял на одном. Понимаю, что решение должно быть тривиальным, но похоже маразм уже подкрадывается. Не прошу полного ответа, просто подскажите начальные шаги, пожалуйста.
Как в исчислении высказываний вывести формулу:
A$\to$(B$\to$(C$\to$(D$\to$A)))

Правка. Заново внес формулу в соответствии с правилами

 Профиль  
                  
 
 Re: Исчисление высказываний. Вывод формулы.
Сообщение08.02.2016, 21:08 
Заслуженный участник


27/04/09
28128
Честно говоря, у исчисления высказываний есть разные аксиоматизации. Несколько распространённых совпадают в наличии двух аксиом$$\begin{array}{ll} \mathsf K. & A\to(B\to A) \\ \mathsf S. & (A\to(B\to C))\to(A\to B)\to(A\to C) \end{array}$$Если в относящейся к задаче аксиоматизации они есть, то можно начинать.

Если воспользоваться изоморфизмом Карри—Говарда, эти аксиомы соответствуют типам двух функций $K, S$ таких, что $Kxy = x$, $Sxyz = xz(yz)$. Надо через них выразить функцию $Xxyzw = x$. Видно, что $Xxyz = Kx$, $Xxy = K(Kx)$, $Xx = K(K(Kx))$, $X = \lambda x.K(K(Kx))$, после чего можно применить правило $\lambda z.AB = S(\lambda z.A)(\lambda z.B)$, выводимое из выражения для $S$, и получить$$X = S(\lambda x.K)(\lambda x.K(Kx)) = S(KK)(S(\lambda x.K)(\lambda x.Kx)) = S(KK)(S(KK)(S(KK)(\lambda x.x))),$$после чего нельзя ничего сделать, если не вспомнить $\lambda x.x = SKK$ (т. к. $SKKx = Kx(Kx) = x$; кстати, отсюда видно, что сгодится и $SK(\text{что угодно})$). Итого $X = S(KK)(S(KK)(S(KK)(SKK)))$, и остаётся применить изоморфизм в обратную сторону, превращая $AB$ в результат применения Modus ponens к $A$ и $B$.

(Выше замаскированно была использована и частично выведена теорема о дедукции.)

 Профиль  
                  
 
 Re: Исчисление высказываний. Вывод формулы.
Сообщение08.02.2016, 21:13 


20/03/14
12041
 i  Korner
Формулы оформляйте по правилам.

Korner
Вот так
Код:
[math]A$\to$(B$\to$(C$\to$(D$\to$A)))[/math]
не надо, надо один доллар в начале формулы, один в конце. И никаких - в середине.

 Профиль  
                  
 
 Re: Исчисление высказываний. Вывод формулы.
Сообщение08.02.2016, 21:15 
Заслуженный участник


27/04/09
28128
А, да, тут использовано соглашение писать $abcd\ldots$ вместо $a(b(c(d\ldots)))$. Т. е. конвертировать назад надо $(S(KK))((S(KK))((S(KK))((SK)K)))$. Очевидно, у вывода будет столько шагов, сколько здесь открывающих скобок, плюс один.

 Профиль  
                  
 
 Re: Исчисление высказываний. Вывод формулы.
Сообщение08.02.2016, 21:30 


08/02/16
2
arseniiv в сообщении #1097973 писал(а):
А, да, тут использовано соглашение писать $abcd\ldots$ вместо $a(b(c(d\ldots)))$. Т. е. конвертировать назад надо $(S(KK))((S(KK))((S(KK))((SK)K)))$. Очевидно, у вывода будет столько шагов, сколько здесь открывающих скобок, плюс один.

Спасибо. Попробую сейчас всё это проделать.

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

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



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

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


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

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