Логика

[RawonaM]

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

[Gerbarius]

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


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

[RawonaM]

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

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

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

[Gerbarius]

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

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

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

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

[Alone Coder]

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

[Gerbarius]

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

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

[Gerbarius]

Очевидно, свойства системы доказывать надо в надсистеме.

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

[Alone Coder]

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

[Gerbarius]

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

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

[Alone Coder]

Цитата: Alone Coder от Сегодня в 15:25

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

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

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

И что, собственно, вы хотели сказать своим замечанием?

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

[Gerbarius]

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

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

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

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

[RawonaM]

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

[Alone Coder]

Цитата: Alone Coder от Сегодня в 16:23

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

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

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

[Alone Coder]

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

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

[Alone Coder]

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

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

[Gerbarius]

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

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

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

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

[Gerbarius]

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

[RawonaM]

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

[Gerbarius]

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

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

[RawonaM]

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

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

[Gerbarius]

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

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

[RawonaM]

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

[RawonaM]

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

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

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

[Gerbarius]

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

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

[RawonaM]

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

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

?