Realizability Semantics for Quantified Modal Logic: Generalizing Flagg's 1985 Construction

TL;DR

This paper introduces a realizability-based semantics for quantified modal logic, extending Flagg's 1985 model construction to encompass various modal theories and demonstrating its broad applicability.

Contribution

It generalizes Flagg's 1985 construction to a realizability semantics for quantified modal logic, enabling modeling of diverse modal theories and principles.

Findings

Constructs a model of a modal version of Church's Thesis

Develops a model of a modal set theory by Goodman and Scedrov

Provides a model based on Scott's graph model showing failure of stability of non-identity

Abstract

A semantics for quantified modal logic is presented that is based on Kleene's notion of realizability. This semantics generalizes Flagg's 1985 construction of a model of a modal version of Church's Thesis and first-order arithmetic. While the bulk of the paper is devoted to developing the details of the semantics, to illustrate the scope of this approach, we show that the construction produces (i) a model of a modal version of Church's Thesis and a variant of a modal set theory due to Goodman and Scedrov, (ii) a model of a modal version of Troelstra's generalized continuity principle together with a fragment of second-order arithmetic, and (iii) a model based on Scott's graph model (for the untyped lambda calculus) which witnesses the failure of the stability of non-identity.