Proof Search on Bilateralist Judgments over Non-deterministic Semantics

TL;DR

This paper develops a two-dimensional semantic framework for bilateralist judgments in non-deterministic logics and introduces a proof-search algorithm with complexity bounds.

Contribution

It proposes a novel semantic and proof-theoretic approach to bilateralist judgments using symmetrical two-dimensional calculi for non-deterministic semantics.

Findings

Proof-search algorithm runs in exponential time in general.

Algorithm runs in polynomial time with restricted rules.

Provides a proof-theoretic foundation for bilateralist non-deterministic semantics.

Abstract

The bilateralist approach to logical consequence maintains that judgments of different qualities should be taken into account in determining what-follows-from-what. We argue that such an approach may be actualized by a two-dimensional notion of entailment induced by semantic structures that also accommodate non-deterministic and partial interpretations, and propose a proof-theoretical apparatus to reason over bilateralist judgments using symmetrical two-dimensional analytical Hilbert-style calculi. We also provide a proof-search algorithm for finite analytic calculi that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned calculus.