Classical Arithmetic is Part of Intuitionistic Arithmetic

1998 ◽  
Vol 55 ◽  
pp. 127-141
Author(s):  
Michael Potter ◽  
Keyword(s):  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

scholarly journals Implicational complexity in intuitionistic arithmetic

1981 ◽  
Vol 46 (2) ◽  
pp. 240-248 ◽  
Author(s):  
Daniel Leivant
Keyword(s):  
Normal Form ◽  
Form Theorem ◽  
Natural Measure ◽  
Normal Form Theorem ◽  
Propositional Constants ◽  
Image Position ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

In classical arithmetic a natural measure for the complexity of relations is provided by the number of quantifier alternations in an equivalent prenex normal form. However, the proof of the Prenex Normal Form Theorem uses the following intuitionistically invalid rules for permuting quantifiers with propositional constants.Each one of these schemas, when added to Intuitionistic (Heyting's) Arithmetic IA, generates full Classical (Peano's) Arithmetic. Schema (3) is of little interest here, since one can obtain a formula intuitionistically equivalent to A ∨ ∀xBx, which is prenex if A and B are:For the two conjuncts on the r.h.s. (1) may be successively applied, since y = 0 is decidable.We shall readily verify that there is no way of similarly going around (1) or (2). This fact calls for counting implication (though not conjunction or disjunction) in measuring in IA the complexity of arithmetic relations. The natural implicational measure for our purpose is the depth of negative nestings of implication, defined as follows. I(F): = 0 if F is atomic; I(F ∧ G) = I(F ∨ G): = max[I(F), I(G)]; I(∀xF) = I(∃xF): = I(F); I(F → G):= max[I(F) + 1, I(G)].

Epistemic arithmetic is a conservative extension of intuitionistic arithmetic

1984 ◽  
Vol 49 (1) ◽  
pp. 192-203 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Propositional Calculus ◽  
Cut Elimination ◽  
Conservative Extension ◽  
First Order ◽  
Classical Mathematics ◽  
Order Arithmetic ◽  
Classical Propositional Calculus ◽  
Epistemic Arithmetic ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

Questions about the constructive or effective character of particular arguments arise in several areas of classical mathematics, such as in the theory of recursive functions and in numerical analysis. Some philosophers have advocated Lewis's S4 as the proper logic in which to formalize such epistemic notions. (The fundamental work on this is Hintikka [4].) Recently there have been studies of mathematical theories formalized with S4 as the underlying logic so that these epistemic notions can be expressed. (See Shapiro [7], Myhill [5], and Goodman [2]. The motivation for this work is discussed in Goodman [3].) The present paper is a contribution to the study of the simplest of these theories, namely first-order arithmetic as formalized in S4. Following Shapiro, we call this theory epistemic arithmetic (EA). More specifically, we show that EA is a conservative extension of Hey ting's arithmetic HA (ordinary first-order intuitionistic arithmetic). The question of whether EA is conservative over HA was raised but left open in Shapiro [7].The idea of our proof is as follows. We interpret EA in an infinitary propositional S4, pretty much as Tait, for example, interprets classical arithmetic in his infinitary classical propositional calculus in [8]. We then prove a cut-elimination theorem for this infinitary propositional S4. A suitable version of the cut-elimination theorem can be formalized in HA. For cut-free infinitary proofs, there is a reflection principle provable in HA. That is, we can prove in HA that if there is a cut-free proof of the interpretation of a sentence ϕ then ϕ is true. Combining these results shows that if the interpretation of ϕ is provable in EA, then ϕ is provable in HA.

Arithmetic Certainty

2015 ◽  
Author(s):  
José Ferreirós
Keyword(s):  
Number Theory ◽  
Model Theory ◽  
Algebraic Number ◽  
Analytic Number Theory ◽  
Algebraic Number Theory ◽  
Elementary Number Theory ◽  
Arithmetical Knowledge ◽  
Classical Arithmetic ◽  
Similar Claim ◽  
Intuitionistic Arithmetic

This chapter considers the idea that we have certainty in our basic arithmetic knowledge. The claim that arithmetical knowledge enjoys certainty cannot be extended to a similar claim about number theory “as a whole.” It is thus necessary to distinguish between elementary number theory and other, more advanced, levels in the study of numbers: algebraic number theory, analytic number theory, and perhaps set-theoretic number theory. The chapter begins by arguing that the axioms of Peano Arithmetic are true of counting numbers and describing some elements found in counting practices. It then offers an account of basic arithmetic and its certainty before discussing a model theory of arithmetic and the logic of mathematics. Finally, it asks whether elementary arithmetic, built on top of the practice of counting, should be classical arithmetic or intuitionistic arithmetic.

The Problem of Consistency

2017 ◽  
Author(s):  
Jan von Plato
Keyword(s):  
Consistency Problem ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

This chapter talks about how the translations from classical to intuistic arithmetic that Gödel and Gentzen found in 1932–33 showed that the consistency of classical arithmetic reduces to that of intuitionistic arithmetic. The main aim of Hilbert's program in the 1920s had been to show that the infinitistic component of arithmetic, namely the use of quantificational inferences in indirect proofs, does not lead to contradiction. It followed from Gödel's and Gentzen's result that these classical steps are harmless. Therefore, the consistency problem of arithmetic has an intuitionistic sense and, consequently, possibly also an intuitionistic solution. Bernays was quick to point out that intuitionism transcends the boundaries of strictly finitary reasoning.

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.

Intensional interpretations of functionals of finite type I

1967 ◽  
Vol 32 (2) ◽  
pp. 198-212 ◽  
Author(s):  
W. W. Tait
Keyword(s):  
Finite Type ◽  
Type I ◽  
Axiom Schema ◽  
Image Position ◽  
Intuitionistic Arithmetic

T0 will denote Gödel's theory T[3] of functionals of finite type (f.t.) with intuitionistic quantification over each f.t. added. T1 will denote T0 together with definition by bar recursion of type o, the axiom schema of bar induction, and the schemaof choice. Precise descriptions of these systems are given below in §4. The main results of this paper are interpretations of T0 in intuitionistic arithmetic U0 and of T1 in intuitionistic analysis is U1. U1 is U0 with quantification over functionals of type (0,0) and the axiom schemata AC00 and of bar induction.

Application of Fuzzy Numbers to Assessment Processes

2018 ◽  
pp. 3215-3225
Author(s):  
Michael Voskoglou
Keyword(s):  
Assessment Tool ◽  
Special Kind ◽  
Assessment Method ◽  
Future Research ◽  
Grade Point ◽  
Mean Values ◽  
The Subject ◽  
The Mean ◽  
Fuzzy Assessment ◽  
Classical Arithmetic

A Fuzzy Number (FN) is a special kind of FS on the set R of real numbers. The four classical arithmetic operations can be defined on FNs, which play an important role in fuzzy mathematics analogous to the role played by the ordinary numbers in crisp mathematics (Kaufmann & Gupta, 1991). The simplest form of FNs is the Triangular FNs (TFNs), while the Trapezoidal FNs (TpFNs) are straightforward generalizations of the TFNs. In the present work a combination of the COG defuzzification technique and of the TFNs (or TpFNs) is used as an assessment tool. Examples of assessing student problem-solving abilities and basket-ball player skills are also presented illustrating in practice the results obtained. This new fuzzy assessment method is validated by comparing its outcomes in the above examples with the corresponding outcomes of two commonly used assessment methods of the traditional logic, the calculation of the mean values and of the Grade Point Average (GPA) index. Finally, the perspectives of future research on the subject are discussed.

Application of Fuzzy Numbers to Assessment Processes

2019 ◽  
pp. 407-420
Author(s):  
Michael Voskoglou
Keyword(s):  
Assessment Tool ◽  
Special Kind ◽  
Assessment Method ◽  
Basketball Player ◽  
Future Research ◽  
Grade Point ◽  
Mean Values ◽  
The Subject ◽  
Fuzzy Assessment ◽  
Classical Arithmetic

A fuzzy number (FN) is a special kind of FS on the set R of real numbers. The four classical arithmetic operations can be defined on FNs, which play an important role in fuzzy mathematics analogous to the role played by the ordinary numbers in crisp mathematics. The simplest form of FNs is the triangular FNs (TFNs), while the trapezoidal FNs (TpFNs) are straightforward generalizations of the TFNs. In the chapter, a combination of the COG defuzzification technique and of the TFNs (or TpFNs) is used as an assessment tool. Examples of assessing student problem-solving abilities and basketball player skills are also presented illustrating in practice the results obtained. This new fuzzy assessment method is validated by comparing its outcomes in the above examples with the corresponding outcomes of two commonly used assessment methods of the traditional logic, the calculation of the mean values, and of the grade point average (GPA) index. Finally, the perspectives of future research on the subject are discussed.

Sign in / Sign up

Export Citation Format

Share Document