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

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

Введение.

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

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

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

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

Формальные понятия.

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

1. Логические связки: "не", "и", "или", "или-или", "если ... то ...", "\Longleftrightarrow" (тогда и только тогда, когда)
2. Логические выражения: "существует" и "для любого"
3. Знак равенства: "=".

На выбранном нами формальном языке эти понятия имеют вид:
1. "не \alpha", "\alpha и \beta", "\alpha или \beta", "\alpha или-или \beta", "если \alpha то \beta", \alpha \Longleftrightarrow \beta
2. "для любого x: \alpha", "существует x: \alpha"
3. "x=y",

где x и y - переменные объекты, а \alpha и \beta - переменные утверждения.

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

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

На выбранном нами формальном языке эти понятия имеют вид:
a) "x-натуральное число"
б) "x-точка", "x-прямая"
в) "x-элемент", "x-множество"

Приведём примеры других формальных понятий (не обязательно первоначальных):
А) "x+y", "x-y", "xy", "x/y" ,"-x"
Б) "x - целое число", "x делится на y", "x - чётное число"
В) "0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10"

Непервоначальным понятиям даются определения через понятия введённые ранее.
Переменная x в первоначальных понятиях 2. называется связанной (выражениями "существует" и "для любого"), во всех других первоначальных понятиях все переменные называются свободными.
Переменные объекты могут быть либо свободными, либо связанными, переменные
утверждения - всегда свободны.
В непервоначальном понятии, переменные называются свободными (связанными),
если они свободны (связаны) в определяющем это понятие выражении.
Любое формальное понятие имеет тип объекта или утверждения.
Формальные понятия в примерах А) и В) имеют тип объекта, а в а), б), в) и Б) - тип утверждения.
При определении формального понятия, нужно указать его тип (объект или утверждение) и перечислить переменные с указанием их типа (по умолчанию, переменные считаются объектами. Кроме этого следует указать область определения понятия (для каких значений переменных оно определяется).
Например, понятие "x+y" определяют сначала для целых неотрицательных чисел, затем для целых чисел, включая отрицательные.
Формальное понятие не имеет области определения, если допускаются произвольные значения переменных.
Логические и именующие понятия не имеют области определения.

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

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

Формальные выражения.

Приведём примеры формальных выражений:

1) "1+2", "(1+2)3"
2) "1=1", "1=2", "для любого x: (x=x)"
3) "(x+y)z", "x+(yz)"
4) "(2x)=4", "(1+x)-чётное число"
5) "(x+y)=z", "если (x=y) то (y=x)"
6) "\alpha$ или (не $\alpha)", "если (\alpha$ и $\beta) то (\beta$ и $\alpha)"

Начальными формальными выражениями являются первоначальные понятия. Новые формальные выражения образуются подстановкой одних формальных выражений в другие вместо свободных переменных. При этом, заменяемая переменная и подставляемое выражение должны быть того же типа (объект или утверждение). Подставляемые выражения следует брать в скобки, но существуют специальные правила, позволяющие избавляться от лишних скобок.
Переменные, свободные в подставляемом выражении, могут стать связанными, попадая в зону действия выражений "существует" и "для любого".
Например, переменная x cвободна в выражении "x=x" и связана в выражении "для любого x: (x=x)".
Подстановки, при которых свободная переменная становится связанной, разрешаются только вместо переменных утверждений.
Можно получать новые формальные выражения и другим способом: заменяя одни переменные другими.
Таким способом, например, можно получить выражение "yz" из понятия "xy".
Замена какой-либо связанной переменной в формальном выражении на переменную, в нём не встречающуюся, не меняет смысла выражения.
Формальные выражения могут содержать одинаково обозначенные и, тем не менее, различные переменные.
Например, в выражении "(существует x: (x=x)) и (x=x)", первые три появления x представляют одну связанную переменную, а последние два появления x представляют другую свободную переменную.
Такие выражения допускаются, но подстановки в них или их разрешаются только после замены переменных таким образом, чтобы различные переменные имели различное обозначение.
Формальные выражения могут иметь неопределённый смысл, например "1/0". Чтобы не вводить сложные правила опознания и исключения таких выражений, мы будем придавать им некоторый смысл, например, будем считать "1/0" некоторым объектом, пусть неопределённым.
Формальные выражения без свободных переменных называются постоянными. Формальное утверждение с одним свободным переменным называется выражением свойства, а с двумя или более переменными - выражением отношения. Формальный объект со свободными переменными называется выражением функции.
Выражения с переменными утверждениями называются логическими и не считаются выражениями свойств или отношений.
Выражения 1) являются постоянными объектами, 2) - постоянными утверждениями, 3) - выражениями функций, 4) - выражениями свойств, 5) - выражениями отношений, 6) - логическими выражениями.

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

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

Область определения формальных выражений.

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

Например, при введении понятия "x/y" для целых чисел, указывают, что x - целое число, y - целое число и y\ne0.

Область определения непервоначального понятия, по умолчанию, ограничивается областью определения определяющего это понятие выражения.
Например, если понятие F(x, y) определяется как "2x/y", то необязательно указывать, что y\ne0.
Учёт определяющего выражения в области определения разрешается снимать специальным указанием, например, чтобы определить F(x, y) при y=0.

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

Область определения составного формального выражения находится из областей определения составляющих выражений.

Найдём область определения выражения А[Б], образованного подстановкой выражения Б в выражение А.

Формула области определения А[Б] включает выражения \alpha[Б] и \beta, где \alpha и \beta - выражения, включённые в формулы областей определения А и Б соответственно.
Мы обозначили через \alpha[Б] результат подстановки Б в \alpha вместо той же свободной переменной, что и при подстановке Б в А.
Если какая-либо свободная переменная в Б становится связанной в А[Б] и эта переменная является свободной в \beta, то \beta не включается в формулу области определения А[Б].
Например, выражение "существует z: (z=x/y)" не имеет области определения, но в дальнейшем мы покажем, что условие y\ne0 появится при подстановке вместо z конкретных значений.

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

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

Аксиомные выражения и аксиомы.

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

Например, "x=x" является аксиомным выражением, задающим аксиомы 1=1, 2=2, и т.д.
Из аксиомного выражения "x=x" можно получить аксиомное выражение "y=y", подставляя переменную y вместо x.
Напомним, что разрешаются только такие подстановки вместо переменных объектов, при которых свободные переменные в подставляемом выражении остаются свободными. Иначе, например, из истинного утверждения "существует x: x\ne$y" можно было бы получить ложное утверждение "существует x: x\ne$x".
Из одних аксиомных выражений можно получать другие также заменой связанных переменных на переменную не содержащуюся в выражении, поскольку смысл выражения при этом не меняется.

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

Сами аксиомы имеют вид: "если \alpha то А", где А - аксиомное выражение без свободных переменных, а \alpha - формула области определения А (если А не имеет области определения, то аксиомой считается просто А).

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

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

Интуитивное определение логических связок.
Таблицы истинности.

Пусть \alpha и \beta обозначают произвольные утверждения.
Выражения: 1. "не \alpha", "\alpha и \beta", "\alpha или \beta", "\alpha или-или \beta", "если \alpha то \beta", "\alpha \Longleftrightarrow \beta" являются утверждениями, истинность которых зависит от истинности утверждений \alpha и \beta.

1) Утверждение "не \alpha" истинно, если утверждение \alpha ложно.
В обычной речи, вместо частицы "не", употребляется выражение "неверно, что", или частица "не" вставляется в утверждение \alpha. Например: "неверно, что единица равна двум", "единица не равна двум".

2) Утверждение "\alpha и \beta" истинно если оба утверждения \alpha и \beta истинны.

3) Утверждение "\alpha или \beta" истинно, если хотя бы одно из утверждений \alpha и \beta истинно.
Случай, когда оба утверждения истинны не исключается.
Чтобы подчеркнуть это, часто пишут \alpha и/или \beta вместо \alpha или \beta.

4) Утверждение "\alpha или-или \beta" истинно, если одно из утверждений \alpha и \beta истинно, а другое ложно.

5) Утверждение "если \alpha то \beta" истинно, если оба утверждения \alpha и \beta истинны, а также, если утверждение \alpha ложно. Наличие истинных утверждений вида "если \alpha то \beta", в которых утверждение \alpha ложно, позволяет выводить следствия из ложных утверждений. На этом основан метод доказательства от противного, в котором для доказательства некоторого утверждения предполагают обратное и из этого ложного обратного выводят абсурдное следствие.

6) Утверждение "\alpha \Longleftrightarrow \beta" истинно, если оба утверждения \alpha и \beta истинны, а также, если оба утверждения \alpha и \beta ложны.

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

(здесь должны быть таблицы истинности)

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

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

Формальное определение логических связок.

Первоначальные логические понятия с переменными утверждениями \alpha и \beta:
"не \alpha", "\alpha и \beta", "\alpha или \beta", "\alpha или-или \beta", "если \alpha то \beta", "\alpha \Longleftrightarrow \beta" имеют тип утверждений и определяются бесконечной системой аксиом, задаваемых особыми аксиомными выражениями - логическими тождествами.

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

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

Приведём примеры логических тождеств и построим таблицу истинности для одного из них.

Пусть \alpha и \beta - переменные утверждения.

1. \alpha или (не \alpha)
2. \alpha \Longleftrightarrow (не (не \alpha))
3. (если \alpha то \beta) \Longleftrightarrow ((не \alpha) или \beta)
4. (если \alpha то \beta) \Longleftrightarrow (если (не \beta) то (не \alpha))
5. (\alpha или-или \beta) \Longleftrightarrow (не (\alpha \Longleftrightarrow \beta))
6. (не (\alpha и \beta)) \Longleftrightarrow ((не \alpha) или (не \beta))
7. (не (\alpha или \beta)) \Longleftrightarrow ((не \alpha) и (не \beta))

Проверим последнее формальное утверждение:

(здесь должна быть таблица истинности)

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

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

Интуитивное определение выражений "существует" и "для любого".

Если \alpha - постоянное утверждение, то истинность утверждений "существует x: \alpha" и "для любого x: \alpha" совпадает с истинностью \alpha.

Пусть \alpha(x) - какое-либо выражение свойства, со свободным переменным объектом x.

Образуем два утверждения:
1) "существует x: \alpha(x)"
2) "для любого x: \alpha(x)"

Если \alpha(x) имеет область определения, то рассматриваются не любые значения x, а только из этой области определения.

Истинность утверждений 1) и 2) определена только если их можно доказать или опровергнуть.

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

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

Утверждение 2) является отрицанием утверждения "существует x: не \alpha(x)"

Утверждение 1) истинно, если определён постоянный объект c из области определения \alpha(x), такой, что утверждение \alpha($с) истинно.

Утверждение 1) ложно, если предположение, что оно истинно, приводит к противоречию.

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

Если "существует x: \alpha(x)" то можно ввести произвольно выбранный объект c из области определения \alpha(x), такой, что \alpha($с) истинно.

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

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

Формальное определение выражений "существует" и "для любого".

Первоначальные логические понятия "существует x: \alpha" и "для любого x: \alpha" с переменным утверждением \alpha и переменным объектом x определяются бесконечной системой аксиом, задаваемых двумя аксиомными выражениями и аксиомами произвольного выбора.

Аксиомные выражения:

1) (для любого x: \alpha) \Longleftrightarrow не (существует x: не \alpha)

При подстановке выражений свойства \alpha(x) вместо переменной \alpha получаются аксиомы вида:

(для любого x: \alpha(x)) \Longleftrightarrow не (существует x: не \alpha(x))

2) если \alpha то (существует x: \alpha)

При подстановке выражений свойства \alpha(x) вместо переменной \alpha и постоянных объектов с вместо свободной переменной x получаются аксиомы вида:

если (\alpha($c) и \beta($c)) то (существует x: \alpha(x))

где \beta($c) - формула области определения выражения \alpha(x), в которой свободная переменная x заменена повсюду на с.

Если \alpha(x) не имеет области определения, то аксиома имеет вид:

если \alpha($c) то (существует x: \alpha(x))

Аксиомы произвольного выбора:

3) если (существует x: \alpha(x)) то (\alpha($c) и \beta($c))

где \alpha(x) - произвольное выражение свойства со свободной переменной x,
с - имя нового постоянного объекта, вводимого этой аксиомой,
\beta($c) - формула области определения выражения \alpha(x), в которой свободная переменная x заменена повсюду на с.

Если \alpha(x) не имеет области определения, то аксиома имеет вид:

если (существует x: \alpha(x)) то (\alpha($c))

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

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

Интуитивное определение равенства.

Знак равенства ставится между двумя выражениями, обозначающими один и тот же объект.

Если x и y обозначают один и тот же объект, то произвольное утверждение о x и то же самое утверждение о y либо оба истинны, либо оба ложны.


Формальное определение равенства.

Знак "=" определяется бесконечной системой аксиом, задаваемой аксиомными выражениями:

1) x=x

2) если x=y то \alpha \Longleftrightarrow \alpha(y$ вместо x)

Выражение 2) не является формальным (и значит аксиомным), аксиомные выражения образуются подстановкой вместо \alpha произвольного формального выражения типа утверждения со свободной переменной x (в котором нет связанных переменных x и y).

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

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

Определения.

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

Примером аксиомного определения утверждения является выражение:

"x-чётное число \Longleftrightarrow x делится на 2",

определяющее понятие чётного числа через понятие делимости на 2.

Аксиомное определение утверждения имеет вид: \alpha \Longleftrightarrow \beta, где \alpha - определяемое формальное понятие, а \beta - определяющее формальное выражение (типа утверждения).

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

Примером аксиомного определения объекта является выражение:

"z=min(x, y) \Longleftrightarrow (z=x и x\le$y) или (z=y и y\le$x)",

определяющее понятие наименьшего числа из двух чисел x и y.

Аксиомое определение объекта имеет вид: "z=A \Longleftrightarrow \beta, где A - определяемое формальное понятие, z - переменная не содержащаяся в A, а \beta - определяющее формальное выражение (типа утверждения) с теми же свободными переменными, что и "z=A".

Аксиомное определение объекта не является аксиомным выражением, аксиомное выражение имеет вид: "если \alpha то (z=A \Longleftrightarrow \beta)", где \alpha обозначает выражение: "существует единственный z: \beta" и называется условием определения объекта.

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

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

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

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

Методы доказательства.

Логическое доказательство не является единственным методом доказательства.

Например, выражение "если (для любого x: \alpha) то \alpha" не является (в нашем тексте) аксиомным, но из него подстановками можно получать теоремы, которые легко доказать для каждого конкретного утверждения \alpha.

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

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

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

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

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

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

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

Простое доказательство теоремы Гёделя о неполноте.

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

Возьмём некоторый язык программирования и занумеруем каким-либо образом все тексты на этом языке: T_1, T_2, ...
Выделим среди этих текстов программы, которые для каждого натурального числа на вводе вычисляют некоторое натуральное число на выводе.
Все эти программы расположены в порядке нумерации и образуют последовательность f_1(x), f_2(x), ...
Мы обозначили эти программы функциями, которые они вычисляют.
Определим функцию F(x)=f_x(x)+1 и докажем, что нет программы, которая эту функцию вычисляет.
Предположим, что такая программа есть, и F(x)=f_n(x). Тогда f_n(n)=F(n)=f_n(n)+1, что невозможно.
Полученное противоречие доказывает, что такой программы нет.
Рассмотрим последовательность утверждений вида:
"Текст T_n вычисляет некоторую функцию из f_1(x), f_2(x), ..."
Не существует программы, определяющей истинность или ложность каждого из этих утверждений (при n=1, 2, ...), потому что с применением такой программы алгоритм вычисления функции F(x)=f_x(x)+1 очевиден.
Теорема Гёделя доказана.

[Николай]

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