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. (shrink)

Our regimentation of Goodman and Myhill’s proof of Excluded Middle revealed among its premises a form of Choice and an instance of Separation.Here we revisit Zermelo’s requirement that the separating property be definite. The instance that Goodman and Myhill used is not constructively warranted. It is that principle, and not Choice alone, that precipitates Excluded Middle.Separation in various axiomatizations of constructive set theory is examined. We conclude that insufficient critical attention has been paid to how those forms of Separation fail, (...) in light of the Goodman–Myhill result, to capture a genuinely constructive notion of set. (shrink)

The one-page 1978 informal proof of Goodman and Myhill is regimented in a weak constructive set theory in free logic. The decidability of identities in general (⁠|$a\!=\!b\vee\neg a\!=\!b$|⁠) is derived; then, of sentences in general (⁠|$\psi\vee\neg\psi$|⁠). Martin-Löf’s and Bell’s receptions of the latter result are discussed. Regimentation reveals the form of Choice used in deriving Excluded Middle. It also reveals an abstraction principle that the proof employs. It will be argued that the Goodman–Myhill result does not provide the constructive set (...) theorist with a dispositive reason for not adopting (full) Choice. (shrink)

Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories, probably the most natural of these is the existence property, EP, sometimes referred to as the set existence property. This states that whenever ϕϕ is provable, there is a formula χχ such that ϕ∧χϕ∧χ is provable. It has been known since the 80s that EP holds for some intuitionistic set theories and yet fails for IZF. Despite this, it has (...) remained open until now whether EP holds for the most well known constructive set theory, CZF. In this paper we show that EP fails for CZF. (shrink)

For every partial combinatory algebra, we define a hierarchy of extensionality relations using ordinals. We investigate the closure ordinals of pca’s, i.e., the smallest ordinals where these relations become equal. We show that the closure ordinal of Kleene’s first model is ${\omega _1^{\textit {CK}}}$ and that the closure ordinal of Kleene’s second model is $\omega _1$. We calculate the exact complexities of the extensionality relations in Kleene’s first model, showing that they exhaust the hyperarithmetical hierarchy. We also discuss embeddings of (...) pca’s. (shrink)

The paper proves a conjecture of Solomon Feferman concerning the indefiniteness of the continuum hypothesis relative to a semi-intuitionistic set theory.

Satisfiability or Sat\ is the metatheoretic statementEvery formally intuitionistically consistent set of first-order sentences has a model.The models in question are the Tarskian relational structures familiar from standard first-order model theory, but here treated within intuitionistic metamathematics. We prove that both IZF, intuitionistic Zermelo–Fraenkel set theory, and HAS, second-order Heyting arithmetic, prove Sat\ to be false outright. Following the lead of Carter :75–95, 2008), we then generalize this result to some provably intermediate first-order logics, including the Rose logic. These metatheorems (...) distinguish the intuitionistic foundational significance of Sat\ sharply from that of Sat\, the satisfiability claim for intuitionistic propositional logic. At the same time, they establish intuitionistic connections with and between Test, COMP\, and \. Here, Test is the scheme of Testability, and COMP\ and \ are completeness for intuitionistic propositional logic and predicate logic, respectively. (shrink)

Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Earlier work showed all of these implications to be strict. Here we reprove one of the strictness results, using very different arguments. The technique used is a mixture of realizability, forcing in the guise of Heyting-valued models, and Kripke models.

Partial combinatory algebras (pcas) are algebraic structures that serve as generalized models of computation. In this article, we study embeddings of pcas. In particular, we systematize the embeddings between relativizations of Kleene’s models, of van Oosten’s sequential computation model, and of Scott’s graph model, showing that an embedding between two relativized models exists if and only if there exists a particular reduction between the oracles. We obtain a similar result for the lambda calculus, showing in particular that it cannot be (...) embedded in Kleene’s first model. (shrink)

In [17], we introduced an extensional variant of generic realizability [22], where realizers act extensionally on realizers, and showed that this form of realizability provides inner models of $\mathsf {CZF}$ (constructive Zermelo–Fraenkel set theory) and $\mathsf {IZF}$ (intuitionistic Zermelo–Fraenkel set theory), that further validate $\mathsf {AC}_{\mathsf {FT}}$ (the axiom of choice in all finite types). In this paper, we show that extensional generic realizability validates several choice principles for dependent types, all exceeding $\mathsf {AC}_{\mathsf {FT}}$. We then show that adding (...) such choice principles does not change the arithmetic part of either $\mathsf {CZF}$ or $\mathsf {IZF}$. (shrink)

We solve a question of McLaughlin by showing that if A is a regressive co-simple isol, there is a co-simple regressive isol B such that the intersection type of A and B is trivial. The proof is a nonuniform 0 priority argument that can be viewed as the execution of a single strategy from a 0-argument. We establish some limit on the properties of such pairs by showing that if AxB has low degree, then the intersection type of A and (...) B cannot be trivial. (shrink)

This paper proves that the disjunction property, the numerical existence property, Church’s rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory, CZF, and also for the theory CZF augmented by the Regular Extension Axiom.As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth.