Формальная аксиоматическая теория
Доказательство Д2).
Пусть
содержит 0 пропозициональных связок. Тогда
- пропозициональная буква А, а утверждение 2) сводится к
.
Пусть утверждение 2) верно для любой формулы, содержащей не более n пропозициональных связок. Пусть формула
содержит n+1 пропозициональную связку. Тогда возможны три варианта представления формулы
: 1)
, 2)
, 3)
, причем
и
содержат не более n пропозициональных связок.
1). 
2) 
3) 
Формальная (аксиоматическая) теория
считается определенной, если:
(1). Задано счетное множество символов. Конечные цепочки символов - выражения (слова) теории
.
(2). Выделено подмножество выражений теории
, называемых формулами
.
(3). Выделено некоторое подмножество формул
, называемых аксиомами теории
.
(4). Задано конечное множество R1, ..., Rn отношений между формулами, называемых правилами вывода.
- Правила вывода позволяет установить «непосредственное следствие» некой формулы из конечного (определенного отношением) набора указанных формул.
- Выводом в
называется такая конечная цепочка формул, что всякая формула этой цепочки либо является аксиомой, либо «непосредственно следует» из предыдущих формул по одному из правил вывода. - Формула
называется теоремой теории
, если существует вывод в
, в котором
является последней формулой цепочки. - Теория
называется эффективно аксиоматизированной, если существует процедура, указывающая, является ли данная формула аксиомой. - Теория
называется разрешимой, если существует алгоритм, который по формуле определяет, существует или нет ее вывод в
. - Формула
называется следствием множества формул Г в
(обозначается
) тогда и только тогда, когда существует такая последовательность формул
, что
есть
, и каждая формула этой последовательности либо есть аксиома, либо элемент Г, либо является непосредственным следствием некоторых предыдущих формул по одному из правил вывода. - В частности,
означает, что
есть теорема теории
.
Доказать:
0 Если
и
, то
.
1
тогда и только тогда, когда в Г существует конечное подмножество
, для которого
.
2 Если
и
для любого
из множества
, то
.