Лингвофорум

Начался семестр, приступил к изучению учебников логики.

Ниче не понятно на самом деле. Какая-то страшная философия, какой глубины даже у нас гуманитариев не наблюдалось ваще. Притом, что курс логики я таки проходил когда-то, хотя и достаточно примитивный, для лингвистов.

Вопрос: что примерно значит конструктивная индукция? Что такое неконструктивная индукция?

Цитата: RawonaMкурс логики я таки проходил когда-то

Ты его тут вроде бы даже вёл...

Цитата: Bhudh от марта 10, 2011, 23:58

Цитироватькурс логики я таки проходил когда-то

Ты его тут вроде бы даже вёл...

Ну начинал. Может вскоре продолжу :)

Так я не понял, никто тут не знает логику? :(

А на других языках неужели ничего не нагуглилось?

Да в общем-то не нагуглилось, но вот вы меня подтолкнули погуглить еще и теперь я понял, что просто неправильно понял термин. Не конструктивная, а структурная индукция дэс. А это уже гуглится неплохо :)

Сохраню тут ссылку на список терминов, чтоб не вляпываться снова.
http://www.cs.huji.ac.il/~udiboker/logic/english_hebrew_lexicon.html

Цитировать(wiki/ru) Структурная_индукция (http://ru.wikipedia.org/wiki/%D0%A1%D1%82%D1%80%D1%83%D0%BA%D1%82%D1%83%D1%80%D0%BD%D0%B0%D1%8F_%D0%B8%D0%BD%D0%B4%D1%83%D0%BA%D1%86%D0%B8%D1%8F)

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

Является ли записью этого предожения: Для любого числа между 0 и 1, которое не 0 и не 1, его квадрат меньше него.
?

Цитата: RawonaM от марта 13, 2011, 22:56
Является ли записью этого предожения: Для любого числа между 0 и 1, которое не 0 и не 1, его квадрат меньше него.
?

Это даже нельзя назвать правильно составленной формулой.
Должно быть что-то вроде

Цитата: Gerbarius от марта 13, 2011, 23:37

ЦитироватьЯвляется ли записью этого предожения: Для любого числа между 0 и 1, которое не 0 и не 1, его квадрат меньше него.
?

Это даже нельзя назвать правильно составленной формулой.

Сорри, пропустил х. Надо так:

Что тут неправильно составлено?

Цитата: Gerbarius от марта 13, 2011, 23:37

А зачем вы закрутили? Ведь проще можно:
Да и скобок у вас как-то не хватает...

Цитата: RawonaM от марта 13, 2011, 23:41
А зачем вы закрутили? Ведь проще можно:
Да и скобок у вас как-то не хватает...

Можно, конечно. Но ведь и вы и в своём первоначальном варианте закрутили будь здоров.  :yes: Насчёт скобок. Все скобки обычно никогда и не пишут. Для восстановления недостающих скобок пользуются некоторыми соглашениями, подобными тем, которые используются при записи обычных арифметических формул. Но, конечно, вы всегда можете выписывать все скобки явно.

Цитата: RawonaM от марта 13, 2011, 23:41
Сорри, пропустил х. Надо так:

Что тут неправильно составлено?

Тут записано другое высказывание, причём ложное. Ложность можно показать так. Возьмём . При таком высказывание будет очевидно ложным, но импликация будет истинной, так как ложна её посылка. Импликация будет тем самым ложной, так как её посылка истинна, а заключение ложно.
В общем, означает вовсе не то, что лежит на отрезке и при том не равно ни 0, ни 1 (для этого следовало использовать конъюнкцию), а то, что или не лежит на отрезке , или оно не равно ни 0, ни 1, или и то и другое вместе.

Цитата: Gerbarius от марта 14, 2011, 00:47
Но ведь и вы и в своём первоначальном варианте закрутили будь здоров.  :yes:

Это не мой вариант, это задание из книги :)

Цитата: Gerbarius от марта 14, 2011, 00:47
Насчёт скобок. Все скобки обычно никогда и не пишут. Для восстановления недостающих скобок пользуются некоторыми соглашениями, подобными тем, которые используются при записи обычных арифметических формул. Но, конечно, вы всегда можете выписывать все скобки явно.

А какие общепринятые приоритеты? Импликация первее?

Цитата: Gerbarius от марта 14, 2011, 00:47
Тут записано другое высказывание, причём ложное. Ложность можно показать так. Возьмём . При таком высказывание будет очевидно ложным, но импликация будет истинной, так как ложна её посылка. Импликация будет тем самым ложной, так как её посылка истинна, а заключение ложно.

Действительно. Спасибо, а то мой парсер запутался :)

Цитата: RawonaM от марта 14, 2011, 08:30
А какие общепринятые приоритеты? Импликация первее?

Попробую объяснить. В следующих примерах под можно понимать любые формулы, заключёные в скобки.
Кванторы и отрицание считаются младше остальных логических связок. То есть, например, означает , а не .
Аналогично, означает , а не .
Дальше идут конъюнкция и дизъюнкция. Потом уже идёт импликация. То есть означает , а не .
У конъюнкции и дизъюнкции обычно также разные приоритеты, но как раз здесь общепринятых соглашений нет. Поэтому в группах, где встречаются и конъюнкции и дизъюнкции скобки как правило ставят. Например, не пишут , а пишут или или .
В группах из нескольких конъюнкций или дизъюнкций скобки обычно не пишут, так как эти операции ассоциативны. То есть, например, вместо или обычно пишут просто .
В группах из нескольких импликаций скобки как правило ставят. То есть явно пишут или , а не .  Последняя запись, кстати, обычно понимается как , но я не уверен, что все без исключения придерживаются именно такого соглашения. Так как импликация неассоциативна, то скобки в таких случаях лучше ставить во избежание возможных недоразумений.

Спасибо. :)
Плохо это, диалекты в логике. Надо чтобы 100% однозначно было, иначе будет лингвистика. :(

Цитата: RawonaM от марта 14, 2011, 12:03
Плохо это, диалекты в логике. Надо чтобы 100% однозначно было, иначе будет лингвистика.

Это диалекты не логики, а записи. В самой логике везде подразумеваются скобки, и всё однозначно.
Что касается приоритета конъюнкции и дизъюнкции, то обычно у конъюнкции он больше.
Конъюнкцию кроме "∧ " ещё обозначают как "∙" (умножение), а дизъюнкцию кроме "∨" — как "+" (сложение). И приоритеты у них соответствуют: A∨B∧C = A+B∙C = A+(B∙C) = A∨(B∧C).

Застрял на одном вопросе.

Допустим B — выражение логики пропозиций, записаное в польской нотации.

Заменим каждую атомную пропозицию на -1, бинарный оператор на +1, а оператор отрицания на 0.

Нужно доказать, что B правильная формула iff после замены сумма получается -1 и сумма любых начальных компонентов неотрицательная.

Понятно вообще? Кому-нибудь по зубам? :)

В одну сторону я могу доказать, это если дана формула и нужно доказать, что эти условия соблюдаются. Делается структурной индукцией.
Вторую сторону нам подсказали, что нужно делать индукцией на длину строки. Так как я с такой индукцией не знаком, даже не представляю, что можно тут поделать.

Индукция по длине строки - это ж обычная математическая (или натуральная) индукция.
Под строкой здесь можно понимать последовательность чисел, получающуюся после замены каждой компоненты формулы на число.
Здесь индукцию можно применить в следующей форме.
1) Доказываем, что свойство верно для строки длины 1.
Так как единственная строка длины 1, которая удовлетворяет заданному условию, состоит из -1, то она соответствует выражению, состоящему из единственного атома, то есть правильной формуле.
2) Допустим, что свойство верно для всех строк длины , где . Покажем, что оно верно и для строк длины . Рассмотрим какую-нибудь строку длины , которая удовлетворяет условию. Здесь возможны три случая в зависимости от числа, которое стоит на первом месте.
а) На первом месте стоит -1. Строка не удовлетворяет условию, что сумма любых начальных элементов неотрицательна. Таким образом этот случай невозможен.
б) На первом месте стоит 0. Тогда, как можно заметить, остаток строки удовлетворяет заданному условию. А значит по индуктивному предположению он соответствует некоторой правильной формуле . Тогда вся строка соответствует выражению , то есть также правильной формуле.
в) На первом месте стоит +1. Будем считать суммы начальных отрезков. Как можно заметить из того, что сумма всех элементов равна -1, и из того, что начальный элемент равен +1, одна из "промежуточных сумм" должна быть равна 0. То есть всю строку можно представить в виде , где . Далее можно заметить, что обе подстроки и удовлетворяют заданному условию, а значит, по индуктивному предположению соответствуют некоторым правильным формулам и . соответствует некоторой бинарной связке . Таким образом вся строка соответствует выражению вида , то есть также правильной формуле.
Это завершает доказательство.

P.S.
По-русски всё-таки обычно говорят о логике или исчислении высказываний . Вместо атомных пропозиций лучше говорить атомарное высказывание или просто атом.

Спасибо, Gerbarius! Я тут уже начал кое что строить, ваша помощь очень существенна. Сейчас попробую вникнуть.

Цитата: Gerbarius от марта 20, 2011, 16:00
По-русски всё-таки обычно говорят о логике или исчислении высказываний . Вместо атомных пропозиций лучше говорить атомарное высказывание или просто атом.

Спасибо, буду знать :)

Да... Жениаль. Я бы до завтра до этого вряд ли дошел скорее всего. Благодарю!

Все-таки рекурсия интересная штука.

Пытаюсь разобраться в дебрях логических символов...

В чем разница между и ?

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

Эти утверждения не эквивалентны?

Нашел объяснение тут:

(wiki/en) Entailment#Syntactic_consequence (http://en.wikipedia.org/wiki/Entailment#Syntactic_consequence)

ЦитироватьSyntactic consequence

A formula A is a syntactic consequence[3][4][5][6] within some formal system FS of a set Г of formulas if there is a formal proof in FS of A from the set Г.

   

Syntactic consequence does not depend on any interpretation of the formal system.[7]

Semantic consequence

A formula A is a semantic consequence of a set of statements Г

   

if and only if no interpretation makes all members of Г true and A false.[8] Or, in other words, the set of the interpretations that make all members of Г true is a subset of the set of the interpretations that make A true.

Но разница не очень ясна. При наличии всех возможных интерпретаций эти следования эквивалентны?

(wiki/en) Propositional_logic#Soundness_and_completeness_of_the_rules (http://en.wikipedia.org/wiki/Propositional_logic#Soundness_and_completeness_of_the_rules)

ЦитироватьSoundness
    If the set of wffs S syntactically entails wff , then S semantically entails
Completeness
    If the set of wffs S semantically entails wff , then S syntactically entails

Получается, что система sound and complete (как это по-русски) iff


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

Хм...

Например:

Верно или нет?

Ведь синтаксически следует же!

Но никак не:

Ибо нет и одной такой модели.

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

Цитата: RawonaM от апреля  2, 2011, 12:41
Таким образом нет разницы между и в обычной логике высказываний. Правильно?

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

P.S.
На практике, конечно, формальная система и её интерпретация обычно связаны. То есть либо формальная система выбирается из тех соображений, чтобы по крайней мере все выводимые в ней утверждения были истинны в некоторой заранее данной интерпретации (в этом случае из следует ), а если возможно, то кроме того, чтобы в ней были выводимы все истинные в интерпретации утверждения (в этом случае и из следует ); либо уже заданная формальная система интерпретируется так, чтобы между выводимостью и интерпретацией была некоторая связь. Но в любом случае никакой эквивалетности между и даже в практически интересных случаях может и не быть.

Цитата: RawonaM от апреля  2, 2011, 13:17
Хм...

Например:

Верно или нет?

Ведь синтаксически следует же!

Это так.

Цитата: RawonaM от апреля  2, 2011, 13:17
Но никак не:

Ибо нет и одной такой модели.

А вот здесь вы не правы, поскольку формула принимает значение истина при всех значениях p, когда принимает значение истина, тривиальным образом, так как формула тождественно ложна.

Спасибо, Gerbarius! Начинает потихоньку укладываться :)

Цитата: RawonaM от марта 10, 2011, 21:43
Начался семестр, приступил к изучению учебников логики.

Ниче не понятно на самом деле. Какая-то страшная философия, какой глубины даже у нас гуманитариев не наблюдалось ваще.

:D Вы это серьйозно?

Цитата: Sirko от апреля  2, 2011, 18:29
:D Вы это серьйозно?

Честное пионерское.

Если для любого b верно и для любого a верно , и выполнима, то выполнима?

Что значит ?

Что-то типа или что-то более конкретное?

Цитата: RawonaM от апреля  3, 2011, 00:27
Что значит ?

Что-то типа или что-то более конкретное?

Ну да, так и есть.

Цитата: RawonaM от апреля  3, 2011, 00:18
Если для любого b верно и для любого a верно , и выполнима, то выполнима?

Этого условия я, честно говоря,  не понял. Если действительно имеется ввиду, что как из , так и из следует, что угодно, то совершенно непонятно, откуда берутся и , из которых составлена формула , и какое они вообще имеют  отношение к делу.
Если же имеется ввиду, что
если для любых и при условии и следует выполнимость формулы , то формулы множества совместно выполнимы,
то это будет верно, как нетрудно показать. Допустим в входят формулы , а в входят . Тогда и . Тогда по условию будет выполнима формула . А из выполнимости конъюнкции формул следует совместная выполнимость всех её членов.

Цитата: Gerbarius от апреля  3, 2011, 01:54
Этого условия я, честно говоря,  не понял.

Да, я там напортачил((

Цитата: Gerbarius от апреля  3, 2011, 01:54
если для любых и при условии и следует выполнимость формулы , то формулы множества совместно выполнимы,

Именно это имелось в виду.
Благодарю! :)

Как по-русски/английски называются множества, в которых для любых верно либо либо ?
У нас это названо что-то типа «линейное множество».
Пытаюсь найти свойства и примеры, сам затрудняюсь придумать хоть одно.

Цитата: RawonaM от апреля  3, 2011, 10:30
Как по-русски/английски называются множества, в которых для любых верно либо либо ?
У нас это названо что-то типа «линейное множество».
Пытаюсь найти свойства и примеры, сам затрудняюсь придумать хоть одно.

По-английски такие множества можно называть linerly preorder set или linearly quasiordered set, по-русски аналогично линейно предупорядоченное множество или линейно квазиупорядоченное множество.
Но я, правда, не очень понимаю, где они могут понадобиться в логике.

Цитата: Gerbarius от апреля  3, 2011, 14:25
Но я, правда, не очень понимаю, где они могут понадобиться в логике.

Вот у меня такое задание: найти такое линейно квазиупорядоченное бесконечное множество , в котором для любого есть , так что .

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

Цитата: RawonaM от апреля  3, 2011, 14:38
Вы можете порекомендовать какие-нибудь книги на эту тему (исчисления высказываний то есть и математическая логика вообще)? У меня недостаточно материалов, все выходные промучился в поисках в интеренете непонятно чего. Нашел кое что, но нельзя сказать, что этим можно ограничиться.

:what: А вам преподаватели никаких книг не посоветовали разве?

Цитата: RawonaM от апреля  3, 2011, 14:38

Цитата: Gerbarius от апреля  3, 2011, 14:25
Но я, правда, не очень понимаю, где они могут понадобиться в логике.

Вот у меня такое задание: найти такое линейно квазиупорядоченное бесконечное множество , в котором для любого есть , так что .

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

Цитата: Gerbarius от апреля  3, 2011, 16:18
Тут можно взять множество формул . С одной стороны для любых двух формул и выполняется либо , если , либо в противном случае. А с другой стороны для любой верно , если .

Ага, точно. Спасибо :)

Цитата: Gerbarius от апреля  3, 2011, 16:18
:what: А вам преподаватели никаких книг не посоветовали разве?

Да есть парочку, но какое-то все оно не очень.

Скажите, множество выполнимо если и только если оно непротиворечиво, правильно?

Цитата: RawonaM от апреля  3, 2011, 20:23
Скажите, множество выполнимо если и только если оно непротиворечиво, правильно?

Угу, но это нетривиальный результат (в одну из сторон).

Цитата: RawonaM от апреля  3, 2011, 20:23
Да есть парочку, но какое-то все оно не очень.

Кстати, на вашем сайте со списком англо-ивритских терминов я обнаружил и список литературы. Я так понимаю, основной учебник по курсу - это Enderton, "A mathematical introduction to logic"? Чем эта книга вам не понравилась? Я её щас мельком глянул, и у меня сложилось впечатление, что все ваши задания заточены именно под неё. А изложение там не слишком традиционное, то есть другие книги именно под ваш курс не очень подойдут скорее всего.

Цитата: Gerbarius от апреля  3, 2011, 21:22
Я так понимаю, основной учебник по курсу - это Enderton, "A mathematical introduction to logic"?

Нет, я такого и даже не знаю. А где вы его скачали? Или в гуглбуксе полистали?
Мне кажется этот учебник используется для более продвинутого курса логики, который для математиков.

Цитата: Gerbarius от апреля  3, 2011, 21:22
Я её щас мельком глянул, и у меня сложилось впечатление, что все ваши задания заточены именно под неё.

Было бы неплохо, надо мне найти эту книгу.
У нас учебник доморощенный в этом университете, как большинство учебников наших курсов. Это курс логики для информатиков, он преподается только третий семестр, в нем куча недочетов и вообще координатор курса какая-то очень не внушающая доверия персона, хотя и весьма приятна как человек.
Удивляет, что практически весь материал приходится добывать из внешних источников и задания вообще ни разу не соответствуют тому, чему они должны. Написано что это задание по третьей главе книги, вдруг оказывается, что в ней используются определения данные в четвертой и пятой главе и т.п.
Вот эту книгу нам рекомендовали как внеклассное чтение: http://estudy.openu.ac.il/opus/static/binaries/editor/bank60\ספר במדעי המחשב_0.pdf (http://estudy.openu.ac.il/opus/static/binaries/editor/bank60%5c%d7%a1%d7%a4%d7%a8%20%d7%91%d7%9e%d7%93%d7%a2%d7%99%20%d7%94%d7%9e%d7%97%d7%a9%d7%91_0.pdf)

Ну и еще вот эта:
Mathematical Logic for Computer Science (http://books.google.co.uk/books?id=hzWlEy1qqR8C&dq=logic+for+computer+science+textbooks&printsec=frontcover&source=in&hl=en&ei=JjhgS7HeKtuN_AbwzeCKDA&sa=X&oi=book_result&ct=result&resnum=11&ved=0CDgQ6AEwCg#v=onepage&q=logic%20for%20computer%20science%20textbooks&f=false)

Но эту похоже только за то, что это диссертация одного израильского ученого. Хотя может и стоящее, не знаю.

Цитата: Gerbarius от апреля  3, 2011, 21:22
Кстати, на вашем сайте со списком англо-ивритских терминов я обнаружил и список литературы.

Что-то я не нахожу.

Список литературы я нашёл здесь http://www.cs.huji.ac.il/~udiboker/logic/
Ну я и подумал, что это и есть рекомендуемая литература.  :what:
Учебник Эндертона (и не только) можно взять здесь
http://lib.homelinux.org/_djvu/_catalog/index_192.html
Логин и пароль зашифрованы в кракозябрах.

Не дает зайти :(

А я вчера зашёл... :what:

И сейчас заходится?

А-а, латиницей надо. А я кириллицей пытался зайти.

;D Недоспал?
А списочек, конечно, мощщный!

Да это же целый клад!

За оста[b]́[/b]льну жизнь перечитаешь?

Цитата: Bhudh от апреля  4, 2011, 12:05
За оста́льну жизнь перечитаешь?

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

Цитата: Gerbarius от апреля  3, 2011, 01:54
если для любых и при условии и следует выполнимость формулы , то формулы множества совместно выполнимы

А в обратную сторону это же тоже верно, правильно? Вроде как тривиально.

Вот такой еще вопрос:
эквивалентны ли два утверждения
1) тавтология
2) для любых верно следующее:

Мне кажется что да, но я не уверен почему-то. Вроде как доказал :)

Должно быть , вроде бы. Из этого ваше докажется двумя подстановками вместо сигмы.

Цитата: arseniiv от апреля  4, 2011, 19:55
Из этого ваше докажется двумя подстановками вместо сигмы.

Не понял.

Вот еще интересная штука:
По индукции определено множество I высказываний, в которых есть только импликация и атом p.
Нужно доказать, что I линейно предупорядоченное.

Я думаю, что тут для начала нужно по структурной индукции показать, что может быть F только в той модели, где p=F.
Ибо каждое высказывание в форме в итоге сводится к p и b может быть F только если p=F. В общем, рекурсия. Как это правильно сформулировать, не знаю.

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

Цитата: RawonaM от апреля  4, 2011, 19:19

Цитата: Gerbarius от апреля  3, 2011, 01:54
если для любых и при условии и следует выполнимость формулы , то формулы множества совместно выполнимы

А в обратную сторону это же тоже верно, правильно? Вроде как тривиально.

Да, верно. Если и , то чтобы выполнить формулу , достаточно тем атомам из неё, которые встречаются в формулах из приписать те значения, которые выполняют , а остальным атомам можно приписать произвольные значения.

Цитата: RawonaM от апреля  4, 2011, 19:19
Вот такой еще вопрос:
эквивалентны ли два утверждения
1) тавтология
2) для любых верно следующее:

Мне кажется что да, но я не уверен почему-то. Вроде как доказал :)

Да. А если доказали, то откуда неуверенность?  :)
На самом деле здесь условие можно заменить на , так как выполняется всегда.

Цитата: Gerbarius от апреля  4, 2011, 20:29
Да. А если доказали, то откуда неуверенность?  :)

Из-за другой логики, точнее из теории вероятности :) Есть задание «доказать или опровернгуть», в нем два пункта. Если оба пункта нужно доказывать или оба пункта нужно опровергать, то всегда есть подозрение, что закралась ошибка. Ну что же, выходит, что в этот раз оба пункта были верны :)

Цитата: RawonaM от апреля  4, 2011, 20:14
Вот еще интересная штука:
По индукции определено множество I высказываний, в которых есть только импликация и атом p.
Нужно доказать, что I линейно предупорядоченное.

Я думаю, что тут для начала нужно по структурной индукции показать, что может быть F только в той модели, где p=F.
Ибо каждое высказывание в форме в итоге сводится к p и b может быть F только если p=F. В общем, рекурсия. Как это правильно сформулировать, не знаю.

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

Здесь потенциально возможны четыре распределения истинностных значений для каждой формулы. И если бы нашлись две формулы, одна из которых принимает значение T при p=T и F при p=F, а другая в точности противоположные значения, то ни одна из них не следовала бы из другой. То есть фактически нужно показать, что таких двух формул нет (остальные случаи "линейности" не мешают).
На самом деле любая формула в I является либо тавтологией, либо эквивалентна p, то есть принимает T при p=T и F при p=F. Это как раз легко доказывается структурной индукцией (или натуральной по "глубине" построения формулы). Можно, кстати, доказывать и то свойство, которое вы предложили, оно тоже подойдёт.
Чтобы структурной индукцией доказать, что все формулы из I обладают нужным свойством, нужно лишь показать, что p обладает этим свойством, и что обладает нужным свойством, коль скоро им обладают как , так и . А больше ничего и не требуется.

Благодарю за помощь!
Запечатал задание, почти неделю над ним сидел.
Таки курс не из простых.

Теперь надо за до конца недели сделать теорвер и дискретку, потом браться за следующее задание по логике...

Бесит нелогичная логика. :(

Вот смотрите: на форуме курса сказали, что означает "нет такой модели, которая выполняет бету", а означает «есть такая модель, которая выполняет альфу и не выполняет бету». Нелогично, по-моему.

Впрочем, может и логично...

Цитата: RawonaM от апреля 15, 2011, 20:13
на форуме курса сказали, что означает "нет такой модели, которая выполняет бету"

Не ну это ваще беспредел...
В другом месте на форуме сказали, что это означает, что «не все модели выполняют бету»...
Что более логично, но ведь путаница страшная, иди знай, что имелось в виду.

Цитата: RawonaM от апреля 15, 2011, 21:33
В другом месте на форуме сказали, что это означает, что «не все модели выполняют бету»...

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

Цитата: arseniiv от апреля 15, 2011, 21:43
Скорее всего, именно это

Мне тоже так кажется. Тем более, что задание тут получается неправильное, если с тем вариантом.

Вроде контрадикцию как-то по другому обозначают.

Мне нужно доказать, что система выводов, включаяющая две аксиомы из системы Гильберта и единственное правило вывода Modus Ponens обладает свойством дедукции.
Мне кажется я доказал это с помощью только одной аксиомы, поэтому терзают сомнения.

Также спрашивается, если добавить к MP еще какое-то правило, то изменится ли свойство. Вот это я не врубаюсь. Система должна быть sound. Вроде кажется, что ничего не изменится, но вопрос подозрителен.

Цитата: RawonaM от апреля 19, 2011, 14:51
включаяющая две аксиомы из системы Гильберта

Какие именно?
Эти что ли?


Или другие какие-то?

Цитата: RawonaM от апреля 19, 2011, 14:51
обладает свойством дедукции

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

Цитата: Gerbarius от апреля 19, 2011, 16:23

Цитироватьвключаяющая две аксиомы из системы Гильберта

Какие именно?
Эти что ли?


Или другие какие-то?

Да, эти.

Цитата: Gerbarius от апреля 19, 2011, 16:23

Цитироватьобладает свойством дедукции

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

Точнее, что это следует в обе стороны.

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

Вторую сторону затрудняюсь. Написано примечание, что для начала рекомендуется доказать . Доказал, но не пойму куда его притулять.

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

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

Тут нужно рассмотреть все случаи, как может быть получен вывод .
Их всего три.
1) входит в или - аксиома. Тогда по определению . Отсюда и из   получаем .
2) - это . В этом случае как раз и нужно , а точнее,
что , что впрочем следует из первого.
Этот случай к предыдущему, если что, не сводится, так как может не быть аксиомой и может
не входить в , а потому может быть неверно (а именно на этом основаны рассуждения в предыдущем случае).
3) получено по правилу modus ponens из и . Допускаем, что мы можем построить выводы и . Тогда вывод строится при помощи этих выводов и аксиомы .
Отсюда дедукционная теорема следует в силу обычной математической индукции по длине вывода (или в силу дедуктивной индукции, если она вам знакома).
Можно привести  и вполне конкретный алгоритм построения нужного вывода. означает, что у нас есть вполне конкретный вывод, который можно, например, представить в виде дерева (в данном случае бинарного). В узлах дерева мы записываем утверждения вида . Утверждения во внутренних узлах получаются из утверждений в дочерних узлах по правилу modes ponens, а утверждения в конечных узлах получаются как в случаях 1 и 2. Затем мы просто последовательно преобразуем это дерево в другое, где  поддеревья с корневым узлом преобразуются в поддеревья с корневым узлом . Сначала преобразуются поддеревья, состоящие из конечных узлов, по алгоритму, рассмотренному в случаях 1 и 2, а затем и все остальные, для которых уже преобразованы оба дочерних поддерева, по алгоритму, описанному в случае 3, пока не будет преобразовано всё дерево.

Цитата: RawonaM от апреля 19, 2011, 14:51
Также спрашивается, если добавить к MP еще какое-то правило, то изменится ли свойство. Вот это я не врубаюсь. Система должна быть sound. Вроде кажется, что ничего не изменится, но вопрос подозрителен.

Аксиомы можно добавлять какие угодно. То рассуждение, которое я привёл выше, не изменится никак. Но если добавить новое правило вывода, то появляется ещё один случай, который нужно рассматривать отдельно. В этом случае справедливость дедукционной теоремы может быть нарушена. Например, если добавить правило подстановки, что из можно вывести , где получено из подстановкой некоторой формулы вместо некоторого атома (во всех вхождениях этого атома в ), то дедукционая теорема уже не будет верна. Например, из подстановкой можно получить , но получить нельзя. Хотя дедукционная теорема может и в таких случаях всё же оказаться справедливой, если наложить соответствующие ограничения на выводы, с которыми мы имеем дело.

Цитата: Gerbarius от апреля 19, 2011, 19:34
Отсюда дедукционная теорема следует в силу обычной математической индукции по длине вывода

У вас получилось так компактно это написать...
Наши почему-то всегда пишут доказательство по индукции в полной форме, т.е. базис индукции (доказательтво в одну строку) и шаг индукции (доказательтво в n строк), хотя по сути они в основном повторяют друг друга.

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

Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы и .

Как же вы это можете допустить? Вы же это доказываете...
Или я чего-то недопонял.

Цитата: RawonaM от апреля 21, 2011, 21:33

Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы и .

Как же вы это можете допустить? Вы же это доказываете...
Или я чего-то недопонял.

Доказывается-то всё индукцией, а это фактически индуктивное предположение, которое используется при обосновании шага индукции. Правда, в случае обычной математической индукции всё выглядит несколько сложнее по форме. То есть в этом случае нужно сначала явно рассмотреть базис индукции, который включает в себя случаи 1 и 2 (только они возможны для выводов длины 1), а затем, допустив, что дедукционная теорема справедлива для всех выводов длины , показать что она справедлива и для выводов длины (шаг индукции). Обоснование шага индукции включает в себя повторное рассмотрение случаев 1 и 2 и случай 3. При рассмотрении случая 3 длина каждого из выводов и будет меньше длины рассматриваемого вывода , а значит, к ним применимо индуктивное предположение. То есть фразу

Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы и .

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

Но в случае дедуктивной индукции всё несколько проще, хотя и не принципиально. Попробую рассказать про неё. Допустим, у нас есть класс высказываний, (в нашем случае это выражения вида ), и из них выделен класс "теорем" следующим образом:
1) Выделен класс "аксиом", то есть высказываний, которые "автоматически" считаются теоремами. В нашем случае это выражения вида , где либо входит в , либо является аксиомой в рассматриваемой нами системе гильбертовского типа.
2) Выделен ряд правил вывода, каждое из которых из заданного числа посылок-"теорем" строит заключение-"теорему". В нашем случае есть единственное правило .
3) "Теоремы" - это те и только те высказывания, которые могут быть "выведены" из "аксиом" при помощи конечного числа применений правил вывода.
Тогда, чтобы доказать, что некоторое свойство справделиво для всех "теорем", достаточно доказать, что
оно справедливо для всех "аксиом", и что для всякого правила вывода его заключение обладает этим свойством, коль скоро им обладают его посылки. В этом и состоит принцип дедуктивной индукции.
В нашем случае применение дедуктивной индукции просто сводится к рассмотрению случаев 1, 2, 3 буквально в том виде, как я написал. В этом случае

Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы и .

это просто (индуктивное) предположение, что доказываемое свойство справедливо для посылок применения правила modus ponens.

Цитата: Gerbarius от апреля 19, 2011, 19:34
Например, если добавить правило подстановки, что из можно вывести , где получено из подстановкой некоторой формулы вместо некоторого атома (во всех вхождениях этого атома в ), то дедукционая теорема уже не будет верна. Например, из подстановкой можно получить , но получить нельзя.

P* ведь должен следовать логически из P, да? Иначе же система не будет sound.
Например вроде сойдет.

А точно из этого нельзя получить ?
Это же тавтология...

Цитата: RawonaM от апреля 22, 2011, 09:27

Цитата: Gerbarius от апреля 19, 2011, 19:34
Например, если добавить правило подстановки, что из можно вывести , где получено из подстановкой некоторой формулы вместо некоторого атома (во всех вхождениях этого атома в ), то дедукционая теорема уже не будет верна. Например, из подстановкой можно получить , но получить нельзя.

P* ведь должен следовать логически из P, да? Иначе же система не будет sound.
Например вроде сойдет.

А точно из этого нельзя получить ?
Это же тавтология...

Я забыл добавить, что мой контрпример относится к обычному классическому исчислению высказываний, но надеюсь, это не вызвало недоразумений.
не обязано ни из чего следовать. Оно просто получается из некоторым формальным преобразованием. Нас ведь спрашивают, что будет, если добавить ещё одно правило, но в выборе этого правила нас никто не ограничивает, а потому для построения контрпримера можно взять любое удобное правило. Опять-таки для контрпримера достаточно указать ровно один случай, когда дедукционная теорема не выполняется. Конечно, можно получить, но уже нет, и одного этого только достаточно, чтобы заключить, что дедукционая теорема при добавлении к классическому исчислению высказываний правила подстановки справедлива не будет. Замечу, кстати, что под невыводимостью  , конечно, имеется в виду невыводимость в системе, к которой добавлено правило подстановки. Строго говоря, это не совсем очевидно, но можно показать, что в классическом исчислении высказываний с единственным правилом modus ponens, из следует , а потому добавление правила подстановки не увеличивает множество доказуемых формул. Тогда  невыводимо (даже с правилом подстановки) просто потому, что это не тавтология.

В задании требуется чтобы система была sound, т.е. чтобы все, что можно вывести, следовало логически.

Цитата: RawonaM от апреля 22, 2011, 17:14
В задании требуется чтобы система была sound, т.е. чтобы все, что можно вывести, следовало логически.

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

Я так понимаю, что у нас по умолчанию имеется в виду strong soundness (все, что выводится из чего-то, должно логически следовать), в противопоставление weak soundness (это когда из ничего только тавтологии выводятся, других ограничений нет).

Тогда можно рассмотреть систему, в которой есть только две схемы аксиом (и никаких других аксиом кроме как определяемых этими схемами нет)


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

Почему-то пропустил ваше последнее сообщение.

Цитата: Gerbarius от апреля 22, 2011, 22:08
Тогда при помощи этого правила можно построить вывод , но вывод построить уже нельзя.

А точно нельзя? Я выше как раз этим вопросом задавался. Как доказывается, что вывести нельзя?

Цитата: RawonaM от апреля 30, 2011, 10:21
Почему-то пропустил ваше последнее сообщение.

Цитата: Gerbarius от апреля 22, 2011, 22:08
Тогда при помощи этого правила можно построить вывод , но вывод построить уже нельзя.

А точно нельзя? Я выше как раз этим вопросом задавался. Как доказывается, что вывести нельзя?

Здесь это можно сделать достаточно просто при помощи "кривых" таблиц истинности. То есть для всех логических связок кроме дизъюнкции берём обычные таблицы истинности, а для дизъюнкции берём "кривую" таблицу, которая содержит одни . То есть у нас будет . Относительно этих таблиц определяем понятие тавтологии точно так же как и раньше (только таблицы сейчас немного другие). Назовём их условно "кривыми" тавтологиями. После чего доказываем, что в нашей системе выводимы только "кривые" тавтологии, например, дедуктивной индукцией. В этом случае нужно показать, что все аксиомы, задаваемые нашими двумя схемами, являются "кривыми" тавтологиями. И что заключения наших двух правил вывода являются "кривыми" тавтологиями, если таковыми являются их посылки. Для аксиом и правила modus ponens это показывается точно также как и для обычных тавтологий, так как в этом случае используются только свойства импликации, таблицу для которой мы не меняли. А в случае правила утверждение верно тривиально, так как не является "кривой" тавтологией. Кстати, можно заметить, что это правило в нашей системе вообще неприменимо, так как вывести нельзя. А дальше остаётся только показать, что не является "кривой" тавтологией, так как в случае значение формулы будет в соответствии с "кривыми" таблицами. В частности, здесь используется, что . Отсюда и следует невыводимость в нашей системе.

Я что-то торможу. Вы ходите доказать полноту системы в этой же самой системе? Если она позволяет диагональный метод, то см. Гёделя. Или в общих словах? В общих словах можно "доказать" что угодно. Очевидно, свойства системы доказывать надо в надсистеме.

Цитата: Alone Coder от апреля 30, 2011, 12:04
Я что-то торможу. Вы ходите доказать полноту системы в этой же самой системе? Если она позволяет диагональный метод, то см. Гёделя. Или в общих словах? В общих словах можно "доказать" что угодно. Очевидно, свойства системы доказывать надо в надсистеме.

Во-первых, с чего вы взяли, что я доказываю свойства системы (в данном случае некоторой разновидности исчисления высказываний) в самой системе? Напротив, все мои рассуждения определённо лежат вне этой самой системы. А в самой системе я могу только установить выводимость некоторых конкретных формул, построив конкретные доказательства.
Во-вторых, с чего вы взяли, что я доказываю какую-то полноту? Я же не доказываю, что в системе доказываются все формулы определённого вида. Я доказываю, что в системе доказываются только формулы определённого вида, то есть не полноту, а непротиворечивость относительно некоторой интерпретации.
В-третьих, причём тут Гёдель?  ;)

Цитата: Alone Coder от апреля 30, 2011, 12:04
Очевидно, свойства системы доказывать надо в надсистеме.

Это, кстати, не так. Доказательства многих свойств достаточно богатых систем можно формализовать в самих этих системах. В качестве примера можно привести ту же теорему Гёделя, которого вы упоминули всуе, о неполноте формальной арифметики. Доказательство этой теоремы прекрасно формализуется в той самой формальной арифметике, о которой идёт речь в теореме. Другое дело, что такой фокус проходит не всегда и не со всеми свойствами, но тем не менее.

Теорема Гёделя доказывается только в самоописывающей арифметике.

Цитата: Alone Coder от апреля 30, 2011, 14:25
Теорема Гёделя доказывается только в самоописывающей арифметике.

А вы не путаете формальную систему, о которой идёт речь в теореме, и те формальные системы, в которых её доказательство может быть формализовано? От последних, строго говоря, совсем не требуется, чтобы они были арифметическими или "самоописывающими". Последнее, конечно, скорее всего будет в какой-то степени иметь место, но это совершенно несущественно. И что, собственно, вы хотели сказать своим замечанием?

Цитата: Gerbarius от апреля 30, 2011, 15:11
Цитата: Alone Coder от Сегодня в 15:25

ЦитироватьТеорема Гёделя доказывается только в самоописывающей арифметике.

А вы не путаете формальную систему, о которой идёт речь в теореме, и те формальные системы, в которых её доказательство может быть формализовано?

Нет, не путаю. Доказательство теоремы Гёделя построено именно на этом свойстве системы.

Цитата: Gerbarius от апреля 30, 2011, 15:11
И что, собственно, вы хотели сказать своим замечанием?

То, что строя доказательство внутри самой системы, вы рискуете прийти к парадоксальным выводам типа теоремы Гёделя или теоремы Лёба. Не надо так делать.

Цитата: Alone Coder от апреля 30, 2011, 15:23
Нет, не путаю. Доказательство теоремы Гёделя построено именно на этом свойстве системы.

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

Цитата: Alone Coder от апреля 30, 2011, 15:23
То, что строя доказательство внутри самой системы, вы рискуете прийти к парадоксальным выводам типа теоремы Гёделя или теоремы Лёба. Не надо так делать.

А что в этом такого страшного? И разве кажущаяся вам парадоксальность, к примеру, теоремы Гёделя делает этот результат менее объективным? Или неполноту формальной арифметики (при условии её непротиворечивости - а в этом, я думаю, ни у кого нет никаких сомнений) вы не считаете объективным фактом?

Вы сильно всерьезн Алона Цодера не воспринимайте, он всем известен своими чудными идеями.  ;D

Цитата: Gerbarius от апреля 30, 2011, 15:55
Цитата: Alone Coder от Сегодня в 16:23

ЦитироватьНет, не путаю. Доказательство теоремы Гёделя построено именно на этом свойстве системы.

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

Не может. Вы не представляете, насколько разными бывают алгебры логики.

Цитата: Gerbarius от апреля 30, 2011, 15:55
Или неполноту формальной арифметики (при условии её непротиворечивости - а в этом, я думаю, ни у кого нет никаких сомнений) вы не считаете объективным фактом?

Теорема Гёделя работает только для той формальной арифметики, для которой может быть доказана. Если вы этого не понимаете, то говорить дальше не о чем.

Цитата: RawonaM от апреля 30, 2011, 16:30
Вы сильно всерьезн Алона Цодера не воспринимайте, он всем известен своими чудными идеями.

Удалите пост.

Цитата: Alone Coder от апреля 30, 2011, 22:14
Не может. Вы не представляете, насколько разными бывают алгебры логики.

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

Цитата: Alone Coder от апреля 30, 2011, 22:18
Теорема Гёделя работает только для той формальной арифметики, для которой может быть доказана. Если вы этого не понимаете, то говорить дальше не о чем.

И? Разумеется, теорема Гёделя доказывается для вполне конкретных формальных систем (или классов систем). Считайте, что в нашей дискуссии "формальной арифметикой" я называю одну из таких формальных арифметических систем. Если захотите, я вам даже полный набор аксиом выпишу. Надеюсь, теперь вы можете продолжить свою мысль.  ;)

И поясните же, зачем вы привели эту цитату из википедии? О том, что непротиворечивость определённых систем нельзя доказать средствами, формализуемыми в этих системах, мне прекрасно известно. Но если вы заметили, я этого нигде не опровергал и, более того, даже не касался этого вопроса.
Кстати, раз уж речь зашла о второй теореме Гёделя, то вам, противнику доказывания свойств системы в ней же самой, стоит вспомнить, как именно она доказывается.  ;)

Что это за свойство натуральных чисел зашифровано? Гадал-гадал, не врубился. А может и нет описания проще чем просто словами эту формулу пересказать...

Цитата: RawonaM от мая  7, 2011, 21:53


Что это за свойство натуральных чисел зашифровано? Гадал-гадал, не врубился. А может и нет описания проще чем просто словами эту формулу пересказать...

Если два числа имеют одни и те же делители, то они равны.
Кажется так.

Цитата: Gerbarius от мая  7, 2011, 22:10
Если два числа имеют одни и те же делители, то они равны.
Кажется так.

Так там же два разных квантификатора на делитель.
Для каждого числа можно получить это число путем деления х на что-то и у на что-то (можно другое), либо чтобы из обоих нельзя было получить делением, тогда это х=у.

Цитата: RawonaM от мая  7, 2011, 22:16
Так там же два разных квантификатора на делитель.
Для каждого числа можно получить это число путем деления х на что-то и у на что-то (можно другое), либо чтобы из обоих нельзя было получить делением, тогда это х=у.

Так означает же просто, что делится на , а ,  что  делится на . Замените всю формулу на и посмотрите, что она значит.

Действительно! Спасибо :)

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

Есть формула p в логике предикатов, в которой одна свободная переменная х.
Обозначим p(y)=sup(p,x,y), это значит все свободные х заменить на у.

Доказать, что если р не содержит у, то .
Не понимаю, что тут и как доказывать, это ведь совершенно очевидно.

Цитата: RawonaM от мая 10, 2011, 12:36
Не понимаю, что тут и как доказывать, это ведь совершенно очевидно.

Также как и прочие очевидности - явно использовать соответствующие определения.

Не понимаю, когда можно использовать универсальное обобщение?

Например дано .
По какой причине нельзя построить доказательство:

?

Цитата: RawonaM от мая 23, 2011, 16:36
Не понимаю, когда можно использовать универсальное обобщение?

Например дано .
По какой причине нельзя построить доказательство:

?

То есть вы хотите из сначала вывести , а затем из вывести ?  :??? Но, вообще говоря, из никакое не выводится.

Цитата: Gerbarius от мая 24, 2011, 12:43
То есть вы хотите из сначала вывести , а затем из вывести ?  :???

Именно. Что мне мешает?

Цитата: Gerbarius от мая 24, 2011, 12:43
Но, вообще говоря, из никакое не выводится.

Почему это? Если есть такой х, то мы можем его взять и будет Р(с) (с — тот самый х который есть).
Забыл как это называется. instantiation, что ли. Что я тут напутал?

Вот, Q7 тут меня смущает:
(wiki/en) Hilbert-style_deductive_system#Logical_axioms (http://en.wikipedia.org/wiki/Hilbert-style_deductive_system#Logical_axioms)

http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/exist_inst.html

http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/univ_gen.html

Цитата: RawonaM от мая 24, 2011, 12:57
http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/exist_inst.html

http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/univ_gen.html

Прокомментирую ваши ссылки. Тут дело вот в чём. В первом случае в обозначает некоторый конкретный, хотя, возможно, и неизвестный элемент (но ни в коем случае не произвольный). Во втором случае в обозначает произвольный элемент из заданной области. То есть у символа в этих двух случаях просто разные значения, которые смешивать нельзя, иначе получится какой-то софизм. То есть здесь фактически используются два рода переменных, но используемый символизм не очень хорошо позволяет их различать.

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

Цитата: RawonaM от мая 24, 2011, 12:53
Вот, Q7 тут меня смущает:
(wiki/en) Hilbert-style_deductive_system#Logical_axioms (http://en.wikipedia.org/wiki/Hilbert-style_deductive_system#Logical_axioms)

И правильно, что смущает. При помощи этой чудесной схемы аксиом можно вывести общее утверждение из любого частного случая. Было бы любопытно узнать, где авторы википедийной статьи её откопали. ;D

Цитата: Gerbarius от мая 24, 2011, 15:42

ЦитироватьВот, Q7 тут меня смущает:
(wiki/en) Hilbert-style_deductive_system#Logical_axioms

И правильно, что смущает. При помощи этой чудесной схемы аксиом можно вывести общее утверждение из любого частного случая. Было бы любопытно узнать, где авторы википедийной статьи её откопали. ;D

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

Цитата: Gerbarius от мая 24, 2011, 15:42
Но это не совсем традиционный подход. В более традиционных логических системах используются только переменные, обозначающие произвольные элементы.

У нас обозначают буквами a,b,c конкретные элементы, а x,y,z — переменные.

Цитата: Gerbarius от мая 24, 2011, 15:42
Прокомментирую ваши ссылки. Тут дело вот в чём. В первом случае в обозначает некоторый конкретный, хотя, возможно, и неизвестный элемент (но ни в коем случае не произвольный). Во втором случае в обозначает произвольный элемент из заданной области. То есть у символа в этих двух случаях просто разные значения, которые смешивать нельзя, иначе получится какой-то софизм. То есть здесь фактически используются два рода переменных, но используемый символизм не очень хорошо позволяет их различать.

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

Цитата: RawonaM от мая 24, 2011, 15:54
Такое правило вывода не википедисты придумали, нас тоже этому учат. К каждому правилу поставляется определенное ограничение.

Понимаете в чём дело. В исчислении предикатов действительно справеделиво , но уже в общем случае неверно. А википедисты, кажется, утверждают второе, а не первое.

Цитата: RawonaM от мая 24, 2011, 15:54
Что формально мне мешает такой бредовый вывод сделать?

Скажем так, у нас есть два рода формальных переменных, одни из которых обозначают конкретные объекты (a, b, c), а другие произвольные (x, y, z). Однако в формулировках правил к ним не относится. Это на самом деле содержательня переменная, которая обозначает некоторый формальный объект. И лучше её было бы обозначить как-нибудь по-другому, чтобы не путать её с формальными переменными, например, греческой буквой . Тогда правила станут выглядеть как и с теми ограничениями, что в первом случае обозначает формальную переменную, обозначающую конкретный объект, а во втором случае - формальную переменную, обозначающую произвольный объект. При применении каждого правила вместо содержательной переменной подставляется соответствующий формальный объект. Из при помощи первого правила можно вывести (при заданном ограничении) , но не . А при помощи второго правила можно получить из , но не из . И бредовый вывод не получается. Единственная, на мой взгляд, здесь трудность, что формализм описан недостаточно ясно, что и приводит к недоразумениям.

Цитата: Gerbarius от мая 24, 2011, 17:03
В исчислении предикатов действительно справеделиво , но уже в общем случае неверно.

А это не следует по дедукции?

Цитата: RawonaM от мая 25, 2011, 10:10

Цитата: Gerbarius от мая 24, 2011, 17:03
В исчислении предикатов действительно справеделиво , но уже в общем случае неверно.

А это не следует по дедукции?

Не следует. В исчислении предикатов к правилу modus ponens добавляются дополнительные правила вывода, и дедукционная становится справедливой лишь с некоторыми ограничениями. То есть в исчислении предикатов уже не всякий вывод можно преобразовать в вывод . Замечу, кстати, что и в чистом исчислении высказываний наличие или отсутствие ограничений на дедукционную теорему существенно зависит от формулировки исчисления.

А что касается формул вида , то они в общем случае выражают свойства довольно абсурдные с интуитивной точки зрения. Возьмём, например, предикат , который означает, что - простое число. Если допустить ,  то отсюда можно получить . Но поскольку верно, то можно немедленно получить , то есть что все числа простые. И было бы странно, если бы исчисление предикатов позволяло строить такие выводы. На самом деле, конечно, формулы вида в исчислении предикатов в общем случае недоказуемы, и это можно строго доказать.

Цитата: Gerbarius от мая 25, 2011, 12:08
Если допустить ,  то отсюда можно получить

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

В том то и дело, что из нельзя получить .

Как можно в логике предикатов понять, следует одно высказывание из другого или нет? В логике высказываний можно было построить таблицу истинности и все было видно, тут же ничего не поймешь. Сижу целый день подбираю методом тыка. :(

Из группы утверждений K не обязательно же следует A или ~A, правильно?

В общем, запутался вообще. У меня есть:






Для каждого из следующих утверждений нужно сказать, следует ли из утверждений 1-4:





Как к этому подходить?
Методом тыка нашел для 6 модель, которая показывает, что 6 не следует из 1-4.

Есть язык L={c, R} (c — константа, R — тринарное отношение). Формула p верна в некоей модели M. Почему у М обязательно есть минимальная модель?
Я так понимаю, что минимальная модель имеет область {c}, но все-таки неясно.

Цитата: RawonaM от июня 18, 2011, 17:40
тринарное

Тернарное!

Что-то я не могу врубиться: если модель Гербанда доказывает, что определенное высказывание верно, то она ведь опирается на определенную модель. Как можно сделать вывод, что она логически верна? Замучился уже...

Робот замучился выводить выводы... Жєсть...