[специалистам по всему] Матлогика

Пальчунов? :)

stevejobs (14.07.2010 10:34:16)

Маловероятно.

Кто это?

balodja (14.07.2010 10:41:48)

Если ты этого не знаешь, то тебе лучше это не знать.

> Кто это?

если расскажу, мне придется тебя убить.

http://koi.nsu.ru/teachers/palchunov.php

нет, мне определенно придется тебя убить.


(кстати, напиши ему на palch@math.nsc.ru этот пост, и если в ответе будет ржака - сообщи о результатах ))

stevejobs (14.07.2010 10:48:17)

Джобс, ну ты рискуешь. Палец тебя покарает...

((p -> q) -> p) -> p => ((not(p) || q) -> p) -> p => ((p && not(q)) || p) -> p => not((p && not(q)) || p) || p => (not(p && not(q)) && not(p)) || p => ((not(p) || q) && not(p)) || p => (not(p) || q || p) && (not(p) || p) => (true || q) && true => true && true => true

kim-roader (14.07.2010 11:04:03)

Гы, вот все фитовцы и спалились :)

gizzka (14.07.2010 11:05:26)

> Палец тебя покарает...

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

stevejobs (14.07.2010 11:11:23)

А у нашего потока не вёл Пальчунов... Хотя может это только пока.

Yareg (14.07.2010 11:13:15)

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

Если уж так хочется уровней, то что мешает у каждой из 16-ти функций приписывать индекс принадлежности к тому или иному слою?

Зачем было велоcипедить свою аксиоматику? Что есть в исчислении высказываний такого, чего не было бы в логике первого порядка (по форме)?

mclaudt (14.07.2010 11:13:24)

> Зачем было велоcипедить свою аксиоматику?

потому что это увлекательно и расширяет сознание? :)

stevejobs (14.07.2010 11:20:50)

Пожалуй я ещё спалюсь.

Kosyak (14.07.2010 12:09:40)

Математики же!

Kosyak (14.07.2010 12:12:04)

Я лучше скастую jtootf.

mclaudt (14.07.2010 12:38:46)

кстати, а чем тебе не понравился форк/копипаста как метод развития? Начинается новый проект, старые вещи обозначаются новыми именами, старый хлам отправлятся в мусорку, дописываются новые модули. Brave new world. Потом форк/копипаста повторяется под новым именем, и так до просветления.

stevejobs (14.07.2010 12:47:29)

В данном случае, насколько я понимаю, это и не форк, а переименование переменных в исходниках.

mclaudt (14.07.2010 12:58:20)

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

mclaudt (14.07.2010 13:07:02)

>>((p -> q) -> p) -> p => ((not(p) || q) -> p) -> p => ((p && not(q)) || p) -> p => not((p && not(q)) || p) || p => (not(p && not(q)) && not(p)) || p => ((not(p) || q) && not(p)) || p => (not(p) || q || p) && (not(p) || p) => (true || q) && true => true && true => true

s/"=>"/"<=>"/g

mclaudt (14.07.2010 15:57:11)

Такие же рассуждения и для логики первого порядка. Только вот вся литература по ней не пестрит отсылками к Аристотелям, модусами поненсами и прочей гумносятиной, в отличие от.

mclaudt (14.07.2010 16:01:47)

> Только вот вся литература по ней не пестрит отсылками к Аристотелям

чем тебе философы-то теперь не угодили?

stevejobs (14.07.2010 16:18:03)

Гм. Замена импликации дизьюнкцией (три раза), правило де моргана (4 раза), дистрибутивность.

P.S. Модус поненс это не гуманитарщина, а удобное правило вывода. Хотя правило резолюции всяко удобней использовать.

P.P.S. Надо было проще писать

((p -> q) -> p) -> p <=> [замена импликации на дизьюнкцию] <=> ((not(p) || q) -> p) -> p <=> [то же самое + де Морган] <=> ((p && not(q)) || p) -> p <=> [закон поглощения] <=> p -> p <=> [тривиально] <=> true

kim-roader (14.07.2010 16:20:42)

При изучении логики высказываний такие теоремы обычно доказываются при помощи таблиц истиности.

p|q|p->q|(p->q)->p|((p->q)->p)->p|
0|0| 1  |    0    |       1      |
0|1| 1  |    0    |       1      |
1|0| 0  |    1    |       1      |
1|1| 1  |    1    |       1      |

В итоге результат истинен для всех p и q.

kim-roader (14.07.2010 16:34:36)

>>P.S. Модус поненс это не гуманитарщина, а удобное правило вывода.

Правило вывода такого вида есть и в формальной логике. То что поненсом его стали величать сотни лет назад применительно к высказываниям, сейчас не играет никакой принципиальной роли.

Назови хотя бы один вывод, которому не было бы полного аналога в обычной логике.

mclaudt (14.07.2010 16:36:35)

> Зачем спрашивается надо было брать за основу обычные логичиеские функции, переобозначить их и раздувать "новый" раздел математики?

Чтобы потом добавить кванторы?

Manhunt (14.07.2010 16:36:48)

>>При изучении логики высказываний такие теоремы обычно доказываются при помощи таблиц истиности

В чем ты видишь особенность именно для логики высказываний? Точно такие же таблицы есть и в логике предикатов.

Я более чем уверен, что с теоретико-категорийной точки зрения эти две теории эквивалентны/гомоморфны/изоморфны полностью.

mclaudt (14.07.2010 16:38:39)

>>Чтобы потом добавить кванторы?

What?

А что есть кванторы кроме сокращенной записи большого числа конъюнкций/дизъюнкций? И почему ты говоришь так будто кванторов нет в логике первого порядка??

mclaudt (14.07.2010 16:55:01)

зря, на самом деле. логика первого порядка - расширение логики высказываний, более сложное исчисление; и нет, они не изоморфны

jtootf (14.07.2010 16:57:24)

> А что есть кванторы кроме сокращенной записи большого числа конъюнкций/дизъюнкций?

Порвало. ∀x ∃y (x + y = 0). Запиши это же, но без кванторов, при помощи "большого числа конъюнкций/дизъюнкций"?

Manhunt (14.07.2010 16:58:40)

>>Порвало

Вкуривай.

http://www.linux.org.ru/jump-message.jsp?msgid=4809592&cid=4810010

А потом швы наложим.

mclaudt (14.07.2010 17:07:36)

>>логика первого порядка - расширение логики высказываний

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

mclaudt (14.07.2010 17:14:08)

>>∀x ∃y (x + y = 0). Запиши это же, но без кванторов, при помощи "большого числа конъюнкций/дизъюнкций"

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

mclaudt (14.07.2010 17:17:57)

>>зря, на самом деле

Отчего же зря ;) Попросим заодно привести в пример какое-нибудь существенное следствие отсутствия такой изоморфности.

mclaudt (14.07.2010 17:20:28)

> Вкуривай.

> x1, x2, ... пробегает все множество чисел

Ох. У тебя формулы не-конечной длины там? Я бы предпочел их закопать, и никогда-никогда не откапывать.

Manhunt (14.07.2010 17:24:08)

тема мне не особо интересна, а соответственно сказать я могу мало что

http://en.wikipedia.org/wiki/First-order_logic#Introduction

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

в частности, предикаты и кванторы - это не к ИВ, там их как раз нет

jtootf (14.07.2010 17:31:59)

>>Я бы предпочел их закопать, и никогда-никогда не откапывать.

Эту функцию и выполняют кванторы. Поздравляю, с открытием, капитан Христофор.

mclaudt (14.07.2010 17:32:10)

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

Деление на логику первого порядка и логику высказываний согласно такому определению - это не более чем расстановка скобок.

Только расстановка скобок гибче, ибо уровней там дохрена, а не два, как при этом надуманном делении.

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

mclaudt (14.07.2010 17:41:30)

>>это не к ИВ, там их как раз нет

Есть операции И и ИЛИ, будут и кванторы.

mclaudt (14.07.2010 17:43:23)

можно привести список функция-аналог?

jtootf (14.07.2010 17:46:03)

>>можно привести список функция-аналог?

Конъюнкция, дизъюнкция и отрицание есть и там и там, а они, как известно, образуют полный базис.

mclaudt (14.07.2010 17:49:36)

Так что список строится: для этих базисных функций - тривиально, а для остальных - через их выражения через эти три базисные.

mclaudt (14.07.2010 17:51:27)

меня больше интересовало то, что именно у тебя будет со стороны логики первого порядка; меня не покидает ощущение, что ты где-то в процессе спора перепутал местами исчисления

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

jtootf (14.07.2010 17:56:17)

>>ИВ - очень простое, без кванторов и предикатов; в логике первого порядка кванторы и предикаты вводятся - и удобство от их использования, в общем-то, очевидно. где предмет спора?

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

>>что именно у тебя будет со стороны логики первого порядка

на стороне логики первого порядка - все 16 логических функций двух переменных, а со стороны ИВ - соответствующие им композиции высказываний.

Правила вывода для таких композиций будут подчиняться законам, которые эквивалентны законам логики первого порядка.

mclaudt (14.07.2010 18:06:31)

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

¬("Нет ни одной задачи, решаемой через логику высказываний которая не описывалась бы логикой первого порядка"∧¬"ИВ не нужно")=1

proof-fix

mclaudt (14.07.2010 18:09:42)

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

jtootf (14.07.2010 18:12:46)

Черт, круто вышло. Cыплю бисер изысканнейший. Жаль только его затопчут под толсксовым хламом.

mclaudt (14.07.2010 18:15:25)

> выражения вида P(y1)∧P(y2)∧... принято сокращать квантором общности ∀, а выражения вида P(y1)∨P(y2)∨... принято сокращать квантором существования ∃

Как только ты напишешь бесконечную дизъюнкцию без кванторов, то это сообщение перестанет считаться бредом.

kim-roader (14.07.2010 19:03:00)

> Вкуривай.

> http://www.linux.org.ru/jump-message.jsp?msgid=4809592&cid=4810010

> А потом швы наложим.

Вот такие люди и считают, что в лямбда исчислении есть константы.

kim-roader (14.07.2010 19:04:34)

Для начала надо разобраться с лемой о дедуции (без нее тут делать нечего). Она утверждает, что из G и A выводится B тогда и только тогда, когда из G выводится (A->B). G - произвольное множество формул, A, B - произвольные формулы.

Таким образом доказать нужно, что из (p->q)->p выводится p.

Доказывать нужно отдельно для 2 гипотез (q и not q). После этого используя A11 и A8 можно оформить искомый вывод.

То, что из q, (p->q)->p выводится p очевидно. Достаточно добавить q->(p->q) (первая аксиома) и применить лемму о дедукции.

То, что из not q, (p->q)->p выводится p тоже очевидно, так как из not q выводится (p->q) (аксиома A9)

По теме настоятельно рекомендуется к прочтению

Н. К. Верещагин, А. Шень. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. (ссылка)

ival (14.07.2010 19:05:43)