A Sketch of a Proof-Theoretic Semantics for Necessity

TL;DR

This paper develops a proof-theoretic semantics for necessity in intuitionist logic, introducing a higher order operator to express a notion of relative necessity based on assumptions and deductions.

Contribution

It extends intuitionist logic with a higher order operator to formalize a proof-theoretic semantics for necessity, inspired by Pfenning and Davies's system.

Findings

Defines a notion of relative necessity within the extended logic

Provides a formal semantics connecting assumptions and conclusions

Offers a framework for understanding necessity in proof-theoretic terms

Abstract

This paper considers proof-theoretic semantics for necessity within Dummett's and Prawitz's framework. Inspired by a system of Pfenning's and Davies's, the language of intuitionist logic is extended by a higher order operator which captures a notion of validity. A notion of relative necessary is defined in terms of it, which expresses a necessary connection between the assumptions and the conclusion of a deduction.