The language of linear temporal logic can be interpreted on the class of dynamic topological systems, giving rise to the intuitionistic temporal logic ${\sf ITL}^{\sf c}_{\Diamond \forall }$, recently shown to be decidable by Fernández-Duque. In this article we axiomatize this logic, some fragments, and prove completeness for several familiar spaces.

There seems to be a view that intuitionists not only take the Axiom of Choice (AC) to be true, but also believe it a consequence of their fundamental posits. Widespread or not, this view is largely mistaken. This article offers a brief, yet comprehensive, overview of the status of AC in various intuitionistic and constructivist systems. The survey makes it clear that the Axiom of Choice fails to be a theorem in most contexts and is even outright false in some (...) important contexts. Of the systems surveyed, only intensional type theory renders AC a theorem, but the extent of AC in that theory does not include, for instance, real analysis. Only a small amount of extensionality is required in order for the obvious proof an intuitionist might offer for AC to break down. (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)

Since in Heyting Arithmetic all atomic formulas are decidable, a Kripke model for HA may be regarded classically as a collection of classical structures for the language of arithmetic, partially ordered by the submodel relation. The obvious question is then: are these classical structures models of Peano Arithmetic ? And dually: if a collection of models of PA, partially ordered by the submodel relation, is regarded as a Kripke model, is it a model of HA? Some partial answers to these (...) questions were obtained in [6], [3], [1] and [2]. Here we present some results in the same direction, announced in [7]. In particular, it is proved that the classical structures at the nodes of a Kripke model of HA must be models of IΔ1 and that the relation between these classical structures must be that of a Δ1-elementary submodel. MSC: 03F30, 03F55. (shrink)

A sentence of the usual language of set theory is said to be stratified if it is obtained by “erasing” type indices in a sentence of the language of Russell's Simple Theory of Types. In this paper we give an alternative presentation of a proof the ambiguity theorem stating that any provable stratified sentence has a stratified proof. To this end, we introduce a new set of ambiguity axioms, inspired by Fraïssé's characterization of elementary equivalence; these axioms can be naturally (...) used to give different proofs of the ambiguity theorem . MSC: 03B15, 03F50, 03F55. (shrink)

Free choice sequences play a key role in the intuitionistic theory of the continuum and especially in the theorems of intuitionistic analysis that conflict with classical analysis, leading many classical mathematicians to reject the concept of a free choice sequence. By treating free choice sequences as potentially infinite objects, however, they can be comfortably situated alongside classical analysis, allowing a rapprochement of these two mathematical traditions. Building on recent work on the modal analysis of potential infinity, I formulate a modal (...) theory of the free choice sequences known as lawless sequences. Intrinsically well-motivated axioms for lawless sequences are added to a background theory of classical second-order arithmetic, leading to a theory I call $MC_{LS}$. This theory interprets the standard intuitionistic theory of lawless sequences and is conservative over the classical background theory. (shrink)

Vardanyan’s Theorems [36, 37] state that $\mathsf {QPL}(\mathsf {PA})$ —the quantified provability logic of Peano Arithmetic—is $\Pi ^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge [38] generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf (...) {QRC_1}$ was previously introduced by the authors [1] as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf {QRC_1}$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf {QRC_1}$ is the strictly positive fragment of $\mathsf {QGL}$ and a fragment of $\mathsf {QPL}(\mathsf {PA})$. (shrink)

We study constructive set theories, which deal with operations applying both to sets and operations themselves. Our starting point is a fully explicit, finitely axiomatized system ESTE of constructive sets and operations, which was shown in 10 to be as strong as PA. In this paper we consider extensions with operations, which internally represent description operators, unbounded set quantifiers and local fixed point operators. We investigate the proof theoretic strength of the resulting systems, which turn out to be impredicative . (...) © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim. (shrink)

A form of Kripke's schema turns out to be equivalent to each of the following two statements from metric topology: every open subspace of a separable metric space is separable; every open subset of a separable metric space is a countable union of open balls. Thus Kripke's schema serves as a point of reference for classifying theorems of classical mathematics within Bishop-style constructive reverse mathematics.

Using the framework of categorical logic, this paper analyzes and streamlines Gabbay's semantical proof of the Craig interpolation theorem for intuitionistic predicate logic. In the process, an apparently new and interesting fact about the relation of coherent and intuitionistic logic is found.