Формальные аксиоматические теории
Формальная теория представляет собой множество чисто абстрактных объектов (не связанных с внешним миром), в которой представлены 
правила оперирования множеством символов в чисто синтаксической трактовке без учета смыслового содержания (или семантики).
Формальную теорию иногда называют аксиоматикой или формальной аксиоматической теорией. Родоначальником аксиоматических теорией можно считать "Начала" Евклида.
Определение. Формальная теория T считается определенной, если:
1) задано некоторое счетное множество символов - символов теории T; конечные последовательности символов теории T называются выражениями теории T;
2) имеется подмножество выражений теории T, называемых формулами теории T;
3) выделено некоторое множество формул, называемых аксиомами теории T;
4) имеется конечное множество R1, R2, …, Rm отношений между формулами, называемых правилами вывода. Правила вывода позволяют получать из некоторого конечного множества формул другое множество формул.
Обычно для формальной теории имеется алгоритм, позволяющий по данному выражению определить, является ли оно формулой. Точно также, чаще всего существует алгоритм, выясняющий, является ли данная формула теории T аксиомой; в таком случае T называется эффективно аксиоматизированной теорией.
Определение.Если формула A и формулы A1, A2,…, Aj находятся в некотором отношении Ri, то A называют непосредственным следствием из формул A1, A2,…, Aj, полученных по правилу Ri.
Выводом в теории T называется всякая последовательность A1, A2,…, An формул такая, что для любого i формула Ai есть либо аксиома теории T, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода.
Формула A называется теоремой теории T, если в ней существует вывод, в котором последней формулой является A. Этот вывод называется выводом (доказательством) формулы A. Иными словами, теоремы аксиоматической теории - это формулы, которые могут выведены (доказаны) по определенным правилам.
Отметим, что в соотношении {теоремы}Ì{формулы}Ì{выражения}
включение множеств является строгим.
Определение. Формула A называется следствием множества формул G в теории T тогда и только тогда, когда существует такая последовательность формул A1, A2,…, An, что An есть A, и для любого i формула Ai есть либо аксиома, либо элемент G, либо непосредственное следствие некоторых предыдущих формул по одному из правил вывода. Такая последовательность называется выводом A из G. Элементы G называются гипотезами или посылками вывода.
Для сокращения утверждения "A есть следствие G" употребляется запись G |― A. Если множество G конечно: G = {B1, B2,..., Bn}, то вместо {B1,B2,..., Bn}|―A пишут B1, B2,..., Bn|―A. Если G есть пустое множество Æ, то G|―A имеет место тогда и только тогда, когда A является теоремой и в этом случае используют сокращенную запись |―A ("A есть теорема").
Приведем несколько простых свойств понятия выводимости из посылок.
1. Если GÍ S и G |― A, то S |― A.
Это свойство выражает тот факт, что если A выводимо из множества посылок G, то оно остается выводимым, если мы добавим к G новые посылки.
2. G|―A тогда и только тогда, когда в G существует конечное подмножество S, для которого S |― A.
Часть "тогда" утверждения 2 вытекает из утверждения 1. Часть "только тогда" этого утверждения очевидно, поскольку всякий вывод A из G использует лишь конечное число посылок из G.
3. Если S |― A и G |― B для любого B из множества S, то G |― A.
Смысл этого утверждения прост: если A выводимо из S и любая формула из S выводима из G, то A выводима из G.
Первым вопросом, который возникает при задании формальной теории, является вопрос о том, возможно ли, рассматривая какую-нибудь формулу формальной теории, определить является ли она доказуемой или нет. Другими словами, речь идет о том, чтобы определить, является ли данная формула теоремой или не-теоремой и как это доказать. В математике предполагается, что при задании формальной теории существует алгоритм, который позволит получить ответ на данный вопрос. Такой алгоритм, если он существует, называется процедурой решения, а соответствующую теорию называют разрешимой. Однако даже такие простые и фундаментальные теории, как исчисление предикатов (см. §3), являются неразрешимыми. Причина этого состоит в следующем. Даже если применить правила словообразования (т. е. правила построения формул, правила вывода) последовательно ко всем возможным объектам формальной теории и формальная теория такова, что имеется принципиальная возможность полного перечисления ее теорем (даже при бесконечном их числе), то все же не существует никакого подходящего способа в общем случае, чтобы перечислить все не-теоремы.
Формальные теории являются не просто игрой ума, а всегда представляют собой модель какой-то реальности (либо конкретной, либо математической). Вначале математик изучает реальность, конструируя некоторое абстрактное представление о ней, т. е. некоторую формальную теорию. Затем он доказывает теоремы этой формальной теории. Вся польза и удобство формальных теорий как раз и заключается в их абстрагировании от конкретной реальности. Благодаря этому одна и та же формальная теория может служить моделью многочисленных различных конкретных ситуаций. Наконец, он возвращается к исходной точке всего построения и дает интерпретацию теорем, полученных при формализации.