Lifschitz' realizability

1990 ◽  
Vol 55 (2) ◽  
pp. 805-821 ◽  
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.

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

1991 ◽  
Vol 56 (3) ◽  
pp. 964-973 ◽  
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.

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

2016 ◽  
Vol 9 (4) ◽  
pp. 752-809 ◽  
Author(s):  
BENJAMIN G. RIN ◽  
SEAN WALSH
Keyword(s):  
Modal Logic ◽  
Graph Model ◽  
Church’S Thesis ◽  
Quantified Modal Logic ◽  
First Order ◽  
Continuity Principle ◽  
Generalized Continuity ◽  
Church's Thesis ◽  
Order Arithmetic ◽  
The Stability

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.

Stewart Shapiro. Introduction—intensional mathematics and constructive mathematics. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, vol. 113, North-Holland, Amsterdam, New York, and Oxford, 1985, pp. 1–10. - Stewart Shapiro. Epistemic and intuitionistic arithmetic. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 11–46. - John Myhill. Intensional set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 47–61. - Nicolas D. Goodman. A genuinely intensional set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 63–79. - Andrej Ščedrov. Extending Godel's modal interpretation to type theory and set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 81–119. - Robert C. Flagg. Church's thesis is consistent with epistemic arithmetic. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 121–172.

1991 ◽  
Vol 56 (4) ◽  
pp. 1496-1499 ◽  
Author(s):  
Craig A. Smoryński
Keyword(s):  
New York ◽  
Set Theory ◽  
Type Theory ◽  
Foundations Of Mathematics ◽  
Constructive Mathematics ◽  
Modal Interpretation ◽  
Church’S Thesis ◽  
Church's Thesis ◽  
Epistemic Arithmetic ◽  
Intuitionistic Arithmetic

The mean value theorem in second order arithmetic

2001 ◽  
Vol 66 (3) ◽  
pp. 1353-1358 ◽  
Author(s):  
Christopher S. Hardin ◽  
Daniel J. Velleman
Keyword(s):  
Mean Value ◽  
Second Order ◽  
Mean Value Theorem ◽  
Natural Numbers ◽  
Second Order Arithmetic ◽  
Elementary Analysis ◽  
Logical Connectives ◽  
The Mean ◽  
Order Arithmetic ◽  
Image Position

This paper is a contribution to the project of determining which set existence axioms are needed to prove various theorems of analysis. For more on this project and its history we refer the reader to [1] and [2].We work in a weak subsystem of second order arithmetic. The language of second order arithmetic includes the symbols 0, 1, =, <, +, ·, and ∈, together with number variables x, y, z, … (which are intended to stand for natural numbers), set variables X, Y, Z, … (which are intended to stand for sets of natural numbers), and the usual quantifiers (which can be applied to both kinds of variables) and logical connectives. We write ∀x < t φ and ∃x < t φ as abbreviations for ∀x(x < t → φ) and ∃x{x < t ∧ φ) respectively; these are called bounded quantifiers. A formula is said to be if it has no quantifiers applied to set variables, and all quantifiers applied to number variables are bounded. It is if it has the form ∃xθ and it is if it has the form ∀xθ, where in both cases θ is .The theory RCA0 has as axioms the usual Peano axioms, with the induction scheme restricted to formulas, and in addition the comprehension scheme, which consists of all formulas of the formwhere φ is , ψ is , and X does not occur free in φ(n). (“RCA” stands for “Recursive Comprehension Axiom.” The reason for the name is that the comprehension scheme is only strong enough to prove the existence of recursive sets.) It is known that this theory is strong enough to allow the development of many of the basic properties of the real numbers, but that certain theorems of elementary analysis are not provable in this theory. Most relevant for our purposes is the fact that it is impossible to prove in RCA0 that every continuous function on the closed interval [0, 1] attains maximum and minimum values (see [1]).Since the most common proof of the Mean Value Theorem makes use of this theorem, it might be thought that the Mean Value Theorem would also not be provable in RCA0. However, we show in this paper that the Mean Value Theorem can be proven in RCA0. All theorems stated in this paper are theorems of RCA0, and all of our reasoning will take place in RCA0.

Predicate Logics of Constructive Arithmetical Theories

2006 ◽  
Vol 71 (4) ◽  
pp. 1311-1326 ◽  
Author(s):  
Albert Visser
Keyword(s):  
Predicate Logic ◽  
Uniqueness Condition ◽  
Church’S Thesis ◽  
Church's Thesis

AbstractIn this paper, we show that the predicate logics of consistent extensions of Heyting's Arithmetic plus Church's Thesis with uniqueness condition are complete . Similarly, we show that the predicate logic of HA*. i.e. Heyting's Arithmetic plus the Completeness Principle (for HA*) is complete . These results extend the known results due to Valery Plisko. To prove the results we adapt Plisko's method to use Tennenbaum's Theorem to prove ‘categoricity of interpretations’ under certain assumptions.

Some models for intuitionistic finite type arithmetic with fan functional

1977 ◽  
Vol 42 (2) ◽  
pp. 194-202 ◽  
Author(s):  
A. S. Troelstra
Keyword(s):  
Finite Type ◽  
Church’S Thesis ◽  
Proper Understanding ◽  
New Model ◽  
Fan Theorem ◽  
Church's Thesis ◽  
Definition Of ◽  
Intuitionistic Arithmetic

In this note we shall assume acquaintance with [T4] and the parts of [T1] which deal with intuitionistic arithmetic in all finite types. The bibliography just continues the bibliography of [T4].The principal purpose of this note is the discussion of two models for intuitionistic finite type arithmetic with fan functional (HAω+ MUC). The first model is needed to correct an oversight in the proof of Theorem 6 [T4, §5]: the model ECF+as defined there cannot be shown to have the required properties inEL+ QF-AC, the reason being that a change in the definition ofW12alone does not suffice—if one wishes to establish closure under the operations of HAωthe definitions ofW1σfor other σ have to be adopted as well. It is difficult to see how to do this directly in a uniform way — but we succeed via a detour, which is described in §2.For a proper understanding, we should perhaps note already here thaton the assumption of the fan theorem, ECF+as defined in [T4] and the new model of this note coincide (since then the definition ofW12[T4, p. 594] is equivalent to the definition forW12in the case of ECF); but inELit is impossible to prove this (and under assumption of Church's thesis the two models differ).

Undecidability of the real-algebraic structure of models of intuitionistic elementary analysis

2000 ◽  
Vol 65 (3) ◽  
pp. 1014-1030 ◽  
Author(s):  
Miklós Erdélyi-Szabó
Keyword(s):  
Algebraic Structure ◽  
Second Order ◽  
Heyting Algebras ◽  
Real Numbers ◽  
Second Order Arithmetic ◽  
The Real ◽  
First Order ◽  
Elementary Analysis ◽  
Order Arithmetic

AbstractWe show that true first-order arithmetic is interpretable over the real-algebraic structure of models of intuitionistic analysis built upon a certain class of complete Heyting algebras. From this the undecidability of the structures follows. We also show that Scott's model is equivalent to true second-order arithmetic. In the appendix we argue that undecidability on the language of ordered rings follows from intuitionistically plausible properties of the real numbers.

Minimal readability of intuitionistic arithmetic and elementary analysis

1995 ◽  
Vol 60 (4) ◽  
pp. 1208-1241 ◽  
Author(s):  
Zlatan Damnjanovic
Keyword(s):  
Finite Type ◽  
Peano Arithmetic ◽  
New Method ◽  
Recursive Functions ◽  
Heyting Arithmetic ◽  
Elementary Analysis ◽  
Skolem Functions ◽  
Definable Functions ◽  
Intuitionistic Arithmetic

AbstractA new method of “minimal” readability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)—functions f such that HA ⊢ ∀x∃!yA(x, y) ⇒ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of ℒ(HA) with only x,y free—are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the < ε0-recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be < ε0-recursive. The method is extended to intuitionistic finite-type arithmetic, , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived.

Sign in / Sign up

Export Citation Format

Share Document