При изучении формальных теорий мы имеем дело с двумя типами высказываний. Во-первых, с высказываниями самой теории (теоремами), которые рассматриваются как чисто формальные объекты, определенные ранее, а во-вторых, с высказываниями о теории (о свойствах ее теорем, доказательств и т.д.), которые формулируются на языке, внешнем по отношению к теории, — метаязыке и называются метатеоремами. Различие между теоремами и метатеоремами не всегда будет проводиться явно, но его обязательно надо иметь в виду.
Интерпретацией формальной теории Т в область интерпретации M называется функция I : Á ® M, которая каждой формуле формальной теории Т однозначно сопоставляет некоторое содержательное высказывание относительно объектов множества (алгебраической системы) M. Это высказывание может быть истинным или ложным (или не иметь истинностного значения). Если соответствующее высказывание является истинным, то говорят, что формула выполняется в М.
Интерпретация I называется моделью множества формул G, если все формулы этого множества выполняются в интерпретации I. Интерпретация I называется моделью формальной теории Т, если все теоремы этой теории выполняются в интерпретации I (то есть все выводимые формулы оказываются истинными в данной интерпретации).
Непротиворечивость. Напомним, что формула называется противоречивой, если она ложна в любой интерпретации. Такое определение противоречивой формулы является семантическим, т.е. связывающим непротиворечивость с истинностью. Исходя из него, можно сформулировать понятие семантически непротиворечивой теории:
Формальная теория Т называется семантически непротиворечивой, если ни одна ее теорема не является противоречием. Таким образом, формальная теория пригодна для описания тех множеств (алгебраических систем), которые являются ее моделями. Модель для формальной теории Т существует тогда и только тогда, когда Т семантически непротиворечива.
Формальная теория Т называется формально непротиворечивой, если в ней не являются выводимыми одновременно формулы F и ØF. Теория Т формально непротиворечива тогда и только тогда, когда она семантически непротиворечива.
С помощью введенных понятий можно сформулировать следующий тезис, что теория Т пригодна для описания тех множеств, которые являются ее моделями. Модель для теории Т существует тогда и только тогда, когда Т семантически непротиворечива. Чисто логические теории – исчисление высказываний и исчисление предикатов пригодны для описания любых множеств, что соответствует общенаучному принципу универсальности законов логики. Лейбниц формулировал его как выполнимость логических законов во всех «мыслимых мирах». Аналогом этого критерия, сформулированным в терминах самих формальных теорий без привлечения семантических понятий, является формальная или дедуктивная непротиворечивость.