Логика и методология математики.

[Феликс Шмидель]

arseniiv в сообщении #943975 писал(а):

По крайней мере, в начале слишком раздуто или хуже того.

В чём это выражается?

arseniiv в сообщении #943975 писал(а):

По-хорошему оно называется Modus ponens (и не надо его в доллары, зачем?).

Согласен.

arseniiv в сообщении #943975 писал(а):

Кроме того, не обязательно правило вывода одно и только MP — могут быть и другие правила. Тем более странно говорить о MP до того как введён язык теории.

В логике первого порядка есть два правила вывода: Modus ponens и правило обобщения.
Но логика первого порядка это формальное исчисление, а не обычная логика.
С точки зрения обычной логики, утверждение $x=x$ не имеет смысла, а утверждение "для любого $x: x=x$ имеет.
В обычной логике есть только одно основное правило вывода: Modus ponens.
Все остальные правила вывода относятся к различным методам доказательства.
Условием применимости любого метода доказательства является существование логического доказательства с применением Modus ponens любого утверждения, доказанного этим методом.

arseniiv в сообщении #943975 писал(а):

Определением теорий в целом? Возможно, этот кусок стоит удалить.

Стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а теория множеств - аксиомами $ZFC$.
Что Вас не устраивает?

Продолжение следует.

-- Чт дек 11, 2014 12:29:43 --

arseniiv в сообщении #943975 писал(а):

Феликс Шмидель в сообщении #943498 писал(а):

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

Этот пассаж явно сократим.

Как его сократить, чтобы было ясно, для чего нужны первоначальные понятия?

arseniiv в сообщении #943975 писал(а):

Феликс Шмидель в сообщении #943498 писал(а):

Первоначальным понятиям даётся интуитивное и формальное определение.
Интуитивное определение описывает смысл первоначальных понятий и их свойства, лежащие в основе формального определения.
Формальное определение первоначальных понятий даётся в форме аксиом.

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

Как сказать это лучше?

arseniiv в сообщении #943975 писал(а):

Феликс Шмидель в сообщении #943498 писал(а):

Непервоначальным понятиям даются определения через понятия введённые ранее.

А как может быть иначе? Какое количество информации содержит это предложение? И кому нужно очередное новое имя «непервоначальные понятия»? Термины плодить на пустом месте не надо.

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

arseniiv в сообщении #943975 писал(а):

Феликс Шмидель в сообщении #943498 писал(а):

Любые математические понятия, как первоначальные, так и не первоначальные записываются с использованием переменных.

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

Само собой разумеющееся, и чем это плохо?

arseniiv в сообщении #943975 писал(а):

Феликс Шмидель в сообщении #943498 писал(а):

Понятия, как и выражения, которые из них образуются, имеют тип объекта или утверждения.
Например, понятие "$x+y$" имеет тип объекта, а понятие "$x=y$ имеет тип утверждения.
Переменные тоже имеют тип объекта или утверждения, в частности в приведённых понятиях, $x$ и $y$ - переменные типа объекта.

(1) Здесь надо уже начинать отказываться от слов.
(2) Определитесь, $x+y$ понятие или выражение, и если оба, то нужно ли иметь как термин «понятие», так и «выражение», потому что они тогда совпадут.

$x+y$ это понятие, которое является выражением, в силу того, что любое понятие является выражением.
Но не любое выражение является понятием.

Продолжение следует.

[grizzly]

Феликс Шмидель в сообщении #944177 писал(а):

arseniiv в сообщении #943975 писал(а):

Определением теорий в целом? Возможно, этот кусок стоит удалить.

Стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а теория множеств - аксиомами $ZFC$.
Что Вас не устраивает?

Феликс Шмидель,
Я тоже никак не мог пропарсить эту фразу:

Цитата:

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

С точки зрения меня, непрофессионала, здесь слово "определение" в сочетании с "понятием" и "теорией" имеет разные оттенки смысла. Русский язык (в отличие от мат.логики) не позволяет в таком случае использовать соединительный союз. Вот такой пример приходит в голову: "учёный в поисках ответа на вопрос зашёл в библиотеку и в тупик".

Если же я ошибся, и смысл понятия "определения" для профессионала в этих случаях тождественен, то между мной и профессионалом лежит некоторая пропасть, о преодолении которой, я считаю, должен заботиться не только я, но и автор :)

[Феликс Шмидель]

grizzly, дело здесь не в профессионалах и не профессионалах. Я не профессионал и пишу для не профессионалов. Вы были бы правы, если бы любой тупик был библиотекой. Я имел в виду, что определение любой математической теории состоит из определения её первоначальных понятий, которое даётся в форме аксиом. Так понятнее?

[grizzly]

Феликс Шмидель в сообщении #944251 писал(а):

Так понятнее?

Да, спасибо. Но вот только теперь понятно настолько, что не осталось сомнений.

[Феликс Шмидель]

И Вам спасибо. Обязательно вставлю это в текст.

[Xaositect]

Феликс Шмидель в сообщении #944177 писал(а):

В логике первого порядка есть два правила вывода: Modus ponens и правило обобщения.
Но логика первого порядка это формальное исчисление, а не обычная логика.
С точки зрения обычной логики, утверждение $x=x$ не имеет смысла, а утверждение "для любого $x: x=x$ имеет.
В обычной логике есть только одно основное правило вывода: Modus ponens.
Все остальные правила вывода относятся к различным методам доказательства.
Условием применимости любого метода доказательства является существование логического доказательства с применением Modus ponens любого утверждения, доказанного этим методом.

Это только в логике первого порядка в гильбертовском стиле много аксиом и два правила вывода.
Что такое "обычная логика"? По моему, как раз в практической логике есть много "приемов доказательства", которые используются именно как правила вывода, например, разбор случаев $A\vee B, A\to C, B\to C\vdash C$или доказательство от противного $A\to \mathbf{F} \vdash \neg A$. В качестве формализации ее можно взять системы типа Natural deduction.

[Феликс Шмидель]

Xaositect в сообщении #944320 писал(а):

По моему, как раз в практической логике есть много "приемов доказательства", которые используются именно как правила вывода, например, разбор случаев $A\vee B, A\to C, B\to C\vdash C$или доказательство от противного $A\to \mathbf{F} \vdash \neg A$. В качестве формализации ее можно взять системы типа Natural deduction.

Методов доказательства много и не нужно делать их частью основной логики.
Всё равно этим их не исчерпать, и всегда будет нужда в новых методах, которые упрощают доказательства и делают их более короткими.
Любой новый метод доказательства нуждается в обосновании.
Таким обоснованием может быть существование логического доказательства с применением Modus ponens любого утверждения, доказанного этим методом.

[Xaositect]

Феликс Шмидель в сообщении #944368 писал(а):

Методов доказательства много и не нужно делать их частью основной логики.
Любой новый метод доказательства нуждается в обосновании.
Таким обоснованием может быть существование логического доказательства с применением Modus ponens любого утверждения, доказанного этим методом.

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

[Феликс Шмидель]

Xaositect в сообщении #944372 писал(а):

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

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

[Xaositect]

Феликс Шмидель в сообщении #944404 писал(а):

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

Правила вывода абсолютно так же могут быть проверены с помощью таблиц истинности.

Феликс Шмидель в сообщении #944404 писал(а):

Что Вы имеете ввиду, говоря что одни логические аксиомы более интуитивно обоснованы, чем другие?

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

[Феликс Шмидель]

Логика первого порядка является стандартом благодаря своей простоте.
В ней нет аксиомных схем, поэтому её немного расширяют.
Более сложная логика с дополнительными правилами вывода не нужна для понимания оснований математики.

[Феликс Шмидель]

Уважаемый arseniiv! Я исправил первый параграф с учётом ваших замечаний.

Введение в математическую логику.


Математика занимается определением вводимых понятий, формулировкой утверждений и доказательством их истинности.
Доказательство это убедительное рассуждение, которое, при необходимости, можно перевести на формальный язык.
Формальный язык отличается от обычного тем, что существует автоматическая процедура (алгоритм), позволяющая проверять правильность записанного на этом языке математического текста.
Перевод математического текста на формальный язык редко осуществляется на практике, обычно достаточно понимания, что такой перевод возможен.
Логическим доказательством называется последовательное применение правила логического вывода Modus ponens, которое позволяет вывести истинность некоторого утверждения $\beta$ из истинности двух других утверждений $\alpha$ и "если $\alpha$, то $\beta$".
Правило вывода Modus ponens применяют один или более раз, до тех пор, пока ни будет получено доказываемое утверждение.
В формальных математических языках могут быть и другие правила вывода одних утверждений из других.
Поскольку доказательство опирается на уже известные истины, то первоначальные истины доказать невозможно.
Утверждения, принимаемые за истину без доказательства, называются аксиомами.
Аксиомы не нуждаются в доказательстве по той причине, что они являются определением вводимых понятий и
математических теорий в целом.
Например, теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а теория множеств - аксиомами Цермело-Френкеля.
Определение любой математической теории состоит из определения её первоначальных понятий, которое даётся в форме аксиом.

Система аксиом математической теории (и сама теория) нызывается противоречивой, если в ней можно доказать некоторое утверждение $\alpha$ и его отрицание "не $\alpha$".
Система аксиом математической теории (и сама теория) называется полной, если любое утверждение теории можно или доказать или опровергнуть.
В идеале, система аксиом математической теории должна быть непротиворечивой и полной, но этот идеал недостижим.
Если теория достаточна для того, чтобы в ней можно было определить арифметику, то утверждение о непротиворечивости теории невозможно доказать в рамках этой теории.
Утверждение о непротиворечивости теории можно перевести на язык арифметики, и, в таком виде, оно не следует из аксиом теории.
Поэтому, если такая теория непротиворечива, то она не является полной.
Это доказал австрийский математик Курт Гёдель в 1931 году.
Из теорем Гёделя не следует, что нельзя доказать непротиворечивость арифметики никаким способом.
Доказательства непротиворечивости арифметики имеются в теории множеств.

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

Цель этого введения познакомить читателя с элементами формальной математической логики.

[arseniiv]

(Оффтоп)

Феликс Шмидель в сообщении #944131 писал(а):

Очень благодарен Вам за подробный разбор текста и большое количество критических замечаний.

Спасибо, что почитали и сочли подробным.

Феликс Шмидель в сообщении #944131 писал(а):

Почему Вы не хотите, чтобы я исправил текст?

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

Xaositect в сообщении #944372 писал(а):

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

Присоединюсь. Такие правила и какую-то автоматизацию допускают.

Феликс Шмидель в сообщении #944177 писал(а):

В чём это выражается?

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

Феликс Шмидель в сообщении #944177 писал(а):

Стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а теория множеств - аксиомами $ZFC$.
Что Вас не устраивает?

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

Феликс Шмидель в сообщении #944177 писал(а):

Как его сократить, чтобы было ясно, для чего нужны первоначальные понятия?

Не знаю. Теория рассматривает какой-то набор объектов, и можно их как-то назвать (множества, натуральные числа и т. п.). Если несколько сортов переменных — тоже можно (множества и классы, напр.). Но можно не называть, т. к. для любой переменной её сорт предполагается известным. Вообще, вы так и не пояснили, для чего нужны и понятия, и выражения, и почему считаете расширение смысла слова «понятие» для называния строк над языком теории и даже отдельных символов алфавита допустимым — по-моему, это только собъёт с толку. Строки могут быть разными, но обозначать одно и то же — тут как раз незачем уходить от слова «выражение». И потом, при обсуждении теорий стоит использовать уже распространённую терминологию (формула, терм). Это окажет читателю услугу в будущем. Впрочем, повторяюсь.

Феликс Шмидель в сообщении #944177 писал(а):

Как сказать это лучше?

Опять же, не знаю. Если бы начинать с того, как предложения на «обычном математическом» формулизуются, то это пришло и ушло бы само собой. А если нет первоначальных понятий, а есть просто имя для любого объекта — то и определять никак не надо, ни интуитивно, ни формулами. Обоснование же именно такого построения теории и имени для её объектов — это уже вопрос отдельный, в теорию не входящий и не необходимый к рассмотрению математической логикой. Хотя это и не какой-то тёмный вопрос, по поводу него много всего написано.

Феликс Шмидель в сообщении #944177 писал(а):

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

Как я уже писал, мне не кажется разумным называть определённые формулы/термы/какие-то другие строки понятиями. И раз первоначальные понятия тоже можно исключить, вопрос исчезает.

Феликс Шмидель в сообщении #944177 писал(а):

Само собой разумеющееся, и чем это плохо?

Тем, что совершенно никак не сказывается на следующем. Вам всё равно придётся сказать, как именно переменные входят куда-то там. Зачем это предварительное эхо? То же со связками, кванторами и равенством. Их свойства придётся описать точнее.

Феликс Шмидель в сообщении #944177 писал(а):

$x+y$ это понятие, которое является выражением, в силу того, что любое понятие является выражением.
Но не любое выражение является понятием.

Это выражения без свободных переменных, правильно понимаю? А зачем отделять их только на этом основании? Что даёт «понятийность» выражения кроме указания, есть ли в нём свободные переменные, когда все конкретные операции над выражениями никак её не используют? Это как оговорки о непустоте множества в теореме, которая верна и для пустого — лишние движения, не приближающие результат.
_______

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

[Феликс Шмидель]

arseniiv в сообщении #944608 писал(а):

Феликс Шмидель в сообщении #944177 писал(а):

$x+y$ это понятие, которое является выражением, в силу того, что любое понятие является выражением.
Но не любое выражение является понятием.

Это выражения без свободных переменных, правильно понимаю?

Нет, неправильно. В понятиях, как правило, есть свободные переменные.
На английском языке "понятие" это "notion", а то, что я называю "первоначальное понятие" - "primitive notion".
Это стандартная терминология аксиоматики, и в Википедии есть статья о "primitive notion".
На русском языке "primitive notion" называется "неопределяемое понятие".
Я предпочитаю говорить о первоначальных понятиях, потому что считаю, что они определяются системой аксиом.

arseniiv в сообщении #944608 писал(а):

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

λ-исчисление и логики высших порядков сложнее логики первого порядка и по этой причине не подходят для
простого объяснения оснований математики неспециалисту в области математической логики.
Логика первого порядка достаточна, если добавить в неё предикатные переменные, для того чтобы можно было формулировать схемы аксиом.

Xaositect в сообщении #944372 писал(а):

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

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

arseniiv в сообщении #944608 писал(а):

Феликс Шмидель в сообщении #944177 писал(а):

Само собой разумеющееся, и чем это плохо?

Тем, что совершенно никак не сказывается на следующем. Вам всё равно придётся сказать, как именно переменные входят куда-то там. Зачем это предварительное эхо? То же со связками, кванторами и равенством. Их свойства придётся описать точнее.

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

[arseniiv]

arseniiv в сообщении #944608 писал(а):

Это выражения без свободных переменных, правильно понимаю?

Феликс Шмидель в сообщении #944671 писал(а):

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

Ой. Я как раз хотел сказать «со свободными» — не знаю, с чего перепутал. А вот формулы без свободных переменных как раз имеют название — замкнутые (и в λ-исчислении — замкнутые термы с синонимом комбинаторы).