Исчисление высказываний

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

Исчисление высказываний есть формальная теория Т, в которой заданы:

•алфавит А:

связки ¬ (или ¯), →; (дополнительно
можно ввестиdef связки или Λ: def
A B A B,	A B A B);

(, ) – служебные символы, позволяющие определить порядок выполнения связок;

D, B, …, A1, B1, … - переменные высказывания;

•формулы F:
переменные есть формулы;
							А В	-
						А	А В
если А, В – формулы, то							и
формулы;
•аксиомы Р:
Р1: (А (В А));
Р2 : ((А (В С)) ((А В) (А С)));
Р3 : ((	В	А	) ((	В	А) В));	А, А В
•правило modus ponens (mp):								-
•правило modus ponens (mp):							В	-
							В

правило заключения (от лат. modus – способ; ponens – отделение, заключение).

Составное	высказывание	В	является
логическим	следствием		составных

высказываний А1, А2, …, Аn, если при всех значениях элементарных высказываний, при которых все А1, А2, …, Аn истинны (в любой

интерпретации),	будет	истинным		и
высказывание В.
Символическая	запись		логического
следования В из	А1, А2, …, Аn		имеет	вид
А1, А2, …, ├Аn	В и читается		так:	«Если

(выполнены) А1, А2, …, Аn, то (выполнено) В».

Аксиомы теории L

Аксиомами теории L назовают всякие формулы, которые порождают нижеследующие формульные схемы при любом выборе формул А, В, С: Каждая из схем (1) — (13) порождает счетное множество аксиом, если символы А, В, С заменять конкретными формулами.

Поэтому (1) — (13) называют аксиомными схемами (АС).