Матема́тика — точная формальная наука, первоначально исследовавшая количественные отношения и пространственные формы. В более современном понимании, это наука об отношениях между объектами, о которых ничего не известно, кроме описывающих их некоторых свойств, — именно тех, которые в качестве аксиом положены в основание той или иной математической теории.
Метаязы́к — язык, предназначенный для описания другого языка, называемого объектным языком. Метаязык — язык лингвистики. Лингвистическая лексика, на основе которой формируются словари. Язык построения теории, слов, фраз в сфере грамматической лингвистики.
Ло́гика (др.-греч. λογική — «наука о правильном мышлении»; «способность к рассуждению»; от λόγος «учение, наука») — философская дисциплина и нормативная наука о законах, формах и приёмах интеллектуальной деятельности.
Андре́й Андре́евич Ма́рков — советский математик, сын известного русского математика А. А. Маркова, основоположник советской школы конструктивной математики.
Логици́зм, или логи́стика, или логистицизм — одно из основных направлений обоснования математики и философии математики, ставящее целью сведе́ние исходных математических понятий к понятиям логики. Двумя другими основными направлениями являются интуиционизм и формализм.
Фри́дрих Лю́двиг Го́тлоб Фре́ге — немецкий логик, математик и философ. Представитель школы аналитической философии.
Конструктивная математика — абстрактная наука о мыслительных конструктивных процессах, человеческой способности осуществлять их, и об их результатах — конструктивных математических объектах. Является результатом развития конструктивного направления в математике — математического мировоззрения, которое в отличие от теоретико-множественного направления считает основной задачей математики исследование конструктивных процессов и конструктивных объектов.
Лёйтзен Э́гберт Ян Бра́уэр — голландский философ и математик, выпускник университета Амстердама, работавший в таких областях математики, как топология, теория множеств, математическая логика, теория меры и комплексный анализ.
Ха́скелл Брукс Ка́рри — американский математик и логик.
Математическое доказательство — рассуждение с целью обоснования истинности какого-либо утверждения (теоремы), цепочка логических умозаключений, показывающая, что при условии истинности некоторого набора аксиом и правил вывода утверждение верно. В зависимости от контекста, может иметься в виду доказательство в рамках некоторой формальной системы или текст на естественном языке, по которому при необходимости можно восстановить формальное доказательство. Необходимость формального доказательства утверждений — одна из основных характерных черт математики как дедуктивной отрасли знаний, соответственно, понятие доказательства играет центральную роль в предмете математики, а наличие доказательств и их корректность определяют статус любых математических результатов.
Да́на Стю́арт Скотт — американский математик, известный работами в области математической логики и информатики.
Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках заданной математической теории.
Метаматематика — раздел математической логики, изучающий основания математики, структуру математических доказательств и математических теорий с помощью формальных методов. Термин «метаматематика» буквально означает «за пределами математики».
Ви́ктор Константи́нович Финн — советский и российский философ, учёный, доктор технических наук, заведующий отделением интеллектуальных систем РГГУ, член Диссертационного совета Д 002.073.05 по защите докторских диссертаций при ФИЦ ИУ РАН, член редколлегии журнала «Научно-техническая информация», член Научного совета Российской ассоциации искусственного интеллекта, член Международной ассоциации оснований науки, заслуженный деятель науки РФ.
Основа́ния матема́тики — система общих для всей математики понятий, концепций и методов, с помощью которых строятся различные её разделы.
Нельсон Гудмен — американский философ аналитической традиции, логик. Описал парадокс безобразного.
Пер Мартин-Лёф — шведский логик, статистик и философ. Член Шведской королевской академии наук.
Гомотопическая теория типов — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, высших категориях и типах в логике и языках программирования.
Тьерри Кокан — французский математик, специалист по теории типов и автоматическому доказательству, создатель исчисления конструкций, соорганизатор программы создания унивалентных оснований математики. Профессор факультета информатики и инженерии Гётеборгского университета.
Интуициони́зм — совокупность философских и математических взглядов, рассматривающих математические суждения с позиций «интуитивной убедительности». Различаются две трактовки интуиционизма: интуитивная убедительность, которая не связана с вопросом существования объектов, и наглядная умственная убедительность.