Импликативное пропозициональное исчисление

- пропозициональное исчисление, использующее единственную исходную связку [img: http://localhost:8080/file/021006-73.jpg] (импликацию). Примерами И. п. и. являются полное (или классическое) И. п. и., задаваемое аксиомами [img: http://localhost:8080/file/021006-74.jpg] и правилами вывода: модус поненс и подстановка, а также позитивное И. п. и., задаваемое аксиомами [img: http://localhost:8080/file/021006-75.jpg] и теми же правилами вывода. Всякая импликативная формула, т. е. формула, содержащая только связку [img: http://localhost:8080/file/021006-76.jpg] выводима в полном (или позитивном) И. п. и. тогда и только тогда, когда она выводима в классическом (соответственно интуиционистском) пропозициональном исчислении. Для любого конечного множества Vпеременных среди имплпкатпвных формул с переменными из Vсуществует лишь конечное число попарно не эквивалентных в позитивном И. п. и. (см. [3]). Существуют конечно аксиоматизируемые И. п. и. с неразрешимой проблемой выводимости (см. [4]).