Формальная аксиоматическая теория

Доказательство Д2).

Пусть содержит 0 пропозициональных связок. Тогда - пропозициональная буква А, а утверждение 2) сводится к .

Пусть утверждение 2) верно для любой формулы, содержащей не более n пропозициональных связок. Пусть формула содержит n+1 пропозициональную связку. Тогда возможны три варианта представления формулы : 1) , 2) , 3) , причем и содержат не более n пропозициональных связок.

1).

2)

3)

 

Формальная (аксиоматическая) теория считается определенной, если:

(1). Задано счетное множество символов. Конечные цепочки символов - выражения (слова) теории .

(2). Выделено подмножество выражений теории , называемых формулами .

(3). Выделено некоторое подмножество формул , называемых аксиомами теории .

(4). Задано конечное множество R1, ..., Rn отношений между формулами, называемых правилами вывода.

 

  • Правила вывода позволяет установить «непосредственное следствие» некой формулы из конечного (определенного отношением) набора указанных формул.
  • Выводом в называется такая конечная цепочка формул, что всякая формула этой цепочки либо является аксиомой, либо «непосредственно следует» из предыдущих формул по одному из правил вывода.
  • Формула называется теоремой теории , если существует вывод в , в котором является последней формулой цепочки.
  • Теория называется эффективно аксиоматизированной, если существует процедура, указывающая, является ли данная формула аксиомой.
  • Теория называется разрешимой, если существует алгоритм, который по формуле определяет, существует или нет ее вывод в .
  • Формула называется следствием множества формул Г в (обозначается ) тогда и только тогда, когда существует такая последовательность формул , что есть , и каждая формула этой последовательности либо есть аксиома, либо элемент Г, либо является непосредственным следствием некоторых предыдущих формул по одному из правил вывода.
  • В частности, означает, что есть теорема теории .

 

Доказать:

0 Если и , то .

1 тогда и только тогда, когда в Г существует конечное подмножество , для которого .

2 Если и для любого из множества , то .