Ценность всякой формальной теории в конечном счете определяется ее способностью описывать какие-то объекты и связи между ними. Поэтому один из первых для любой теории вопросов – это вопрос о том, для описания каких объектов пригодна эта теория.
Рассмотрим эту проблему как математическую задачу о соответствии между содержательно построенной теорией, рассматриваемой как множество объектов с операциями и отношениями на нем, и множеством высказываний об этой теории, построенном как формальное исчисление.
Интерпретация формальной теории состоит из множества М и однозначного отображения, которое каждой предикатной букве ставит в соответствие n -местное отношение на М, каждой функциональной букве – n -местную операцию на М, каждой предметной константе – элемент М.
Всякая замкнутая, т.е не содержащая свободных переменных, формула теории представляет собой высказывание об элементах, отношениях и функциях М, которое может быть истинным или ложным. Значения истинности составных формул вычисляются в соответствии с входящими в них логическими операциями.
Открытая формула соответствует некоторому отношению на М, при подстановке предметных констант она превращается в высказывание о том, что между элементами М, соответствующим подставленным константам, выполняется данное отношение.
Открытая формула называется выполнимой в данной интерпретации, если существует такая подстановка предметных констант, при которых она превращается в истинное высказывание. Формула называется истинной в данной интерпретации, если она выполняется при любой подстановке констант. Формула называется ложной в данной интерпретации, если она невыполнима.
Интерпретация называется моделью для множества формул Г, если любая формула Г истинна в данной интерпретации. Интерпретация называется моделью теории Т, если она является моделью множества всех теорем теории Т, т.е. если всякая формула доказуемая в теории Т истинна в данной интерпретации.
О формальных свойствах исчисления, его формул и формальных преобразований над ними принято говорить как о синтаксисе исчисления. Свойства исчисления, описанные в терминах его интерпретаций – это семантика исчисления.
Формула называется общезначимой, если она истинна в любой интерпретации, и противоречивой, если она ложна в любой интерпретации.
Для любого множества общезначимых формул любая алгебраическая система и вообще любое множество является моделью. Напротив, для любого множества формул, содержащего хотя бы одну противоречивую формулу, моделей не существует.
Введенное определение противоречивой формулы является семан-тическим, т.е. связывающим непротиворечивость с истинностью. Исходя из него сформулируем следующее понятие: теория семантически непротиворечива, если ни одна из ее теорем не является непротиворечивой, т.е. ложной в любой интерпретации.
С помощью введенных понятий ответ на вопрос о пригодности теории формулируется следующим образом: теория Т пригодна для описания тех множеств, которые являются ее моделями. Такой критерий пригодности теорий по существу известен уже давно; отыскание модели для теории до возникновения оснований математики было единственным общепризнанным методом доказательства законности теории. В основаниях математики сформулирован аналог этого критерия в терминах самих формальных теорий. Этим аналогом является понятие формальной непротиворечивости.
Теория Т называется формально непротиворечивой, если не существует формулы F, такой, что F и F являются теоремами теории Т, т.е. что в теории Т не выводимы одновременно F и ее отрицание.
Теорема. Множество формул формально непротиворечиво, если и только если оно семантически непротиворечиво.
Т.о. понятие формальной непротиворечивости оказывается экви-валентным более привычному в математике понятию семантической непротиворечивости; однако оно сформулировано в синтаксических терминах и с конструктивной точки зрения более надежно (ведь именно семантические трудности - парадоксы- и привели к возникновению оснований математики и концепциям формального подхода).
Законность неэвклидовых геометрий Лобачевского-Боайи обосновывалась именно отсутствием в них противоречий – аргумент, который по существу совпадает с современным понятием формальной непротиворечивости. Геометрические модели для этих теорий, доказывающие их семантическую непротиворечивость, были найдены позднее.
Пусть имеется с одной стороны содержательная теория S, сформулированная в семантических терминах, с другой стороны – формальная теория Т. В каких случаях можно утверждать, что Т является удовлетворительной формализацией S?
Очевидно, что необходимым условием является утверждение, что S является моделью теории, т.е. чтобы существовало отображение, при котором всякая теорема из Т отображается в истинное высказывание из S. Однако этого условия явно недостаточно, иначе для формализации любой теории хватило бы чистого исчисления предикатов: ведь для него любое множество является моделью. Исчерпывающей формализацией S будет служить такая Т, для которой выполняется и обратное соответствие: каждое истинное высказывание S отображается в некоторую теорему Т. Теория Т с таким свойством называется полно относительно S, или адекватной S.
Если для семантической теории удается построить непротиворечивую и полную формальную теорию Т, то S называют аксиоматизируемой, или формализуемой, теорией.
Еще одна важная характеристика формальной теории это ее разрешимость. Формальная теория Т называется разрешимой, если существует алгоритм, который для любой формулы языка определяет, является ли она теоремой в Т или нет, иначе говоря, если предикат "быть теоремой в теории Т " общерекурсивен.