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

[longstreet]

longstreet в сообщении #580824 писал(а):

Есть только истинные и ложные доказательства (и то в условном смысле, в каком? - см. выше).

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

-- 04.06.2012, 19:21 --

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

А при неформальном подходе, есть правильные доказательства?

"Правильное"-"неправильное" $-$ это Ваша отсебятина, я в ней разбираться не собираюсь. Я хотел только указать на то, что так не говорят (нет такого понятия).

-- 04.06.2012, 19:25 --

У меня создалось ощущение, что в целом Вы, Феликс Шмидель, не понимаете, что даёт математическое доказательство. Оно многое даёт, кроме самого доказанного факта. Неосмысленное получение доказательства из списка аксиом приведёт к стагнации математической мысли.

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

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

Потом, формально можно только проверить, выводится ли что-то из чего-то другого, или нет. А откуда будут браться начальные списки аксиом? Это нужно делать осмысленно, перебором этого не получить.

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

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

longstreet в сообщении #580827 писал(а):

"Правильное"-"неправильное" $-$ это Ваша отсебятина, я в ней разбираться не собираюсь. Я хотел только указать на то, что так не говорят (нет такого понятия).

Во- первых, так говорят ("правильное математическое доказательство"), во-вторых говорят "строгое математическое доказательство".
И единственное возможное понимание этого заключается в том, что в строгом математическом доказательстве вывод логически следует из аксиом и уже доказанных теорем.

Цитата:

Неосмысленное получение доказательства из списка аксиом приведёт к стагнации математической мысли.

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

Цитата:

У меня создалось ощущение, что в целом Вы, Феликс Шмидель, не понимаете, что даёт математическое доказательство. Оно многое даёт, кроме самого доказанного факта.

Я это прекрасно понимаю. Во многих случаях истиной является не доказанный факт, а то, что он следует из явных или неявных допущений.
Но из этого правила есть исключения, как в случае с выводом, что "Сократ-смертен", или что уравнение Ферма не имеет нетривиальных решений в натуральных числах.

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

[longstreet]

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

Во- первых, так говорят ("правильное математическое доказательство")

Дайте пруфлинк на достойный научный источник.

-- 04.06.2012, 20:58 --

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

Я это прекрасно понимаю.

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

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

longstreet в сообщении #580857 писал(а):

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

Во- первых, так говорят ("правильное математическое доказательство")

Дайте пруфлинк на достойный научный источник.

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

[longstreet]

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

Я не знаю такого источника, но знаю, что так можно сказать.

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

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

Давайте забудем о "правильных-неправильных" доказательствах и везде, где мы о них говорили, заменим их на "строгие-нестрогие" доказательства.

Давайте.

-- 04.06.2012, 22:03 --

Нужно хорошо представлять себе проблемы при использовании компьютера. Компьютерная проверка доказательств всё ещё остаётся предметом веры. Даже проверка всех программ (алгоритм для проблемы четырёх красок $~800$ стр.) и всех входных данных не может гарантировать от случайных сбоев или даже от скрытых пороков электроники (тут обычно вспоминают, что ошибки при выполнении деления у первой версии процессора Pentium были случайно обнаружены спустя полгода после начала его коммерческих задач - кстати, математиком, специалистом по теории чисел). Кстати, касательно проблемы четырёх красок, в компьютерном доказательстве, после самого доказательства, потом ещё около года ошибки находили (правда, на результат они не повлияли)...

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

[Ales]

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

[longstreet]

Как бы то ни было, компьютеры $-$ не панацея.

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

longstreet в сообщении #580885 писал(а):

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

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

[longstreet]

Вы не поняли. Это как раз один из главных доводов. Вы не сможете проверить всё компьютерное железо на отсутствие ошибок. Вы не можете проверять всё, что делает компьютер, Вы вынуждены полагаться на веру в его безошибочную работу. Если же Вы полностью проверяете доказательство, то смысл привлекать компьютер? Вы всё-равно не полностью его проверяете: Вы можете проверить только сам алгоритм и сам текст доказательства. То, как оно получено Вы проверить не можете (перебрать $100500$ вариантов вручную вместо компьютера как в проблеме четырёх красок).

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

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

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

-- 04.06.2012, 23:21 --

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

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

longstreet и Ales,

Я вовсе не предлагаю, чтобы компьютер занимался математикой вместо человека.
Человек находит идеи доказательств и проверяет их, прежде всего, исходя из их смысла.
Именно идеи и смысл составляют сущность математики, а не формализм.
Я сторонник того, чтобы доказательства излагались в простой и ясной форме и не загромождались большим колличеством формальных выкладок.
Но без формальных выкладок, математика не была бы математикой.
Формализм является другой стороной математики, которая имеет двойственную природу.
Он дополняет идеи и смысл и придаёт доказательствам бОльшую достоверность.

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

longstreet в сообщении #580915 писал(а):

Если же Вы полностью проверяете доказательство, то смысл привлекать компьютер? Вы всё-равно не полностью его проверяете: Вы можете проверить только сам алгоритм и сам текст доказательства. То, как оно получено Вы проверить не можете (перебрать $100500$ вариантов вручную вместо компьютера как в проблеме четырёх красок).

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

Цитата:

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

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

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

Я имел ввиду доказательство, найденное человеком, а не компьютером.
Автором доказательства является человек, который проверяет, вникая
в его смысл.
Компьютер проверяет формальное доказательство, которое дополняет обычное.

Цитата:

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

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

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

Прошу уважаемых модераторов переименовать эту тему на:

Введение в формальную математику (версия 1).

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

Я решил назвать эту тему: "Введение в математическую логику".
Первая версия этого введения не является удовлетворительной, потому что не основана на стандартном
формальном математическом языке: логике первого порядка.
С другой стороны, логика первого порядка является только ядром, недостаточным для формализации
математики.
Примером более полного формального языка, основанного на логике первого порядка является язык "Мицар".
После ознакомления с этим языком, я начал писать вторую версию этого введения.

========================================================================================================

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


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

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

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


Математические понятия.


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

Любые математические понятия, как первоначальные, так и не первоначальные записываются с использованием переменных.
Понятия, как и выражения, которые из них образуются, имеют тип объекта или утверждения.
Например, понятие "$x+y$" имеет тип объекта, а понятие "$x=y$ имеет тип утверждения.
Переменные тоже имеют тип объекта или утверждения, в частности в приведённых понятиях, $x$ и $y$ - переменные типа объекта.
Переменные объекты обозначаются латинскими буквами, возможно с индексами, например $x, y, z, X, Y, Z, x_1, y_2, z_3$.
Переменные утверждения обозначаются греческими буквами, например, $\alpha, \beta$.

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

В математике, иногда, используются переменные, содержащие другие переменные, например, $X(x), Y(x, y), \alpha(x), \beta(x, y)$.
Такие переменные называются переменными с аргументами.
Переменные с аргументами случаются в математических выражениях, но в математических понятиях они не используются.

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

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

В математике есть стандартный формальный язык, который называется логикой первого порядка.
Математические понятия записываются на языке логики первого порядка в следующей форме: $f(x_1, ..., x_n)$, где $f$ - так называемый функциональный или предикатный символ, а $x_1, ..., x_n$ - объектные переменные.
Например, понятие $x+y$ записывается на языке логики первого порядка в форме $+(x, y)$, где $+$ - функциональный символ.
В других формальных языках есть различные формы записи математических понятий, и форма $x+y$ является одной из них.

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

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

Следующие понятия являются первоначальными в логике:

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

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

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

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

Логические понятия имеют специальные обозначения, например, $\&$ (и), $\rightarrow$ (если ... то ..., из ... следует ...), $\Longleftrightarrow$ (тогда и только тогда, когда), $\exists$ (cуществует), $\forall$ (для любого).
Из других обозначений отметим непервоначальное понятие $\exists!$ (существует единственный).

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

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

Эти понятия имеют вид:
a) $x$ - натуральное число
б) $x$ - точка, $x$ - прямая
в) $x$ - множество

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

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

При определении понятия следует указать его область определения (для каких значений переменных оно определяется).
Например, понятие $x+y$ определяют сначала для целых неотрицательных чисел, затем для целых чисел, включая отрицательные.
Если допускаются произвольные значения переменных, то понятие не имеет области определения.
Логические и именующие понятия не имеют области определения.

Область определения понятия указывается при его определении.
В дальнейшем, при использовании понятия в выражениях, область определения обычно указывается до или после выражения.
Например: пусть $z=x+y$, где $x$ и $y$ - целые числа.


Математические выражения.


Приведём примеры математических выражений:

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

Начальными выражениями являются первоначальные понятия.
Новые выражения образуются подстановкой одних выражений в другие вместо свободных переменных.
При этом, заменяемая переменная и подставляемое выражение должны быть того же типа (объект или утверждение).
Можно также получать новые выражения заменяя одни переменные другими.
Например, можно получить выражение $y z$ из понятия $x y$.
Заменяя переменную без аргументов переменной с аргументами, можно получить выражения с предикатными и функциональными переменными.

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

Выражения 1) являются постоянными объектами, 2) - постоянными утверждениями, 3) - выражениями функций, 4) - выражениями свойств, 5) - выражениями отношений.

Математические утверждения со свободными объектными переменными называются предикатами.
Выражения свойств и отношений являются предикатами.


Аксиомы и аксиомные схемы.


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

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

Таким образом, аксиомная схема порождает бесконечное множество аксиом.

Например, выражение "если $x=y$ то $\alpha(x) \Longleftrightarrow \alpha(y)$" с предикатной переменной $\alpha(x)$ является аксиомной схемой.

Если вместо $\alpha(x)$ подставить, например, предикат $x \in z$, получится аксиома "если $x=y$ то $x \in z \Longleftrightarrow y \in z$.

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

Присутствие выделенной переменной $x$ в подставляемом предикате не является обязательным.
Например, можно вместо $\alpha(x)$ подставить предикат $1 \in z$ или даже постоянное утверждение $1=1$.
Вообще, в логике первого порядка формализм начинается после замены предикатной переменной подставляемым выражением, и при формулировке аксиомной схемы можно указать специальные правила подстановки.

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


Определения и аксиомы определения.


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

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

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

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

Аксиома определения утверждения имеет вид: $\alpha \Longleftrightarrow \beta$, где $\alpha$ - определяемое понятие типа утверждения, а $\beta$ - определяющий предикат с теми же свободными переменными, что и $\alpha$.

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

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

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

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

Можно давать аксиому определения объекта и в виде: $\beta(A)$.

При определении объекта должно выполняться следующее условие: "существует единственный $z: \beta(z)$".

Это условие, которое называется условием определения объекта, должно быть доказано перед принятием определения.

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


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

[arseniiv]

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

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

Логическим доказательством называется последовательное применение правила логического вывода $modes-ponens$, которое позволяет вывести истинность некоторого утверждения $\beta$ из истинности двух других утверждений $\alpha$ и "если $\alpha$, то $\beta$".

По-хорошему оно называется Modus ponens (и не надо его в доллары, зачем?). Кроме того, не обязательно правило вывода одно и только MP — могут быть и другие правила. Тем более странно говорить о MP до того как введён язык теории.

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

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

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

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

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

Стоит добавлять ссылки не в таком

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

Это доказал австрийский математик Курт Гёдель в 1931 году.
Из теоремы Гёделя

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Переменные объекты обозначаются латинскими буквами, возможно с индексами, например $x, y, z, X, Y, Z, x_1, y_2, z_3$.
Переменные утверждения обозначаются греческими буквами, например, $\alpha, \beta$.

Видимо, стоит дописать «здесь». Вообще ведь обозначается всё по-разному.

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

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

Рано. Не нужно.

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

В математике, иногда, используются переменные, содержащие другие переменные, например, $X(x), Y(x, y), \alpha(x), \beta(x, y)$.
Такие переменные называются переменными с аргументами.
Переменные с аргументами случаются в математических выражениях, но в математических понятиях они не используются.

Как минимум надо переписать. «Переменные с аргументами» — это очень интересное название само по себе, не говоря уже о финальной заметке, которая совершенно cryptic.

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

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

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

См. выше: вы вводите названия, забыв об обосновании. И далее опять таинственная заметка о понятиях, про которые (и выражения) см. выше тоже.

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

Математические понятия записываются на языке логики первого порядка в следующей форме: $f(x_1, ..., x_n)$, где $f$ - так называемый функциональный или предикатный символ, а $x_1, ..., x_n$ - объектные переменные.

Читатель наверняка не увидит связи. Даже несмотря на наличие примера ниже про функциональный символ.

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

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

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

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

Следующие понятия являются первоначальными в логике:

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

В записи с переменными, эти понятия имеют вид:

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

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

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

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

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

Из других обозначений отметим непервоначальное понятие $\exists!$ (существует единственный).

Стоило бы показать, каким формулам без $\exists!$ эквивалентны формулы с $\exists!$. И вообще, кое-кто может считать $\exists$ «непервоначальным». Опять же необходим рефакторинг всего этого, единичные замены на местах дело не улучшат.

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

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

Эти понятия имеют вид:
a) $x$ - натуральное число
б) $x$ - точка, $x$ - прямая
в) $x$ - множество

Или высказывания? Или это высказывания — примеры использования понятий? Или это просто двоекратное повторение. Менять.

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

При определении понятия следует указать его область определения (для каких значений переменных оно определяется).
Например, понятие $x+y$ определяют сначала для целых неотрицательных чисел, затем для целых чисел, включая отрицательные.
Если допускаются произвольные значения переменных, то понятие не имеет области определения.
Логические и именующие понятия не имеют области определения.

Область определения понятия указывается при его определении.

Это интересный вопрос, но не в таком виде.

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

В дальнейшем, при использовании понятия в выражениях, область определения обычно указывается до или после выражения.
Например: пусть $z=x+y$, где $x$ и $y$ - целые числа.

Снова конкретика без достаточных оснований не вовремя.

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

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

Не стесняйтесь упомянутых вами выше $\vee, \mathbin\&, \forall$ и пр.. А в текущем виде нужны запятые перед «то».

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

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

(1) Так и стоило указать те «первоначальные понятия», которыми были объявлены логические связки, кванторы и $=$, с переменными нужного типа в нужных местах. А пока там нечего заменять.
(2) Словами это описание ужасно длинно, и даже точность страдает. Введите правила построения выражений. Они в точности как правила вывода, только делают не из теорем теоремы, а из формул формулы. (После некоторых преобразований всё это можно свести к теоремам и правилам вывода как поступают, в частности, в Metamath.) Плюс типы были описаны тёмно.
(3) Переменные — тоже выражения, нечего их отделять от других.

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

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

Выражения 1) являются постоянными объектами, 2) - постоянными утверждениями, 3) - выражениями функций, 4) - выражениями свойств, 5) - выражениями отношений.

И чего это должго сказать? Это опять не обосновано/не вовремя.

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

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

Когда как.

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

Смысл аксиом со свободными переменными заключается в их истинности для любых значений свободных переменных.
Например, смысл аксиомы $x=x$ выражается утверждением: "для любого $x: x=x$".

Опять же, можно это выразить более понятным языком.

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

Аксиомной схемой

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

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

Например, выражение "если $x=y$ то $\alpha(x) \Longleftrightarrow \alpha(y)$" с предикатной переменной $\alpha(x)$ является аксиомной схемой.

Если вместо $\alpha(x)$ подставить, например, предикат $x \in z$, получится аксиома "если $x=y$ то $x \in z \Longleftrightarrow y \in z$.

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

Ну можно же определить подстановку нормальнее. И не использовать эти переменные со скобочками. Если $\alpha\equiv 28x + t$, то $\alpha[a/x]\equiv 28a + t$, $\alpha[x/t]\equiv 28x + x$, $\alpha[b/z]\equiv\alpha$ ($/$ можно читать как «вместо»). Более того, раз уж переменные для формул имеются, замену можно определить на уровне правил вывода и аксиом (опять же сошлюсь на Metamath, но в обоих упоминаниях всё придумано задолго до его автора, он просто удачно скомпилировал, а я для ссылания помню сейчас только его).

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

Язык "Мицар"

Не, ну тоже хоть сослались бы на него как-то более распространённо.

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

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

Это всё равно станет ясно дальше. Как отдельный факт это не нужно.

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

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

Можно давать аксиому определения объекта и в виде: $\beta(A)$.

Собственно, первый вид является частным случаем второго.

Наконец, если что-то не прокомментировано, это не значит, что там нечего комментировать.

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

-- Чт дек 11, 2014 01:03:54 --

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

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

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

Уважаемый arseniiv,

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

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

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

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