Как любая формальная теория, ИВ основывается на определении формальной системы (16):

, (16)

где Т – алфавит системы; Р – синтаксические правила; А – система аксиом; Ð – семантические правила.

Алфавит ИВ:

·  переменные высказываний (пропозициональные буквы) А, В, С…;

·  знаки логических связок {∧ или & – «и», ∨– «или», → – «если…то…», или черта над формулой – «не»};

·  скобки (, ).

Формулы:

·  переменное высказывание есть формула;

·  если Ø и Ù – формулы, то (Ø∨Ù),(Ø&Ù), (Ø→Ù) и Ø – формулы;

·  других формул нет.

Аксиомы. Возможны различные системы аксиом, порождающие одно и то же множество формул. Одна из них (10 штук) непосредственно использует все логические связки. Другая использует только две связки и →; операции & – «и», ∨ – «или» рассматриваются только как сокращения, а именно А∨В = А→В; А&В = (А→В). Тогда аксиом всего три:

А→(В→А);

(А→(В→С) →(А→В) → (А→С);

(А→В) →((А→ В) →А).

Правила вывода.

·  Правило подстановки: если Ø – выводимая формула, содержащая букву А (обозначим этот факт Ø(А)), то выводима формула Ø(Ù), которая получается из Ø заменой всех вхождений А на произвольную формулу, т. е.

Ù; Ø(А)

;

Ø(Ù)

·  Правило заключения (modus ponens): если Ø и Ø→Ù – выводимые формулы, то Ù выводима, т. е.

Ø; Ø→Ù

-.

Ù

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

В математической логике показывается, что ИВ выполняет задачу порождения общелогических закономерностей – тождественно-истинностных высказываний. С точки зрения теории алгоритмов множество всех истинных высказываний ИВ перечислимо и разрешимо.

Область применения ИВ – анализ и синтез конечных автоматов, которые, как известно, являются логической основой компьютеров.

Однако существенным недостатком аппарата ИВ является ограниченность выразительных средств, что не позволяет описывать логические задачи и дедуктивные рассуждения всех типов, в частности, силлогистические умозаключения. Естественным развитием аппарата ИВ является исчисление предикатов (ИП), разработанное в рамках логики предикатов (ЛП).

Первая теорема Гёделя о неполноте

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

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

Теорема была доказана Куртом Гёделем в 1931 году.

Вторая теорема Гёделя о неполноте

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

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

Эта теорема имеет широкие последствия как для математики, так и для философии, в частности, для онтологии и философии науки.

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

Доказательство теоремы Тарского опирается на гёделевскую нумерацию.