On Modal Logics of Partial Recursive Functions

TL;DR

This paper introduces modal logics for partial recursive functions, extending propositional logic with a new modality, and proves their soundness, completeness, and decidability for both deterministic and non-deterministic cases.

Contribution

It develops and characterizes modal logics that capture the semantics of partial recursive functions, including their deterministic and non-deterministic variants.

Findings

Semantic completeness of the modal logics is established.

Decidability of the proposed modal logics is proven.

Modal logics accurately model partial recursive functions.

Abstract

The classical propositional logic is known to be sound and complete with respect to the set semantics that interprets connectives as set operations. The paper extends propositional language by a new binary modality that corresponds to partial recursive function type constructor under the above interpretation. The cases of deterministic and non-deterministic functions are considered and for both of them semantically complete modal logics are described and decidability of these logics is established.