53. Сколько различных формул соответствует каждой из схем аксиом

Каковы бы ни были формулы  , следующие формулы называют аксиомами исчисления высказываний:

	( 1)
			( 2)

	( 3)
		( 4)

			( 5)
	( 6)

	( 7)
				( 8)

	( 9)
			( 10)

	( 11)

Как говорят, мы имеем здесь одиннадцать "схем аксиом"; из каждой схемы можно получить различные конкретные аксиомы, заменяя входящие в нее буквы на пропозициональные формулы.

Единственным правилом вывода исчисления высказываний является правило со средневековым названием "modus ponens" (MP). Это правило разрешает получить (вывести) из формул   и   формулу  .

Выводом в исчислении высказываний называется конечная последовательность формул, каждая из которых есть аксиома или получается из предыдущих по правилу modus ponens.

Вот пример вывода (в нем первая формула является частным случаем схемы (1), вторая — схемы (2), а последняя получается из двух предыдущих по правилу modus ponens):

Пропозициональная формула   называется выводимой в исчислении высказываний, или теоремой исчисления высказываний, если существует вывод, в котором последняя формула равна  . Такой вывод называют выводом формулы  . (В принципе можно было бы и не требовать, чтобы формула   была последней — все дальнейшие формулы можно просто вычеркнуть.)

Как мы уже говорили, в исчислении высказываний выводятся все тавтологии и только они. Обычно это утверждение разбивают на две части: простую и сложную.

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

55. В каком случае логическое исчисление является непротиворечивым

Формула называется тождественно истинной, или

тавтологией (тождественно ложной, или противоречием), если она

обращается в истинное (ложное) высказывание при всех наборах

значений переменных. Обозначение тавтологии: »= F(XX, X2, ..., Хп).

Формула называется общезначимой (или тавтологией), если она истинна в любой интерпретации. Формула называется противоречивой, если она ложна в любой интерпретации.

Формула G называется логическим следствием множества формул Г, если G выполняется в любой модели Г.

Формальная теория   называется семантически  непротиворечивой, если ни одна её теорема не является противоречием. Таким образом, формальная теория пригодна для описания тех множеств (алгебраических систем), которые являются её моделями. Модель для формальной теории   существует тогда и только тогда, когда   семантически непротиворечива.

Формальная теория   называется формально непротиворечивой, если в ней не являются выводимыми одновременно формулы F и не F . Теория   формально непротиворечива тогда и только тогда, когда она семантически непротиворечива.