REALIZABILITY SEMANTICS FOR QUANTIFIED MODAL LOGIC: GENERALIZING FLAGG’S 1985 CONSTRUCTION

AbstractA 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 nonidentity.

Download Full-text

Flagg realizability in arithmetic

Journal of Symbolic Logic ◽

10.1017/s002248120003125x ◽

1986 ◽

Vol 51 (2) ◽

pp. 387-392 ◽

Cited By ~ 2

Author(s):

Nicolas D. Goodman

Keyword(s):

Church’S Thesis ◽

First Order ◽

Suitable Form ◽

Church's Thesis ◽

Order Arithmetic ◽

Epistemic Arithmetic

Epistemic arithmetic—that is, first-order arithmetic with S4 as the underlying logic—was introduced by Shapiro in [7] and independently by Reinhardt in [6]. Shapiro showed that intuitionistic first-order arithmetic HA can be embedded in epistemic arithmetic EA. Moreover he showed that some of the basic proof-theoretic facts about HA, such as the existence and disjunction properties, can be extended to EA. In [3] we showed that the interpretation of HA in EA is faithful. (G.E. Mine has independently also proved this theorem.) Finally, in [2], Flagg showed that a suitable form of Church's thesis is consistent with EA. (Carlson [1] has announced another proof of this result.) Flagg's argument involves an ingenious realizability notion for EA which, as it stands, is not very perspicuous. The purpose of the present paper is to give a more transparent treatment of Flagg realizability. We obtain a new version of Flagg's proof of the consistency of Church's thesis with EA. Our main new result is that, in a sense to be made precise below, Flagg realizability coincides on HA embedded in EA with Kleene's 1945 realizability (e.g. see [5, pp. 501–516]). Thus it turns out once more that methods and results proved for EA can be viewed as extensions or generalizations of well-known methods and results for HA.

Download Full-text

Extension of Lifschitz' realizability to higher order arithmetic, and a solution to a problem of F. Richman

Journal of Symbolic Logic ◽

10.2307/2275064 ◽

1991 ◽

Vol 56 (3) ◽

pp. 964-973 ◽

Cited By ~ 2

Author(s):

Jaap van Oosten

Keyword(s):

Higher Order ◽

Second Order ◽

Church’S Thesis ◽

Second Order Arithmetic ◽

Church's Thesis ◽

Order Arithmetic ◽

Image Position

AbstractF. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic HAH:and if not, whether assuming Church's Thesis CT and Markov's Principle MP would help. Blass and Scedrov gave models of HAH in which this principle, which we call RP, is not valid, but their models do not satisfy either CT or MP.In this paper a realizability topos Lif is constructed in which CT and MP hold, but RP is false. (It is shown, however, that RP is derivable in HAH + CT + MP + ECT0, so RP holds in the effective topos.) Lif is a generalization of a realizability notion invented by V. Lifschitz. Furthermore, Lif is a subtopos of the effective topos.

Download Full-text

Lifschitz' realizability

Journal of Symbolic Logic ◽

10.2307/2274666 ◽

1990 ◽

Vol 55 (2) ◽

pp. 805-821 ◽

Cited By ~ 11

Author(s):

Jaap van Oosten

Keyword(s):

Axiomatic Characterization ◽

Uniqueness Condition ◽

Church’S Thesis ◽

Second Order Arithmetic ◽

Elementary Analysis ◽

Continuous Application ◽

Church's Thesis ◽

Order Arithmetic ◽

Intuitionistic Arithmetic

AbstractV. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a “q-variant” we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe an analogous development for elementary analysis, with partial continuous application replacing partial recursive application.

Download Full-text

FIRST-ORDER POSSIBILITY MODELS AND FINITARY COMPLETENESS PROOFS

The Review of Symbolic Logic ◽

10.1017/s1755020319000418 ◽

2019 ◽

Vol 12 (4) ◽

pp. 637-662

Author(s):

MATTHEW HARRISON-TRAINOR

Keyword(s):

Modal Logic ◽

Possible Worlds ◽

Canonical Model ◽

Model Construction ◽

Completeness Proof ◽

Quantified Modal Logic ◽

First Order ◽

Propositional Modal Logic ◽

Computable Set ◽

Order Case

AbstractThis article builds on Humberstone’s idea of defining models of propositional modal logic where total possible worlds are replaced by partial possibilities. We follow a suggestion of Humberstone by introducing possibility models for quantified modal logic. We show that a simple quantified modal logic is sound and complete for our semantics. Although Holliday showed that for many propositional modal logics, it is possible to give a completeness proof using a canonical model construction where every possibility consists of finitely many formulas, we show that this is impossible to do in the first-order case. However, one can still construct a canonical model where every possibility consists of a computable set of formulas and thus still of finitely much information.

Download Full-text

Undecidability of First-Order Intuitionistic and Modal Logics with Two variables

Bulletin of Symbolic Logic ◽

10.2178/bsl/1122038996 ◽

2005 ◽

Vol 11 (3) ◽

pp. 428-438 ◽

Cited By ~ 7

Author(s):

Roman Kontchakov ◽

Agi Kurucz ◽

Michael Zakharyaschev

Keyword(s):

Modal Logic ◽

Intuitionistic Logic ◽

Modal Logics ◽

Kripke Frame ◽

Standard Nomenclature ◽

Quantified Modal Logic ◽

First Order

AbstractWe prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, GL.3, etc.). For many quantified modal logics, including those in the standard nomenclature above, even the monadic two-variable fragments turn out to be undecidable.

Download Full-text

Relativized realizability in intuitionistic arithmetic of all finite types

Journal of Symbolic Logic ◽

10.2307/2271946 ◽

1978 ◽

Vol 43 (1) ◽

pp. 23-44 ◽

Cited By ~ 25

Author(s):

Nicolas D. Goodman

Keyword(s):

Extension Theorem ◽

General Notion ◽

Conservative Extension ◽

First Order ◽

New Information ◽

Reflection Theorem ◽

Order Arithmetic ◽

Special Case ◽

Dependent Choice ◽

Intuitionistic Arithmetic

In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in §1, we motivate and define our notion of realizability in §2. In §3 we prove a soundness theorem, and in §4 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In §5 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in §6, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let Σ be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let Σω be the theory obtained from Σ by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then Σω is a conservative extension of Σ. An interesting example of this theorem is obtained by taking Σ to be classical first-order arithmetic.

Download Full-text

Formula size games for modal logic and μ-calculus

Journal of Logic and Computation ◽

10.1093/logcom/exz025 ◽

2019 ◽

Vol 29 (8) ◽

pp. 1311-1344 ◽

Cited By ~ 2

Author(s):

Lauri T Hella ◽

Miikka S Vilander

Keyword(s):

Modal Logic ◽

Optimal Strategy ◽

Order Logic ◽

First Order Logic ◽

Kripke Models ◽

First Order ◽

Modal Operators ◽

Crucial Difference ◽

Definition Of ◽

Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

Download Full-text

Bleaching of chlorophylls by UV irradiation in vitro: The effects on chlorophyll organization in acetone and n-hexane

Journal of the Serbian Chemical Society ◽

10.2298/jsc0803271z ◽

2008 ◽

Vol 73 (3) ◽

pp. 271-282 ◽

Cited By ~ 12

Author(s):

Jelena Zvezdanovic ◽

Dejan Markovic

Keyword(s):

Uv Irradiation ◽

Photosynthetic Pigments ◽

Energy Input ◽

First Order ◽

First Order Kinetics ◽

Uv Photons ◽

The Stability ◽

Major Factors

The stability of chlorophylls toward UV irradiation was studied by Vis spectrophotometry in extracts containing mixtures of photosynthetic pigments in acetone and n-hexane. The chlorophylls underwent destruction (bleaching) obeying first-order kinetics. The bleaching was governed by three major factors: the energy input of the UV photons, the concentration of the chlorophylls and the polarity of the solvent, implying different molecular organizations of the chlorophylls in the two solvents.

Download Full-text