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

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

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

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

Кто это?

Кто это?

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

> Кто это?

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

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

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


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

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

((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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

>>((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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

What?

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

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

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

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

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

>>Порвало

Вкуривай.

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

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

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

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

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

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

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

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

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

> Вкуривай.

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

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

Отчего же зря

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

какое-нибудь существенное следствие отсутствия такой изоморфности

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

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

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

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

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

The most immediate way to develop a more complex logical calculus is to introduce rules that are sensitive to more fine-grained details of the sentences being used. When the «atomic sentences» of propositional logic are broken up into terms, variables, predicates, and quantifiers, they yield first-order logic, or first-order predicate logic, which keeps all the rules of propositional logic and adds some new ones. (For example, from «All dogs are mammals» we may infer «If Rover is a dog then Rover is a mammal».) It makes sense to refer to propositional logic as «zeroth-order logic», when comparing it with first-order logic and second-order logic.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

proof-fix

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

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

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

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

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

> Вкуривай.

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

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

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

Для начала надо разобраться с лемой о дедуции (без нее тут делать нечего). Она утверждает, что из 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. Языки и исчисления. (ссылка)