V Пример. Обоснуем также и то, что теоремой является и другая формула закона введения отрицания: (pÉq)É((pÉØq)ÉØp)

Обоснуем также и то, что теоремой является и другая формула закона введения отрицания: (pÉq)É((pÉØq)ÉØp). При этом получим схему вывода:

Эвристики натурального исчисления высказываний

Построение выводов и доказательств является творческой задачей, например, при поиске посылок в доказательстве при условии, что хотя в качестве посылок можно брать любые формулы, но в ходе вывода все они должны быть исключены. Выбор нужных для вывода посылок может быть случайным и иметь характер простого перебора различных возможностей. Во избежание последнего в логике были выработаны и применяются особые методологические приёмы эвристики, позволяющие предельно сократить число переборов. Натуральное исчисление высказываний опирается на 3-и основных эвристики. 1-я эвристика применяется тогда, когда являющаяся целью вывода формула импликативна; в таком случае антецедент этой формулы берётся в качестве дополнительной посылки, а целью выведения становится консеквент формулы.