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