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

[Someone]

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

В рамках какой теории мы это делаем?

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

[epros]

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

Мне неясно это определения предиката. Если предикат не выражается формулой теории, то что это такое?
Любое утверждение об объектах теории? Например, "натуральное число делится на чёрную дыру" является предикатом?

А «натуральное число» и «чёрная дыра» — оба являются объектами теории? Вообще-то предикат в данном случае должен записаться примерно так: $\text{Делится}(x, y)$, где $x$ и $y$ — объектные переменные, а стало быть вместо них могут подставляться любые комбинации конкретных натуральных чисел, чёрных дыр и прочих объектов теории. Если для некоторых аргументов невозможно в рамках теории вычислить значение истинности предиката, это не означает, что такого предиката «в принципе не может существовать».

В сущности, Ваши вопросы сейчас идут в правильном направлении в том смысле, что они должны прояснить для Вас различия между логиками первого и второго порядков. Вот смотрите: Теория первого порядка не может что-то утверждать обо «всех предикатах» (включая туда и то, что невыразимо в языке), а теория второго порядка — может. Отсюда — возможность доказательства чего-то, недоказуемого в теории первого порядка.

Кстати, это не значит, что любой синтаксически выразимый в теории первого порядка предикат однозначно определён в ней. Простой пример: Добавить в язык арифметики Пеано предикатный символ «Делится», но забыть добавить в аксиоматику определяющую его аксиому:
$\text{Делится}(x, y) \leftrightarrow \exists z \, y \times z = x$.
В таком случае мы не сможем в рамках теории доказать или опровергнуть делимость ни для какой пары чисел.

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

Someone в сообщении #948253 писал(а):

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

В рамках какой теории мы это делаем?

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

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

-- Ср дек 17, 2014 15:21:39 --

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

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

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

-- Ср дек 17, 2014 16:35:15 --

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

-- Ср дек 17, 2014 17:23:33 --

vicvolf в сообщении #948239 писал(а):

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

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

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

epros в сообщении #946284 писал(а):

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

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

[epros]

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

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

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

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

[Xaositect]

И это связано с тем, что в определении модели для логики второго порядка область изменения предикатных переменных жестко определена областью определения объектных. Если рассматривать арифметику второго порядка как теорию первого порядка с двумя сортами переменных (как делают в reverse mathematics), то моделей много.

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

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

И это связано с тем, что в определении модели для логики второго порядка область изменения предикатных переменных жестко определена областью определения объектных. Если рассматривать арифметику второго порядка как теорию первого порядка с двумя сортами переменных (как делают в reverse mathematics), то моделей много.

Уважаемый epros утверждает, что единственность модели является преимуществом логики второго порядка перед логикой первого порядка. Если эта единственность относительна, то в чём преимущество?

[epros]

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

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

Нет, что это преимущество — я не говорил. Я упомянул это просто как факт.

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

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

[epros]

Xaositect, тут мне тоже стало интересно.

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

Если рассматривать арифметику второго порядка как теорию первого порядка с двумя сортами переменных (как делают в reverse mathematics), то моделей много.

Правильно ли я понял, что речь о формализации «арифметики второго порядка» в логике первого порядка? Т. е. это примерно то же самое, что определение «стандартных натуральных чисел» в рамках ZFC (теории первого порядка)?

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

И это связано с тем, что в определении модели для логики второго порядка область изменения предикатных переменных жестко определена областью определения объектных.

Честно говоря, я плохо разбираюсь в различных типах семантик логики второго порядка (их ведь, вроде, несколько: помимо «полной» бывают какие-то урезанные?) Поэтому мне непонятно, какой смысл заключается в определении предикатной переменной как-то иначе, чем на «всех объектах и только на них»...

-- Чт дек 18, 2014 19:26:21 --

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

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

Нет, это не так. ZFC (формализация теории множеств в логике первого порядка) не знает ответа на вопрос об истинности гипотезы континуума, а логика второго порядка утверждает, что знает (но нам не говорит: это та самая недоказуемая общезначимая истина).

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

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

Насколько я знаю, язык логики второго порядка применяется для формализации проблем в reverse mathematics. А это — та самая дисциплина, которая изучает, что должно лежать в основаниях математики, чтобы мы не потеряли никаких важных результатов.

[Xaositect]

Да, это про разные семантики. В стандартной семантике теории в модели задается множество объектов $M$ и предикатные переменные пробегают все множество $2^M$. В генкиновской семантике задается множество объектов $M$ и множество предикатов $P\subset 2^M$, то есть то же самое, что для теории первого порядка, в которой есть два типа объектных переменных.

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

Новая версия первого параграфа введения:

Введение в основания математики на основе логики первого порядка.

Математика занимается определением вводимых понятий, формулировкой утверждений и доказательством их истинности.
Доказательство это убедительное рассуждение, которое, при необходимости, можно перевести на формальный язык.
Формальный язык отличается от обычного тем, что существует автоматическая процедура (алгоритм), позволяющая проверять правильность записанного на этом языке математического текста.
Перевод математического текста на формальный язык редко осуществляется на практике, обычно достаточно понимания, что такой перевод возможен.
Математические доказательства основаны на логике, которая позволяет выводить одни утверждения из других.
Основное правило логического вывода называется Modus ponens, оно позволяет вывести истинность некоторого утверждения $\beta$ из истинности двух других утверждений $\alpha$ и "если $\alpha$, то $\beta$".
Примером применения правила Modus ponens является вывод утверждения:
"число 1001001 делится на 3" из утверждений: "сумма цифр числа 1001001 делится на 3" и "если сумма цифр числа 1001001 делится на 3, то число 1001001 делится на 3".
Правило Modus ponens применяют один или более раз, до тех пор, пока ни будет получено доказываемое утверждение.
Поскольку доказательство опирается на уже известные истины, то первоначальные истины доказать невозможно.
Утверждения, принимаемые за истину без доказательства, называются аксиомами.
Аксиомы не нуждаются в доказательстве по той причине, что они являются определением вводимых понятий и математических теорий в целом.
Например, стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а стандартная теория множеств - аксиомами Цермело-Френкеля.
Определение любой математической теории состоит из определения её понятий, которое даётся в форме аксиом.
Аксиомы определяют понятия, но слово "определение" используется в математике в другом смысле.
Поэтому вместо аксиоматического определения понятий будем говорить об аксиоматическом введении понятий.
В любой математической теории есть два вида понятий: неопределяемые и определяемые понятия.
Неопределяемыми понятиями называются начальные понятия теории, которые вводятся системой аксиом.
Определяемые понятия вводятся математическими определениями, которые определяют эти понятия через понятия, введённые ранее.
Любое математическое определение порождает аксиому, которая является утверждением, верным "по определению".
Аксиомы, порождаемые математическими определениями, называются аксиомами определения.
Система аксиом математической теории задаётся списком выражений, каждое из которых либо является аксиомой, либо задаёт бесконечное множество аксиом.
Выражение, задающее бесконечное множество аксиом называется схемой аксиом или аксиомной схемой.
Кроме правила Modus ponens, в логике есть и другие методы доказательства утверждений.
Например, метод доказательства от противного, в котором для доказательства некоторого утверждения предполагают обратное и из этого ложного обратного выводят абсурдное следствие.
Различные методы доказательства нуждаются в обосновании, которым может быть сведение этих методов к доказательству в выбранной логической системе.
Назовём эту выбранную логическую систему базовой логикой, а доказательства в ней - базовыми доказательствами.
Условием применимости любого метода доказательства является существование базового доказательства любого утверждения, доказанного этим методом.
В математике есть стандартная логическая система, которая называется логикой первого порядка.
В этом введении мы выбрали логику первого порядка в качестве базовой логики.
Логика первого порядка может показаться необычной начинающему из-за короткой формы записи утверждений в этой логике.
Например, утверждение "для любого x: x=x" можно записать в короткой форме "x=x".
В логике первого порядка есть два правила вывода: Modus ponens и правило обобщения, которое позволяет из короткой формы утверждения получить более длинную.
Например, используя правило обобщения, можно из утверждения "x=x" получить утверждение: "для любого x: x=x".
Изучением логики первого порядка и других формальных логических систем занимается особый раздел математики, который называется математической логикой.
Математическая логика также изучает вопросы непротиворечивости и полноты математических теорий.
Система аксиом математической теории (и сама теория) нызывается противоречивой, если в ней можно доказать некоторое утверждение $\alpha$ и его отрицание "не $\alpha$".
Система аксиом математической теории (и сама теория) называется полной, если любое утверждение теории можно или доказать или опровергнуть.
В идеале, система аксиом математической теории должна быть непротиворечивой и полной, но этот идеал недостижим.
Если теория достаточна для того, чтобы в ней можно было определить арифметику, то такая теория не является полной и утверждение о непротиворечивости теории невозможно доказать в рамках этой теории.
Это следует из двух теорем австрийского математика Курта Гёделя, которые были опубликованы в 1931 году.
Утверждение о непротиворечивости теории можно перевести на язык арифметики, и, в таком виде, оно не следует из аксиом теории.
Это не значит, что нельзя доказать непротиворечивость арифметики никаким способом.
Доказательства непротиворечивости арифметики имеются в теории множеств.
Теория множеств, также как и логика, находится в основании современной математики.
В рамках теории множеств можно определить любое математическое понятие, и во многих разделах математики теория множеств является единственной используемой теорией.
Поэтому логику и теорию множеств часто объединяют.
Мы предпочитаем сначала объяснить логику и принципы построения математических теорий.
Теория множеств не рассматривается в этом введении.

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

Я прочитал главу об основаниях математике в учебнике Миши Вербицкого:
http://verbit.ru/MATH/UCHEBNIK/top-book.pdf

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

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

Я добавил определение строгого доказательства и обсуждение неполноты "определения" понятий системой аксиом.

Глава 1. Введение в основания математики на основе логики первого порядка.

1.1
Что такое математика.
Формализация математических доказательств.
Логический вывод одних утверждений из других.
Определение математических понятий аксиомами.
Определение математической теории системой аксиом.
Строгость доказательства и логический вывод из аксиом.
Неопределяемые и определяемые понятия.
Математические определения и аксиомы определения.
Неполнота "определения" неопределяемых понятий системой аксиом.
Аксиомы и схемы аксиом.
Методы доказательства и их обоснование.
Логика первого порядка.
Роль теории множеств в основаниях математики.
Математическая логика и вопросы непротиворечивости и полноты математических теорий.

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

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

Математические доказательства основаны на логике, которая позволяет выводить одни утверждения из других.
Основное правило логического вывода называется Modus ponens, оно позволяет вывести истинность некоторого утверждения $\beta$ из истинности двух других утверждений $\alpha$ и "если $\alpha$, то $\beta$".
Примером применения правила Modus ponens является вывод утверждения:
"число 1001001 делится на 3" из утверждений: "сумма цифр числа 1001001 делится на 3" и "если сумма цифр числа 1001001 делится на 3, то число 1001001 делится на 3".
Правило Modus ponens применяют один или более раз, до тех пор, пока ни будет получено доказываемое утверждение.
Поскольку доказательство опирается на уже известные истины, то первоначальные истины доказать невозможно.
Утверждения, принимаемые за истину без доказательства, называются аксиомами.

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

Например, стандартная теория арифметики определяется аксиомами Пеано, евклидова геометрия - аксиомами Евклида, а стандартная теория множеств - аксиомами Цермело-Френкеля.
Определение любой математической теории состоит из определения её понятий, которое даётся в форме аксиом.

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

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

Любое математическое определение порождает аксиому, которая является утверждением, верным "по определению".
Аксиомы, порождаемые математическими определениями, называются аксиомами определения.

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

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

Кроме правила Modus ponens, в логике есть и другие методы доказательства утверждений.
Например, метод доказательства от противного, в котором для доказательства некоторого утверждения предполагают обратное и из этого ложного обратного выводят абсурдное следствие.
Различные методы доказательства нуждаются в обосновании, которым может быть сведение этих методов к доказательству в выбранной логической системе.
Назовём эту выбранную логическую систему базовой логикой, а доказательства в ней - базовыми доказательствами.
Условием применимости любого метода доказательства является существование базового доказательства любого утверждения, доказанного этим методом.

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

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

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