В математике и логике аксиоматическая система — это любой набор примитивных понятий и аксиом для логического вывода теорем . Теория — это последовательная, относительно самодостаточная совокупность знаний, которая обычно содержит аксиоматическую систему и все ее производные теоремы. Полностью описанная аксиоматическая система — это особый вид формальной системы . Формальная теория — это аксиоматическая система (обычно формулируемая в рамках теории моделей ), которая описывает набор предложений, замкнутый относительно логической импликации. [1] Формальное доказательство — это полное представление математического доказательства в рамках формальной системы.
Говорят, что аксиоматическая система непротиворечива , если в ней нет противоречий . То есть, из аксиом системы невозможно вывести как утверждение, так и его отрицание. Непротиворечивость является ключевым требованием для большинства аксиоматических систем, поскольку наличие противоречий позволило бы доказать любое утверждение ( принцип взрыва ).
В аксиоматической системе аксиома называется независимой, если ее нельзя доказать или опровергнуть с помощью других аксиом в системе. Система называется независимой, если каждая из ее базовых аксиом независима. В отличие от согласованности, независимость не является необходимым требованием для функционирующей аксиоматической системы — хотя обычно ее стремятся минимизировать количество аксиом в системе.
Аксиоматическая система называется полной , если для каждого утверждения либо оно само, либо его отрицание выводимо из аксиом системы (эквивалентно, каждое утверждение может быть доказано как истинное или ложное). [2]
Помимо согласованности, относительная согласованность также является признаком стоящей системы аксиом. Это описывает сценарий, в котором неопределенные термины первой системы аксиом предоставляются определениями из второй, так что аксиомы первой являются теоремами второй.
Хорошим примером является относительная согласованность абсолютной геометрии по отношению к теории системы действительных чисел . Линии и точки являются неопределенными терминами (также называемыми примитивными понятиями ) в абсолютной геометрии, но им приписаны значения в теории действительных чисел таким образом, что это согласуется с обеими системами аксиом. [ необходима цитата ]
Модель для аксиоматической системы — это четко определенный набор , который присваивает значение неопределенным терминам, представленным в системе, способом, который является правильным с отношениями, определенными в системе. Существование конкретной модели доказывает согласованность системы [ оспаривается — обсуждается ] . Модель называется конкретной, если присваиваемые значения являются объектами и отношениями из реального мира [ требуется разъяснение ] , в отличие от абстрактной модели , которая основана на других аксиоматических системах.
Модели также могут использоваться для демонстрации независимости аксиомы в системе. Построив допустимую модель для подсистемы без конкретной аксиомы, мы показываем, что опущенная аксиома независима, если ее правильность не обязательно следует из подсистемы.
Две модели называются изоморфными , если между их элементами можно найти однозначное соответствие таким образом, чтобы сохранить их взаимосвязь. [3] Аксиоматическая система, для которой каждая модель изоморфна другой, называется категоричной (иногда категоричной ). Свойство категоричности (категоричности) обеспечивает полноту системы, однако обратное неверно: полнота не гарантирует категоричности (категоричности) системы, поскольку две модели могут различаться по свойствам, которые не могут быть выражены семантикой системы .
В качестве примера рассмотрим следующую аксиоматическую систему, основанную на логике первого порядка с дополнительной семантикой следующих счетно-бесконечного числа добавленных аксиом (их можно легко формализовать в виде схемы аксиом ):
Неформально этот бесконечный набор аксиом утверждает, что существует бесконечно много различных элементов. Однако понятие бесконечного набора не может быть определено внутри системы — не говоря уже о мощности такого набора.
Система имеет по крайней мере две различные модели: одна — натуральные числа (изоморфные любому другому счетно бесконечному множеству), а другая — действительные числа (изоморфные любому другому множеству с мощностью континуума ). Фактически, она имеет бесконечное число моделей, по одной на каждую мощность бесконечного множества. Однако свойство, отличающее эти модели, — это их мощность — свойство, которое не может быть определено внутри системы. Таким образом, система не является категориальной. Однако можно показать, что она полна.
Формулировка определений и предложений таким образом, что каждый новый термин может быть формально устранен ранее введенными терминами, требует примитивных понятий (аксиом), чтобы избежать бесконечного регресса . Такой способ выполнения математики называется аксиоматическим методом . [4]
Распространенное отношение к аксиоматическому методу — логицизм . В своей книге Principia Mathematica Альфред Норт Уайтхед и Бертран Рассел попытались показать, что вся математическая теория может быть сведена к некоторому набору аксиом. В более общем смысле, сведение корпуса предложений к определенному набору аксиом лежит в основе исследовательской программы математика. Это было очень заметно в математике двадцатого века, в частности, в предметах, основанных на гомологической алгебре .
Экспликация конкретных аксиом, используемых в теории, может помочь прояснить подходящий уровень абстракции, с которым математик хотел бы работать. Например, математики решили, что кольца не обязательно должны быть коммутативными , что отличалось от первоначальной формулировки Эмми Нётер . Математики решили рассматривать топологические пространства в более общем плане без аксиомы разделения , которую изначально сформулировал Феликс Хаусдорф .
Теория множеств Цермело-Френкеля , результат аксиоматического метода, примененного к теории множеств, позволила «правильно» сформулировать проблемы теории множеств и помогла избежать парадоксов наивной теории множеств . Одной из таких проблем была гипотеза континуума . Теория множеств Цермело-Френкеля, с включенной исторически спорной аксиомой выбора , обычно сокращается как ZFC , где «C» означает «выбор». Многие авторы используют ZF для обозначения аксиом теории множеств Цермело-Френкеля с исключенной аксиомой выбора. [5] Сегодня ZFC является стандартной формой аксиоматической теории множеств и, как таковая, является наиболее распространенной основой математики .
Математические методы достигли определенной степени сложности в Древнем Египте, Вавилоне, Индии и Китае, по-видимому, без использования аксиоматического метода.
Евклид Александрийский является автором самого раннего сохранившегося аксиоматического представления евклидовой геометрии и теории чисел . Его идея начинается с пяти неоспоримых геометрических предположений, называемых аксиомами . Затем, используя эти аксиомы, он установил истинность других предложений с помощью доказательств , отсюда и аксиоматический метод. [6]
Многие аксиоматические системы были разработаны в девятнадцатом веке, включая неевклидову геометрию , основы вещественного анализа , теорию множеств Кантора , работу Фреге по основам и «новое» использование аксиоматического метода Гильбертом в качестве исследовательского инструмента. Например, теория групп была впервые поставлена на аксиоматическую основу ближе к концу того столетия. После того, как аксиомы были прояснены (например, что должны быть обратные элементы ), предмет мог продолжаться автономно, без ссылки на происхождение этих исследований в виде группы преобразований .
Не каждый последовательный корпус предложений может быть охвачен описываемым набором аксиом. В теории рекурсии набор аксиом называется рекурсивным, если компьютерная программа может распознать, является ли данное предложение в языке теоремой. Первая теорема Гёделя о неполноте затем говорит нам, что существуют определенные последовательные корпуса предложений без рекурсивной аксиоматизации. Обычно компьютер может распознавать аксиомы и логические правила для вывода теорем, и компьютер может распознавать, является ли доказательство действительным, но определить, существует ли доказательство для утверждения, можно только «ожидая», пока будет сгенерировано доказательство или опровержение. Результатом является то, что никто не будет знать, какие предложения являются теоремами, и аксиоматический метод перестает работать. Примером такого корпуса предложений является теория натуральных чисел , которая лишь частично аксиоматизирована аксиомами Пеано (описанными ниже).
На практике не каждое доказательство прослеживается до аксиом. Иногда даже не ясно, к какому набору аксиом апеллирует доказательство. Например, теоретико-числовое утверждение может быть выражено на языке арифметики (т. е. языке аксиом Пеано), и может быть дано доказательство, апеллирующее к топологии или комплексному анализу . Может быть не сразу ясно, можно ли найти другое доказательство, которое выводится исключительно из аксиом Пеано.
Любая более или менее произвольно выбранная система аксиом является основой некоторой математической теории, но такая произвольная аксиоматическая система не обязательно будет свободна от противоречий, и даже если это так, она вряд ли прольет свет на что-либо. Философы математики иногда утверждают, что математики выбирают аксиомы «произвольно», но возможно, что хотя они могут казаться произвольными, если рассматривать их только с точки зрения канонов дедуктивной логики, эта видимость обусловлена ограничением целей, которым служит дедуктивная логика.
Математическая система натуральных чисел 0, 1, 2, 3, 4, ... основана на аксиоматической системе, впервые разработанной математиком Джузеппе Пеано в 1889 году. Он выбрал аксиомы на языке одного унарного функционального символа S (сокращение от « преемник ») для множества натуральных чисел следующим образом:
В математике аксиоматизация — это процесс взятия совокупности знаний и работы в обратном направлении к ее аксиомам. Это формулировка системы утверждений (т. е. аксиом ), которые связывают ряд примитивных терминов — для того, чтобы из этих утверждений можно было дедуктивно вывести непротиворечивую совокупность утверждений . После этого доказательство любого утверждения должно, в принципе, прослеживаться до этих аксиом.
