Comments | falcao: правила логического рассуждения: обсуждение

falcao

правила логического рассуждения: обсуждение

Feb 15, 2007 07:21

Я только что разместил серию больших постов о правилах логического рассуждения (в трёх частях). Это часть 1 -- исчисление высказываний, часть 2 -- исчисление предикатов, и часть 3 -- теорема Гёделя о полноте исчисления предикатов. Комменты в основных постах отключены. Обсуждение можно проводить здесь; все посты и обсуждение являются общедоступными.

математика

Comments 106

kdv2005 February 15 2007, 06:50:48 UTC

Виктор, я прочел до середины второй части, очень хорошо написано, но хочу пожаловаться на непривычный вид кванторов -- глаз спотыкается и тормозится чтение. А можно воспользоваться символами из этой таблички?
http://www.danshort.com/HTMLentities/index.php?w=maths

kurbatov February 20 2007, 11:24:46 UTC

Можно считать, что уважаемый falcao использует в качестве квантора общности букву A, перевёрнутую справа налево, а в качестве квантора существования - букву E, перевёрнутую сверху вниз.

обозначения falcao February 22 2007, 00:26:15 UTC

На самом деле обозначения в виде A и E даже встречаются в литературе, хотя я их использовал из-за трудностей с наличием спецсимволов.

Re: обозначения kurbatov February 22 2007, 10:13:41 UTC

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

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

Thread 5

Дочитал kdv2005 February 15 2007, 07:24:06 UTC

По-моему, очень хороший план. Мне тоже гентценовский подход больше нравится -- он легче воспринимается при первом знакомстве с логикой. Правда, когда я прочел книжку Смаллиана "First order logic", то метод семантических таблиц навсегда покорил мое сердце. Тем более, что он позволяет строить модели для данного списка аксиом, правда они не будут очень содержательными с точки зрения нашей интуиции.

PS Мой предыдущий комментарий носит временный характер и, если хотите, его можно стереть.

приёмы falcao February 15 2007, 12:11:55 UTC

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

К тому же "жирные" буквы A, E для кванторов в принципе встречаются в литературе.

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

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

Re: приёмы kdv2005 February 16 2007, 15:45:40 UTC

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

требования falcao February 16 2007, 17:34:21 UTC

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

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

alisarin February 15 2007, 07:43:17 UTC

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

кодирование falcao February 15 2007, 12:04:21 UTC

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

Но ясно, что такие вещи не дают ничего нового. Более того, проблема возникает с тем, какие формулы задают "законы", а какие -- не задают. Если мы не умеем отличать истинные арифметические формулы от ложных или доказуемые предложения от недоказуемых, то правило сопоставления будет абстрактным и бесполезным.

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

Re: кодирование alisarin February 15 2007, 12:36:30 UTC

Совсем не это. Нет. Вопрос куда более философски примитивен: до момента доказательства теоремы Пифагора доказанное в ней отношение было справедливо или нет? Если было, то как в общей форме сформулировать независимость математических норм от физических условий? (А человек, в определенной мере хотя бы "пользователь" условий физического мира, для своей деятельности он нуждается во времени, пространстве и материи.)

Re: кодирование timur0 February 15 2007, 14:43:42 UTC

>>до момента доказательства теоремы Пифагора доказанное в ней отношение было справедливо или нет?
А еще можно спросить: до того, как теорема Пифагора была сформулирована, была ли она верна? Строгого ответа на эти вопросы не может быть - реалисты (платоники) считают, что математика исследует вневременной мир идеальных ("реальных" в платоновском смысле) объектов, тогда ответ "да"; конструктивисты считают наоборот, что математика есть произведение человека (его конструкции), тогда ответ "нет"; в математике существуют недоказуемые и неопровержимые утверждения (к примеру, гипотеза континуума), по ее поводу sowa как-то сказал, что Бог может еще решить, сделать верной ее или ее опровержение. Это последнее утверждение предполагает своеобразный двухуровневый конструктивизм: для Бога математика конструктивна, для людей идеальна (в смысле они изучают "реальные" идеи); красота дальнейшего построения в том, что Бог, видя человеческую математику, может так подправить идеальные объекты, что они повернутся людям чуть иной стороной и станет возможно ( ... )

Thread 15

jared_lj February 16 2007, 01:01:36 UTC

> Классическую "формальную логику" с
> её "железобетонными" конструктами,
> на мой взгляд, следует считать
> безнадёжно устаревшей. Я бы очень
> хотел написать отдельный пост на эту
> тему с критикой формальной логики
> и обоснованием её недостаточности.

У меня ровно такое же впечатление. Причем на том уровне, что "формальная логика" просто довольно плохо годится для описания реального мира, нас окружающего (что является неким эмпирическим, философским фактом). Вернее, годится для очень малого круга достаточно простых явлений. Было бы интересно увидеть Ваш пост на эту тему!

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

заформализованность falcao February 16 2007, 01:09:52 UTC

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

Это совершенно верно. И мне кажется, что было бы очень полезно явно указать рамки применимости этой "науки наук" :)

Я до идеи правил (приёмов) доказательства вместо традиционной схемы дошёл совсем недавно. До этого я просто разъяснял смысл аксиом, доказывал теорему дедукции. Но это ведь совершенно ненужное усложнение, причём двойное. Проверки, перепроверки... Базовые-то идеи совершенно простые!

Завтра утром (точнее, сегодня уже) пойду как раз читать первую лекцию по логике в этом семестре. Вместо учебников буду давать студентам ссылку на ЖЖ. Пусть "приобщаюццо" :)

Re: заформализованность timur0 February 16 2007, 05:55:25 UTC

>>Вместо учебников буду давать студентам ссылку на ЖЖ.
Я даже не знаю, завидую или сочувствую так обучаемым студентам :)
Что же касается всей концепции курса, то как семестровый курс логики для всех математиков (не логиков) - очень правильный подход, хотя не совсем понимаю уровня его строгости - как-то странно без понятия терма доказывать теорему Левенгейма-Сколема; также при таком подходе трудно будет объяснить возможность иных правил вывода, все-таки логические аксиомы тут необходимы. Хотя все эти трудности вполне преодолимы.

лектуры falcao February 16 2007, 19:14:13 UTC

А чего им сочувствовать? :) Я же по учебникам никогда не читаю, а тут они могут и текст в ЖЖ посмотреть, и "жжЫвьём" пообщаться, вопросы задать :)

Сегодня прочитал как раз две лекции, рассказал полностью про исчисление высказываний, с примерами и теоремой о полноте ИВ.

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

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

Теорема Гёделя и множественность моделей kamchatnov February 16 2007, 09:01:25 UTC

Спасибо за интересный пост - такое сжатое и простое изложение очень полезно, поскольку изучать книги по логике нет ( ... )

Re: Теорема Гёделя и множественность моделей timur0 February 16 2007, 09:13:11 UTC

>>... у меня ранее сложилось впечатление, что теорема Гёделя утверждает существование недоказуемых и неопровержимых утверждений ВНУТРИ какой-либо достаточно богатой аксиоматической теории (типа арифметики), и при этом теорема не даёт конструктивного построения такого утверждения.
Впечатление в корне неверное - такое утверждение именно строится, выписывается ЯВНО. Более того, доказательство теоремы Геделя отвечает требованиям интуиционистской логики, так что это действительно фундаментальный факт, от которого не отмахнуться. Интересней другой вопрос - а не являются ли такие утверждения в какой-то мере неинтересными, периферийными? Как-то этот вопрос в ЖЖ обсуждался и приводились математические утверждения, возникшие не в логике, в традиционной математике, которые не доказуемы и не опровержимы в породившей их теории. Так что и загнать на периферию теорему Геделя не получается.

Re: Теорема Гёделя и множественность моделей kamchatnov February 16 2007, 14:14:39 UTC

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

Очень интересно! А не могли бы Вы дать ссылку или пояснить, что это за утверждения и как они связаны с теоремой Гёделя?

Re: Теорема Гёделя и множественность моделей kamchatnov February 16 2007, 15:10:21 UTC

Вот, нашёл, откуда, в частности, у меня возникло такое впечатление - с год назад просматривал выпуск Notices of AMS, посвящённый столетию Гёделя. Там в статье С. Фефермана ( ... )

Thread 19