Джузе́ппе Пеа́но — итальянский математик. Внёс вклад в математическую логику, аксиоматику, философию математики. Создатель вспомогательного искусственного языка латино-сине-флексионе. Более всего известен как автор стандартной аксиоматизации натуральной арифметики — арифметики Пеано.
Аксио́ма, или постула́т — исходное положение какой-либо теории, принимаемое в рамках данной теории истинным без требования доказательства и используемое при доказательстве других её положений, которые, в свою очередь, называются теоремами.
Курт Фри́дрих Гёдель — австрийский логик, математик и философ математики. Наиболее известен сформулированными и доказанными им теоремами о неполноте, которые оказали огромное влияние на представление об основаниях математики. Считается одним из наиболее выдающихся мыслителей XX века.
Теорема Гёделя о неполноте и вторая теорема Гёделя — две теоремы математической логики о принципиальных ограничениях формальной арифметики и, как следствие, всякой формальной системы, в которой можно определить основные арифметические понятия: натуральные числа, 0, 1, сложение и умножение.
Недоказу́емые утвержде́ния в какой-либо теории — утверждения, которые нельзя ни доказать, ни опровергнуть в рамках этой теории. Теорема Гёделя о неполноте говорит, что в каждой достаточно сложной непротиворечивой теории, включающей в себя формальную арифметику, имеется недоказуемое [и неопровергаемое в ней] утверждение. Однако нахождение достаточно простых утверждений такого рода и доказательство их недоказуемости — сложная задача.
Аксио́мы Пеа́но — одна из систем аксиом для натуральных чисел, введённая в 1889 году итальянским математиком Джузеппе Пеано.
Непротиворечи́вость — свойство формальной системы, заключающееся в невыводимости из неё противоречия. Если отрицание какого-то предложения из системы может быть доказано в теории, то о самом предложении говорится, что оно опровержимо в ней. Непротиворечивость системы означает, что никакое предложение не может быть в ней и доказано, и вместе с тем опровергнуто. Требование непротиворечивости является обязательным требованием к научной и, в частности, логической теории. Противоречивая система заведомо несовершенна: наряду с истинными положениями она включает также ложные; в ней что-то одновременно и доказывается, и опровергается. Во многих системах имеет место закон Дунса Скота. В этих условиях доказуемость противоречия означает, что становится доказуемым.
Форма́льная систе́ма — результат строгой формализации теории, предполагающей полную абстракцию от смысла слов используемого языка, причём все условия, регулирующие употребление этих слов в теории, явно высказаны посредством аксиом и правил, позволяющих вывести одну фразу из других.
Математическое доказательство — рассуждение с целью обоснования истинности какого-либо утверждения (теоремы), цепочка логических умозаключений, показывающая, что при условии истинности некоторого набора аксиом и правил вывода утверждение верно. В зависимости от контекста, может иметься в виду доказательство в рамках некоторой формальной системы или текст на естественном языке, по которому при необходимости можно восстановить формальное доказательство. Необходимость формального доказательства утверждений — одна из основных характерных черт математики как дедуктивной отрасли знаний, соответственно, понятие доказательства играет центральную роль в предмете математики, а наличие доказательств и их корректность определяют статус любых математических результатов.
Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках заданной математической теории.
Метаматематика — раздел математической логики, изучающий основания математики, структуру математических доказательств и математических теорий с помощью формальных методов. Термин «метаматематика» буквально означает «за пределами математики».
Теорема Лёба — теорема в математической логике о взаимосвязи между доказуемостью утверждения и самим утверждением. Установлена математиком Мартином Хуго Лёбом в 1955 году.
Основа́ния матема́тики — система общих для всей математики понятий, концепций и методов, с помощью которых строятся различные её разделы.
Вильге́льм Фри́дрих Аккерман — немецкий математик и логик, педагог.
Principia Mathematica — трёхтомный труд по логике и философии математики Альфреда Норта Уайтхеда и Бертрана Рассела, выпущенный в 1910, 1912 и 1913 годах. Монография написана на английском языке, но название дано на латыни. Название переводилось на русский как «Принципы математики», «Начала математики» и «Основания математики».
Джеффри (Джефф) Брюс Парис — британский математик, преподаватель в Манчестерском университете.
Лео Энтони Харрингтон — американский математик, профессор Калифорнийского университета в Беркли, специалист по теориям вычислимости, моделей и множеств.
- В 1977 году совместно с Джеффом Парисом опубликовал доказательство теоремы Париса–Харрингтона.
- Харрингтон доказал, что аксиома детерминации точна для всех аналитических множеств, то есть существует для каждого числа.
- Харрингтон и Сахарон Шелах показали, что теория упорядочения рекурсивно перечисляемых степеней неразрешимости.
Метатеорема — логическое утверждение о формальной системе, доказанное на метаязыке. В отличие от теорем, доказанных в рамках данной формальной системы, метатеорема доказывается в рамках метатеории и может ссылаться на понятия, которые присутствуют в метатеории, но не в теории объектов.
