The term computational content typically refers to the computational information hidden in a proof of a first-order
sentence. For instance, for a statement of the form ∀∃ (, ) , the computational content is a method to compute for a given such that (, )
holds. However, the concept of extracting computational data from logical proofs is not limited to first-order theories. For example, in intuitionistic propositional or modal systems, the computational content of a disjunction ∨
is a way to read a proof of the disjunction and compute which disjunct is provable and then provide a proof for that disjunct [1]. When this computation can be carried out in polynomial time, the system is said to exhibit the feasible disjunction property.
In this talk, we will present our recent work [2] on the feasible disjunction property in intuitionistic modal logics. We begin by introducing a syntactically defined family of formulas, referred to as constructive formulas, to formalize the notion of constructively acceptable axioms. This class is chosen to be tight: it includes all commonly accepted axioms, yet any deviation from its syntactical form results in systems that lack the disjunction property and are therefore constructively unacceptable. Next, we demonstrate that any intuitionistic modal system axiomatized by constructive axioms and satisfying a mild technical condition possesses the feasible disjunction property. On the positive side, this result establishes the feasible disjunction property for several intuitionistic modal systems, including CK, IK, their extensions with the modal axioms , , 4, 5, axioms for bounded width and depth, and their fragments such as CK□, propositional lax logic, and IPC. On the negative side, we show that if a suficiently strong intuitionistic modal logic (meeting a mild technical condition) lacks the disjunction we prove that IPC is the only intermediate logic that admits a constructive axiomatization. property, it cannot be axiomatized using constructive axioms. Furthermore, by generalizing our main theorem, admissible rules, feasible disjunction property, intuitionistic modal logics LGOBE CEUR