Интерактивные реализации логических формул

Рассматривается новое конструктивное понимание логических формул, согласованное с интуицией и с традиционными средствами конструктивного логического вывода. Новое понимание логически проще традиционной реализуемости (в смысле кванторной глубины), но является также естественным с точки зрения алгоритмического решения задач. Это понимание, кроме свидетельства (реализации, подтверждения) понимаемой формулы, привлекает понятия теста (противодействия, препятствия) этой реализации на данной формуле. Для понимания формулы $A$ рассматриваются предложения вида $a:A:b$. Это предложение означает, что объект $a$ (выдвигаемый в подтверждение формулы $A$) выигрывает у объекта $b$ (который противодействует выполнению формулы $A$) формулу $A$ в процессе осуществления специальной процедуры сопоставления этих объектов друг с другом и с данной формулой. Данная процедура может считаться некоторой процедурой арбитража для вынесения необходимого решения. Базис процедуры арбитража для атомарных формул задается интерпретацией языка. Процедура для сложных предложений задается специальными правилами определения смысла логических связок. При наиболее естественном определении процедура арбитража имеет полиномиальную временную сложность. Формула $A$ считается истинной в новом смысле этого слова, если имеется подтверждение, выигрывающее ее у всех возможных противодействий. Рассматривается логический язык без отрицаний. Доказана теорема о корректности в новом смысле традиционных интуиционистских аксиом и правил вывода. При этом рассматривается секвенциальное логическое исчисление, ориентированное на обратный метод поиска вывода.