Правила вывода

1. Правило подстановки: Если формула A доказуема в исчислении высказываний, x – переменная, B – произвольная формула исчисления высказываний (и.в.), то формула, полученная в результате замены в формуле A переменной x формулой B, является также доказуемой формулой. Операция замены в формуле A переменной x формулой B называется подстановкой и обозначается .

2. Правило заключения: Если формулы A и A→B доказуемы в исчислении высказываний, то формула B также доказуема.

3. Определение доказуемой формулы:

· Всякая аксиома является доказуемой формулой;

· Формула, полученная из доказуемой формулы путем применения подстановки вместо переменной x произвольной формулы B есть доказуемая формула;

· Формула B, полученная из доказуемых формул A и A→B путем применения правил заключения, есть доказуемая формула;

· Никакая другая формула исчисления высказываний не является доказуемой.

Процесс получения доказуемых формул называется доказательством.