On the interpretation of intuitionistic number theory

1945 ◽  
Vol 10 (4) ◽  
pp. 109-124 ◽  
Author(s):  
S. C. Kleene

The purpose of this article is to introduce the notion of “recursive realizability.”Let P be some property of natural numbers. Consider the existential statement, “There exists a number n having the property P.” To explain the meaning which this has for a constructivist or intuitionist, it has been described as a partial judgement, or incomplete communication of a more specific statement which says that a certain given number n, or the number n obtainable by a certain given method, has the property P. The meaning of the existential statement thus resides in a reference to certain information, which it implies could be stated in detail, though the trouble is not taken to do so. Perhaps the detail is suppressed in order to convey a general view of some fact.The information to which reference is made should be thought of as possibly comprising other items besides the value of n or method for obtaining it, namely such items as may be necessary to complete the communication that that n has the property P.

2004 ◽  
Vol 89 (516) ◽  
pp. 403-408
Author(s):  
P. G. Brown

In many of the basic courses in Number Theory, Finite Mathematics and Cryptography we come across the so-called arithmetic functions such as ϕn), σ(n), τ(n), μ(n), etc, whose domain is the set of natural numbers. These functions are well known and evaluated through the prime factor decomposition of n. It is less well known that these functions possess inverses (with respect to Dirichlet multiplication) which have interesting properties and applications.


1992 ◽  
Vol 57 (3) ◽  
pp. 1108-1119 ◽  
Author(s):  
Gerhard Jäger ◽  
Barbara Primo

AbstractThis paper presents several proof-theoretic results concerning weak fixed point theories over second order number theory with arithmetic comprehension and full or restricted induction on the natural numbers. It is also shown that there are natural second order theories which are proof-theoretically equivalent but have different proof-theoretic ordinals.


2013 ◽  
Vol 56 (1) ◽  
pp. 35-45
Author(s):  
Milan Paštéka ◽  
Zuzana Václavíková

ABSTRACT In this paper we study the conditions (1), (2) and (3) for the permutations which preserve the weighted density. These conditions are motivated by the conditions of Lévy group, originated in [Levy, P.: Problèmes concrets d’Analyse Fonctionelle. Gauthier Villars, Paris, 1951], and studied in [Obata, N.: Density of natural numbers and Lévy group, J. Number Theory 30 (1988), 288-297]. In the second part we prove that under some conditions for the sequence of weights, for instance for the logarithmic density, the first two conditions can be launched


Author(s):  
Michael Detlefsen

In the first, geometric stage of Hilbert’s formalism, his view was that a system of axioms does not express truths particular to a given subject matter but rather expresses a network of logical relations that can (and, ideally, will) be common to other subject matters. The formalism of Hilbert’s arithmetical period extended this view by emptying even the logical terms of contentual meaning. They were treated purely as ideal elements whose purpose was to secure a simple and perspicuous logic for arithmetical reasoning – specifically, a logic preserving the classical patterns of logical inference. Hilbert believed, however, that the use of ideal elements should not lead to inconsistencies. He thus undertook to prove the consistency of ideal arithmetic with its contentual or finitary counterpart and to do so by purely finitary means. In this, ‘Hilbert’s programme’, Hilbert and his followers were unsuccessful. Work published by Kurt Gödel in 1931 suggested that such failure was perhaps inevitable. In his second incompleteness theorem, Gödel showed that for any consistent formal axiomatic system T strong enough to formalize what was traditionally regarded as finitary reasoning, it is possible to define a sentence that expresses the consistency of T, and is not provable in T. From this it has generally been concluded that the consistency of even the ideal arithmetic of the natural numbers is not finitarily provable and that Hilbert’s programme must therefore fail. Despite problematic elements in this reasoning, post-Gödelian work on Hilbert’s programme has generally accepted it and attempted to minimize its effects by proposing various modifications of Hilbert’s programme. These have generally taken one of three forms: attempts to extend Hilbert’s finitism to stronger constructivist bases capable of proving more than is provable by strictly finitary means; attempts to show that for a significant family of ideal systems there are ways of ‘reducing’ their consistency problems to those of theories possessing more elementary (if not altogether finitary) justifications; and attempts by the so-called ‘reverse mathematics’ school to show that the traditionally identified ideal theories do not need to be as strong as they are in order to serve their mathematical purposes. They can therefore be reduced to weaker theories whose consistency problems are more amenable to constructivist (indeed, finitist) treatment.


2014 ◽  
Vol 24 (2-3) ◽  
pp. 316-383 ◽  
Author(s):  
PIERRE-ÉVARISTE DAGAND ◽  
CONOR McBRIDE

AbstractProgramming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: We can finally write correct-by-construction software. However, this extreme accuracy is also a curse: A datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: The users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.


1952 ◽  
Vol 17 (3) ◽  
pp. 192-197 ◽  
Author(s):  
John Myhill

Martin has shown that the notions of ancestral and class-inclusion are sufficient to develop the theory of natural numbers in a system containing variables of only one type.The purpose of the present paper is to show that an analogous construction is possible in a system containing, beyond the quantificational level, only the ancestral and the ordered pair.The formulae of our system comprise quantificational schemata and anything which can be obtained therefrom by writing pairs (e.g. (x; y), ((x; y); (x; (y; y))) etc.) for free variables, or by writing ancestral abstracts (e.g. (*xyFxy) etc.) for schematic letters, or both.The ancestral abstract (*xyFxy) means what is usually meant by ; and the formula (*xyFxy)zw answers to Martin's (zw; xy)(Fxy).The system presupposes a non-simple applied functional calculus of the first order, with a rule of substitution for predicate letters; over and above this it has three axioms for the ancestral and two for the ordered pair.


1953 ◽  
Vol 18 (1) ◽  
pp. 49-59 ◽  
Author(s):  
Hao Wang

It is known that we can introduce in number theory (for example, the system Z of Hilbert-Bernays) by induction schemata certain predicates of natural numbers which cannot be expressed explicitly within the framework of number theory. The question arises how we can define these predicates in some richer system, without employing induction schemata. In this paper a general notion of definability by induction (relative to number theory), which seems to apply to all the known predicates of this kind, is introduced; and it is proved that in a system L1 which forms an extension of number theory all predicates which are definable by induction (hereafter to be abbreviated d.i.) according to the definition are explicitly expressible.In order to define such predicates and prove theorems answering to their induction schemata, we have to allow certain impredicative classes in L1. However, if we want merely to prove that for each constant number the special case of the induction schema for a predicate d.i. is provable, we do not have to assume the existence of impredicative classes. A certain weaker system L2, in which only predicative classes of natural numbers are allowed, is sufficient for the purpose. It is noted that a truth definition for number theory can be obtained in L2. Consistency proofs for number theory do not seem to be formalizable in L2, although they can, it is observed, be formalized in L1.In general, given any ordinary formal system (say Zermelo set theory), it is possible to define by induction schemata, in the same manner as in number theory, certain predicates which are not explicitly definable in the system. Here again, by extending the system in an analogous fashion, these predicates become expressible in the resulting system. The crucial predicate instrumental to obtaining a truth definition for a given system is taken as an example.


1973 ◽  
Vol 38 (2) ◽  
pp. 232-248 ◽  
Author(s):  
Philip T. Shepard

In this paper I shall argue that the presumption of infinitude may be excised from the area of mathematics known as natural number theory with no substantial loss. Except for a few concluding remarks, I shall restrict my concern in here arguing the thesis to the business of constructing and developing a first-order axiomatic system for arithmetic (called ‘FA’ for finite arithmetic) that contains no theorem to the effect that there are infinitely many numbers.The paper will consist of five parts. Part I characterizes the underlying logic of FA. In part II ordering of natural numbers is developed from a restricted set of axioms, induction schemata are proved and a way of expressing finitude presented. A full set of axioms are used in part III to prove working theorems on comparison of size. In part IV an ordinal expression is defined and characteristic theorems proved. Theorems for addition and multiplication are derived in part V from definitions in terms of the ordinal expression of part IV. The crucial final constructions of part V present a new method of replacing recursive characterizations by strict definitions.In view of our resolution not to assume that there are infinitely many numbers, we shall have to deal with the situation where singular arithmetic terms of FA may fail to refer. For I know of no acceptable and systematic way of avoiding such situations. As a further result, singular-term instances of universal generalizations of FA are not to be inferred directly from the generalizations themselves. Nevertheless, (i) (x)(y)(x + y = y + x), for example, and all its instances are provable in FA.


Author(s):  
B.Mahaboob, Et. al.

The generalization of sum of integral powers of first n-natural numbers has been an interesting problem among the researchers in Analytical Number Theory for decades. This research article mainly focuses on the derivation of generalized result of this sum. More explicit formula has been derived in order to get the sum of any arbitrary integral powers of first n-natural numbers. Furthermore by using the fundamental principles of Combinatorics and Linear Algebra an attempt has been made to answer an interesting question namely: Is the sum of integral powers of natural numbers a unique polynomial? As a result it is depicted that this sum always equals a unique polynomial over natural numbers. Moreover some properties of the coefficients of this polynomial are derived.More importantly a recurrence relation which can give the formulas for sum of any positive integral powers of first n-natural numbers has been proposed and it is strongly believed that this recurrence relation is the most significant thing in this entire discussion


Author(s):  
Zurab Agdgomelashvili ◽  

The article considers the following issues: – It’s of great interest for p and q primes to determine the number of those prime number divisors of a number 1 1 pq A p    that are less than p. With this purpose we have considered: Theorem 1. Let’s p and q are odd prime numbers and p  2q 1. Then from various individual divisors of the 1 1 pq A p    number, only one of them is less than p. A has at least two different simple divisors; Theorem 2. Let’s p and q are odd prime numbers and p  2q 1. Then all prime divisors of the number 1 1 pq A p    are greater than p; Theorem 3. Let’s q is an odd prime number, and p N \{1}, p]1;q] [q  2; 2q] , then each of the different prime divisors of the number 1 1 pq A p    taken separately is greater than p; Theorem 4. Let’s q is an odd prime number, and p{q1; 2q1}, then from different prime divisors of the number 1 1 pq A p    taken separately, only one of them is less than p. A has at least two different simple divisors. Task 1. Solve the equation 1 2 1 z x y y    in the natural numbers x , y, z. In addition, y must be a prime number. Task 2. Solve the equation 1 3 1 z x y y    in the natural numbers x , y, z. In addition, y must be a prime number. Task 3. Solve the equation 1 1 z x y p y    where p{6; 7; 11; 13;} are the prime numbers, x, y  N and y is a prime number. There is a lema with which the problem class can be easily solved: Lemma ●. Let’s a, b, nN and (a,b) 1. Let’s prove that if an  0 (mod| ab|) , or bn  0 (mod| ab|) , then | ab|1. Let’s solve the equations ( – ) in natural x , y numbers: I. 2 z x y z z x y          ; VI. (x  y)xy  x y ; II. (x  y)z  (2x)z  yz ; VII. (x  y)xy  yx ; III. (x  y)z  (3x)z  yz ; VIII. (x  y) y  (x  y)x , (x  y) ; IV. ( y  x)x y  x y , (y  x) ; IX. (x  y)x y  xxy ; V. ( y  x)x y  yx , (y  x) ; X. (x  y)xy  (x  y)x , (y  x) . Theorem . If a, bN (a,b) 1, then each of the divisors (a2  ab  b2 ) will be similar. The concept of pseudofibonacci numbers is introduced and some of their properties are found.


Sign in / Sign up

Export Citation Format

Share Document