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