Логические доказательства, Сергей Попов und Наталья Брошкова

Исследуются секвенциальные пропозициональные выводы. Для этого вводится оригинальный механизм диаграмм выводов, представляющие собой нагруженные графы произвольной структуры, и описывающие классы выводов. Отношение эквивалентности выводов, как изоморфизма канонических диаграмм, совпадает с традиционной эквивалентностью, определяемой эквивалентными преобразованиями выводов. Диаграммы позволяют решить ряд задач исследования выводов: определить нелокальные преобразования, соответствующих устранению сечений, без собственно их устранения; описать формулы сечения, не выводящие выводы из класса эквивалентности, и т.п. Сформулирован класс локальных секвенций, характеризующихся простыми доказательствами. С другой стороны описаны классы сложно выводимых секвенций. При этом если аргументом функции сложности выступает число переменных, из которых построены секвенция, то почти все выводы сложные. Но если выступает длина секвенции, то удалось построить только одну последовательность нелокальных...