Опишем формальную теорию исчисления высказываний.
Исчисление высказываний – это формальная теория £, которой:
1. Алфавит:
- — буквы (A,B,…Z);
- — специальные символы ⌐ → ( ).
2. Формулы:
- любая буква A, B,…Z – формула;
- если А, В – формулы, то (А), (⌐А), (А→ В) – формулы.
3. Аксиомы:
1. А1:
2. А2:
3. А3:
Выражения А1-А3 называются схемами аксиом, т. к. каждая из них порождает бесконечное множество формул. Вместо А, В и С можно подставлять любые формулы.
4. Правило вывода: правило modus ponens (m.p.):
A и B- любые формулы. Т. о. множество аксиом теории £ — бесконечно. Множество правил вывода также бесконечно.