Finite injury and Σ1-induction

1989 ◽  
Vol 54 (1) ◽  
pp. 38-49 ◽  
Author(s):  
Michael Mytilinaios
Keyword(s):  
First Order ◽  
Base Theory ◽  
Order Arithmetic

AbstractWorking in the language of first-order arithmetic we consider models of the base theory P−. Suppose M is a model of P− and let M satisfy induction for Σ1-formulas. First it is shown that the Friedberg-Muchnik finite injury argument can be performed inside M, and then, using a blocking method for the requirements, we prove that the Sacks splitting construction can be done in M. So, the “amount” of induction needed to perform the known finite injury priority arguments is Σ1-induction.

Relativized realizability in intuitionistic arithmetic of all finite types

1978 ◽  
Vol 43 (1) ◽  
pp. 23-44 ◽  
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.

On the role of Ramsey quantifiers in first order arithmetic

1982 ◽  
Vol 47 (2) ◽  
pp. 423-435 ◽  
Author(s):  
James H. Schmerl ◽  
Stephen G. Simpson
Keyword(s):  
Formal System ◽  
Intended Meaning ◽  
Completeness Proof ◽  
First Order ◽  
Uncountable Cardinal ◽  
Consistent Extension ◽  
Witness Set ◽  
Order Arithmetic ◽  
Infinite Set

The purpose of this paper is to study a formal system PA(Q2) of first order Peano arithmetic, PA, augmented by a Ramsey quantifier Q2 which binds two free variables. The intended meaning of Q2xx′φ(x, x′) is that there exists an infinite set X of natural numbers such that φ(a, a′) holds for all a, a′ Є X such that a ≠ a′. Such an X is called a witness set for Q2xx′φ(x, x′). Our results would not be affected by the addition of further Ramsey quantifiers Q3, Q4, …, Here of course the intended meaning of Qkx1 … xkφ(x1,…xk) is that there exists an infinite set X such that φ(a1…, ak) holds for all k-element subsets {a1, … ak} of X.Ramsey quantifiers were first introduced in a general model theoretic setting by Magidor and Malitz [13]. The system PA{Q2), or rather, a system essentially equivalent to it, was first defined and studied by Macintyre [12]. Some of Macintyre's results were obtained independently by Morgenstern [15]. The present paper is essentially self-contained, but all of our results have been directly inspired by those of Macintyre [12].After some preliminaries in §1, we begin in §2 by giving a new completeness proof for PA(Q2). A by-product of our proof is that for every regular uncountable cardinal k, every consistent extension of PA(Q2) has a k-like model in which all classes are definable. (By a class we mean a subset of the universe of the model, every initial segment of which is finite in the sense of the model.)

scholarly journals Finite Arithmetic Axiomatization for the Basis of Hyperrational Non-Standard Analysis

Axioms ◽  
2021 ◽  
Vol 10 (4) ◽  
pp. 263
Author(s):  
Yuri N. Lovyagin ◽  
Nikita Yu. Lovyagin
Keyword(s):  
Set Theory ◽  
Mathematical Analysis ◽  
Axiomatic System ◽  
Elementary Number Theory ◽  
Mathematical Application ◽  
First Order ◽  
Logic Approach ◽  
Order Arithmetic ◽  
Finite Arithmetic ◽  
Non Standard Analysis

The standard elementary number theory is not a finite axiomatic system due to the presence of the induction axiom scheme. Absence of a finite axiomatic system is not an obstacle for most tasks, but may be considered as imperfect since the induction is strongly associated with the presence of set theory external to the axiomatic system. Also in the case of logic approach to the artificial intelligence problems presence of a finite number of basic axioms and states is important. Axiomatic hyperrational analysis is the axiomatic system of hyperrational number field. The properties of hyperrational numbers and functions allow them to be used to model real numbers and functions of classical elementary mathematical analysis. However hyperrational analysis is based on well-known non-finite hyperarithmetic axiomatics. In the article we present a new finite first-order arithmetic theory designed to be the basis of the axiomatic hyperrational analysis and, as a consequence, mathematical analysis in general as a basis for all mathematical application including AI problems. It is shown that this axiomatics meet the requirements, i.e., it could be used as the basis of an axiomatic hyperrational analysis. The article in effect completes the foundation of axiomatic hyperrational analysis without calling in an arithmetic extension, since in the framework of the presented theory infinite numbers arise without invoking any new constants. The proposed system describes a class of numbers in which infinite numbers exist as natural objects of the theory itself. We also do not appeal to any “enveloping” set theory.

Reverse Mathematics: The Playground of Logic

2010 ◽  
Vol 16 (3) ◽  
pp. 378-402 ◽  
Author(s):  
Richard A. Shore
Keyword(s):  
Mathematical Logic ◽  
Reverse Mathematics ◽  
Computational Approach ◽  
Second Order ◽  
Second Order Arithmetic ◽  
Base Theory ◽  
Order Arithmetic

AbstractThis paper is essentially the author's Gödel Lecture at the ASL Logic Colloquium '09 in Sofia extended and supplemented by material from some other papers. After a brief description of traditional reverse mathematics, a computational approach to is presented. There are then discussions of some interactions between reverse mathematics and the major branches of mathematical logic in terms of the techniques they supply as well as theorems for analysis. The emphasis here is on ones that lie outside the usual main systems of reverse mathematics. While retaining the usual base theory and working still within second order arithmetic, theorems are described that range from those far below the usual systems to ones far above.

A weak absolute consistency proof for some systems of illative combinatory logic

1983 ◽  
Vol 48 (3) ◽  
pp. 771-776 ◽  
Author(s):  
M.W. Bunder
Keyword(s):  
Set Theory ◽  
Combinatory Logic ◽  
Weak Consistency ◽  
Consistency Proof ◽  
First Order ◽  
Formal Systems ◽  
Elementary Methods ◽  
Order Arithmetic ◽  
Strongly Consistent ◽  
Order Predicate Calculus

A large number of formal systems based on combinatory logic or λ-calculus have been extended to include first order predicate calculus. Several of these however have been shown to be inconsistent, all, as far as the author knows, in the strong sense that all well formed formulas (which here include all strings of symbols) are provable. We will call the corresponding consistency notion—an arbitrary wff ⊥ is provable—weak consistency. We will say that a system is strongly consistent if no formula and its negation are provable.Now for some systems, such as that of Kuzichev [11], the strong and weak consistency notions are equivalent, but in the systems of [5] and [6], which we will be considering, they are not. Each of these systems is strong enough to have all of ZF set theory, except Grounding and Choice, interpretable in it, and the system of [5] can also encompass first order arithmetic (see [7]). It therefore seems unlikely that a strong consistency result could be proved for these systems using elementary methods. In this paper however, we prove the weak consistency of both these systems by means that could be formulated, at least within the theory of [5]. The method also applies to the typed systems of Curry, Hindley and Seldin [10] and to Seldin's generalised types [12].

Some properties of epistemic set theory with collection

1986 ◽  
Vol 51 (3) ◽  
pp. 748-754 ◽  
Author(s):  
Andre Scedrov
Keyword(s):  
Set Theory ◽  
Intuitionistic Logic ◽  
Existential Quantifier ◽  
Modal Interpretation ◽  
Conservative Extension ◽  
Disjunction Property ◽  
First Order ◽  
Slight Extension ◽  
Order Arithmetic ◽  
Epistemic Systems

Myhill [12] extended the ideas of Shapiro [15], and proposed a system of epistemic set theory IST (based on modal S4 logic) in which the meaning of the necessity operator is taken to be the intuitive provability, as formalized in the system itself. In this setting one works in classical logic, and yet it is possible to make distinctions usually associated with intuitionism, e.g. a constructive existential quantifier can be expressed as (∃x) □ …. This was first confirmed when Goodman [7] proved that Shapiro's epistemic first order arithmetic is conservative over intuitionistic first order arithmetic via an extension of Gödel's modal interpretation [6] of intuitionistic logic.Myhill showed that whenever a sentence □A ∨ □B is provable in IST, then A is provable in IST or B is provable in IST (the disjunction property), and that whenever a sentence ∃x.□A(x) is provable in IST, then so is A(t) for some closed term t (the existence property). He adapted the Friedman slash [4] to epistemic systems.Goodman [8] used Epistemic Replacement to formulate a ZF-like strengthening of IST, and proved that it was a conservative extension of ZF and that it had the disjunction and existence properties. It was then shown in [13] that a slight extension of Goodman's system with the Epistemic Foundation (ZFER, cf. §1) suffices to interpret intuitionistic ZF set theory with Replacement (ZFIR, [10]). This is obtained by extending Gödel's modal interpretation [6] of intuitionistic logic. ZFER still had the properties of Goodman's system mentioned above.

scholarly journals Random reals, the rainbow Ramsey theorem, and arithmetic conservation

2013 ◽  
Vol 78 (1) ◽  
pp. 195-206 ◽  
Author(s):  
Chris J. Conidis ◽  
Theodore A. Slaman
Keyword(s):  
Ramsey Theorem ◽  
First Order ◽  
Base Theory ◽  
Random Reals

AbstractWe investigate the question “To what extent can random reals be used as a tool to establish number theoretic facts?” Let 2-RAN be the principle that for every real X there is a real R which is 2-random relative to X. In Section 2, we observe that the arguments of Csima and Mileti [3] can be implemented in the base theory RCA0 and so RCA0 + 2-RAN implies the Rainbow Ramsey Theorem. In Section 3, we show that the Rainbow Ramsey Theorem is not conservative over RCA0 for arithmetic sentences. Thus, from the Csima–Mileti fact that the existence of random reals has infinitary-combinatorial consequences we can conclude that 2-RAN has non-trivial arithmetic consequences. In Section 4, we show that 2-RAN is conservative over RCA0 + BΣ2 for -sentences. Thus, the set of first-order consequences of 2-RAN is strictly stronger than P− + IΣ1 and no stronger than P− + BΣ2.

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.

Sign in / Sign up

Export Citation Format

Share Document