Джузе́ппе Пеа́но — итальянский математик. Внёс вклад в математическую логику, аксиоматику, философию математики. Создатель вспомогательного искусственного языка латино-сине-флексионе. Более всего известен как автор стандартной аксиоматизации натуральной арифметики — арифметики Пеано.
Аксио́ма, или постула́т — исходное положение какой-либо теории, принимаемое в рамках данной теории истинным без требования доказательства и используемое при доказательстве других её положений, которые, в свою очередь, называются теоремами.
Логика первого порядка — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций и предикатов. Расширяет логику высказываний.
Выска́зывание в математической логике — предложение, выражающее суждение. Если суждение, составляющее содержание (смысл) некоторого высказывания, истинно, то и о данном высказывании говорят, что оно истинно. Сходным образом ложным называют такое высказывание, которое является выражением ложного суждения. Истинность и ложность называются логическими, или истинностными, значениями высказываний.
Ква́нтор — общее название для логических операций, ограничивающих область истинности какого-либо предиката и создающих высказывание. Чаще всего упоминают:
- Квантор всеобщности.
- Квантор существования.
- Квантор единственности.
Логика высказываний, пропозициональная логика или исчисление высказываний, также логика нулевого порядка — это раздел символической логики, изучающий сложные высказывания, образованные из простых, и их взаимоотношения. В отличие от логики предикатов, пропозициональная логика не рассматривает внутреннюю структуру простых высказываний, она лишь учитывает, с помощью каких союзов и в каком порядке простые высказывания сочленяются в сложные.
Мода́льная ло́гика — логика, в которой кроме стандартных логических связок, переменных и предикатов есть модальности.
Форма́льная систе́ма — результат строгой формализации теории, предполагающей полную абстракцию от смысла слов используемого языка, причём все условия, регулирующие употребление этих слов в теории, явно высказаны посредством аксиом и правил, позволяющих вывести одну фразу из других.
Перечисли́мое мно́жество — множество конструктивных объектов, все элементы которого могут быть получены с помощью некоторого алгоритма. Дополнение перечислимого множества называется корекурсивно перечислимым. Всякое перечислимое множество является арифметическим. Корекурсивно перечислимое множество может не быть перечислимым, но всегда является арифметическим. Перечислимые множества соответствуют уровню 
арифметической иерархии, а корекурсивно перечислимые — уровню 
Многозначная логика — это логика высказываний, в которой существует более двух истинностных значений логического выражения. Традиционно, в классической логике Аристотеля, мы имеем дело только с двумя возможными значениями — «истиной» или «ложью». Однако данная двухзначная логика может быть дополнена до n — значной с n > 2. Наиболее популярными в литературе являются трехзначная логика, конечнозначная и бесконечнозначная логики.
Алгоритмическая разрешимость — свойство формальной теории обладать алгоритмом, определяющим по данной формуле, выводима она из множества аксиом данной теории или нет. Теория называется разрешимой, если такой алгоритм существует, и неразрешимой, в противном случае. Вопрос о выводимости в формальной теории является частным, но вместе с тем важнейшим случаем более общей проблемы разрешимости.
Задача выполнимости формул в теориях — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для SMT-формул являются: теории целых и вещественных чисел, теории списков, массивов, битовых векторов и т. п.
Основа́ния матема́тики — система общих для всей математики понятий, концепций и методов, с помощью которых строятся различные её разделы.
Арифметическое множество — множество натуральных чисел 
, которое может быть определено формулой в языке арифметики первого порядка, то есть если существует такая формула 
с одной свободной переменной 
, что 
. Аналогично, множество кортежей натуральных чисел 
называется арифметическим, если существует такая формула 
, что 
. Также можно говорить об арифметических множествах кортежей натуральных чисел, конечных последовательностей натуральных чисел, формул и, вообще, об арифметических множествах любых объектов, кодируемых натуральными числами.
Общезна́чимость — свойство логической формулы, состоящее в том, что эта формула истинна при любой интерпретации входящих в неё нелогических символов, то есть предикатных и пропозициональных переменных. Логические формулы, обладающие этим свойством, называют общезначимыми, или тождественно истинными, или тавтологиями. Всякая общезначимая формула выражает логический закон. Вместо слов «формула A общезначима» часто пишут: 
.
Экзистенциальная теория вещественных чисел — это множество всех верных утверждений вида
Гипотеза об экспоненциальном времени — это недоказанное допущение о вычислительной сложности, которое сформулировали Импальяццо и Патури. Гипотеза утверждает, что 3-SAT не может быть решена за субэкспоненциальное время в худшем случае. Из верности гипотезы об экспоненциальном времени, если она верна, следовало бы, что P ≠ NP, но гипотеза является более сильным утверждением. Из утверждения гипотезы можно показать, что многие вычислительные задачи эквиваленты по сложности в том смысле, что если одна из них имеет алгоритм экспоненциального времени, то все они имеют алгоритмы такой же сложности.
Аксиоматика вещественных чисел Тарского — вариант системы оснований арифметики вещественных чисел, предложенный Альфредом Тарским в 1936 году.
