Системы натурального вывода для некоторых логик с истинностными провалами и логик с пресыщенными оценками

Аннотация

В статье мы представляем системы натурального вывода в стиле Фитча для некоторых логик с пресыщенными оценками и истинностными провалами. Мы показываем, что системы натурального вывода рассматриваемых логик могут быть заданы с различными формулировками либо правила исключения дизъюнкции, либо правила введения отрицания. Мы даем конструктивное доказательство того, что для каждой естественной системы выводов N логики $\alpha$ формула A доказуема в N тогда и только тогда, когда A является $\alpha$-теоремой.