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

Как уже известно, формальная аксиоматическая теория B считается за-

данной, если:

1. Задано некоторое множество символов - алфавит теории B. Конечная

последовательность букв алфавита называется выражением теории.

Алфавит, следовательно, и выражения теории, задаются эффективным

образом.

2. Заданы формулы теории B как некоторое подмножество выражений

теории. Формулы тоже обычно задаются эффективным образом.

3. Заданы аксиомы теории B как подмножество множества формул. Если

аксиом конечное число, то их можно задать перечислением. Если же их

беско-нечное множество, то задают с помощью схем, т.е. правил построения

аксиом. Если аксиомы заданы эффективным образом, то теория B

называется эффек-тивно аксиоматизированной.

4. Задано конечное число правил вывода R1, R2,..., Rn, согласно каждому из

которых некоторая формула, именуемая непосредственным следствием (за-

ключением), непосредственно выводима из некоторого конечного множества

формул, называемых посылками. При этом для каждого Ri существует целое

положительное k такое, что для каждого множества, состоящего из k формул

и для каждой формулы А эффективно решается вопрос о том, является ли А

не-посредственным следствием данных k формул по правилу Ri.

Выводом в B называется всякая последовательность A1, A2,..., An формул,

такая, что для каждого i (1≤ i ≤ n) формула Ai есть либо аксиома теории B,

либо непосредственное следствие каких-либо предыдущих формул этой

последова-тельности по одному из правил вывода.

Формула А теории B называется теоремой теории B если существует вы-вод

в B, в котором последней формулой является A, такой вывод называется

выводом формулы А.

Формула А называется следствием в B множества формул G тогда и только

тогда, когда существует такая последовательность формул A1, A2,..., An, что

An=A и для любого i Ai есть либо аксиома, либо элемент G, либо непосред-

ственное следствие некоторых предыдущих формул этой

последовательности по одному из правил вывода. Такая последовательность

называется выводом А из G. Элементы G называются гипотезами или

посылками вывода. Для сокра-щения утверждения «А есть следствие G»

будем употреблять запись: G├ A. Например, если G={B1, B2,...Bm}, то будем

писать

B1, B2,..., Bm ├ A.

Нетрудно видеть, что если G есть пустое множество, т. е. G =∅ то ∅ ├ A

имеет место тогда и только тогда, когда А является теоремой. Вместо ∅ ├ А

принято писать просто

├ А,

что читается: «формула А является теоремой».

Чтобы избежать путаницы там, где будут рассматриваться не одна, а не-

сколько теорий, употребляют запись

G ├ A и ├ А B B указывая индексом B на то, о какой теории идет речь.