A finitary metalanguage for extended basic logic

1952 ◽  
Vol 17 (3) ◽  
pp. 164-178 ◽  
Author(s):  
John Myhill

In a series of five papers, Fitch has constructed a system of combinatory logic K′ which is adequate for much of classical analysis, and is demonstrably consistent if we assume the validity of transfinite induction up to a certain ordinal (at present undetermined). The system has the following peculiarities:1.1. It is non-finitary, i.e. the class of Gödel-numbers of its theorems does not form the range of values of any recursive function (nor, as a matter of fact, of any function definable in elementary number theory).1.2. It does not permit quantification over real numbers; i.e. it contains no theorems of the form1.3. Because of 1.1, we cannot, except in trivial cases, construct actual proofs in K′; we have to resort to a metalanguage (of undetermined strength) in order to show that certain formulae are theorems of K′. Also because of 1.2, many important theorems of classical mathematics are not forthcoming in K′ itself, but only in the aforementioned metalanguage, e.g. in the formwhere ‘x’ is a syntactical rather than a numerical variable, a U-real is an expression of K′ rather than a number, and ‘ … x– – –’ ascribes a syntactical rather than a real number-theoretic property to x.The purpose of this paper is to construct a finitary metalanguage for K′ in which all of Fitch's important theorems may be proved.

1950 ◽  
Vol 15 (3) ◽  
pp. 185-196 ◽  
Author(s):  
John R. Myhill

The purpose of the present paper is to construct a fragment of number theory not subject to Gödel incompletability. Originally the system was designed as a metalanguage for classical mathematics (see section 10); but it now appears to the author worthwhile to present it as a mathematical system in its own right, to serve however rather as an instrument of computation than of proof. Its resources in the latter respect seem very extensive, sufficient apparently for the systematic tabulation of every function used in any but the most recondite physics. The author intends to pursue this topic in a later paper; the present one will simply present the system, along with proofs of consistency and completeness and a few metatheorems which will be used as lemmas for future research.Completeness is achieved by sacrificing the notions of negation and universal quantification customary in number-theoretic systems; the losses consequent upon this are made good in part by the use of the ancestral as a primitive idea. The general outlines of the system follow closely the pattern of Fitch's “basic logic”; however the latter system uses combinatory operators in place of the variables used in the present paper, and if variables are introduced into Fitch's system by definition their range of values will be found to be much more extensive than that of my variables. The present system K is thus a weaker form of Fitch's system.It is apparently not known whether or not Fitch's system is complete.


1961 ◽  
Vol 57 (4) ◽  
pp. 759-766
Author(s):  
A. S. Besicovitch

Given † probability vector μ(X) = (μ1(X), … μk (X)) of a finite number of components on a Borel class of sets X, we say that μ(X0) has a diagonal value α if μi(X0) = α for all i = 1, 2,…,K. J. Neyman(l), (2), (3) has proved that in the class of Borel sets of real numbers any non-atomic vector μ(X) takes all diagonal values. A. Liapounoff has studied the full range of values of k-dimensional vector-valued measures and in two papers (4) he has proved that the range is closed and in the case of non-atomic measures the range is also convex. He also gave an example showing that neither of these results holds in the case of vectors of infinitely many components. A simplified proof of Liapounoff's results has been given by P. R. Halmos (5). In the present paper I study the range of values of probability vectors of infinitely many components. Various types of conditions are studied which are sufficient to imply that, for each ε > 0, 0 ≤ α ≤ 1, it is possible to find a set X such that


1969 ◽  
Vol 6 (03) ◽  
pp. 478-492 ◽  
Author(s):  
William E. Wilkinson

Consider a discrete time Markov chain {Zn } whose state space is the non-negative integers and whose transition probability matrix ║Pij ║ possesses the representation where {Pr }, r = 1,2,…, is a finite or denumerably infinite sequence of non-negative real numbers satisfying , and , is a corresponding sequence of probability generating functions. It is assumed that Z 0 = k, a finite positive integer.


1955 ◽  
Vol 7 ◽  
pp. 337-346 ◽  
Author(s):  
R. P. Bambah ◽  
K. Rogers

1. Introduction. Several authors have proved theorems of the following type:Let x0, y0 be any real numbers. Then for certain functions f(x, y), there exist numbers x, y such that1.1 x ≡ x0, y ≡ y0 (mod 1),and1.2 .The first result of this type, but with replaced by min , was given by Barnes (3) for the case when the function is an indefinite binary quadratic form. A generalisation of this was proved by elementary geometry by K. Rogers (6).


Author(s):  
James A. Cochran ◽  
Cheng-Shyong Lee
Keyword(s):  

In a 1975 paper [8], Heinig established the following three inequalities:where A = p/(p + s − λ) with p, s, λ real numbers satisfying p + s > λ,p > 0;where B = p/(2p + sp − λ −1) with p, s, λ real numbers satisfying 2p +sp > λ, + 1, p > 0;where is a sequence of nonnegative real numbers,and C = p[l + l/(p + s−λ)] with p, s, λ real numbers satisfying s > 0, p ≥ 1, and p +s > λ 0.


1966 ◽  
Vol 62 (4) ◽  
pp. 637-642 ◽  
Author(s):  
T. W. Cusick

For a real number λ, ‖λ‖ is the absolute value of the difference between λ and the nearest integer. Let X represent the m-tuple (x1, x2, … xm) and letbe any n linear forms in m variables, where the Θij are real numbers. The following is a classical result of Khintchine (1):For all pairs of positive integers m, n there is a positive constant Г(m, n) with the property that for any forms Lj(X) there exist real numbers α1, α2, …, αn such thatfor all integers x1, x2, …, xm not all zero.


1984 ◽  
Vol 49 (1) ◽  
pp. 47-50 ◽  
Author(s):  
Frederic B. Fitch

In [3] a definition of negation was presented for the system K′ of extended basic logic [1], but it has since been shown by Peter Päppinghaus (personal communication) that this definition fails to give rise to the law of double negation as I claimed it did. The purpose of this note is to revise this defective definition in such a way that it clearly does give rise to the law of double negation, as well as to the other negation rules of K′.Although Päppinghaus's original letter to me was dated September 19, 1972, the matter has remained unresolved all this time. Only recently have I seen that there is a simple way to correct the definition. I am of course very grateful to Päppinghaus for pointing out my error in claiming to be able to derive the rule of double negation from the original form of the definition.The corrected definition will, as before, use fixed-point operators to give the effect of the required kind of transfinite induction, but this time a double transfinite induction will be used, somewhat like the double transfinite induction used in [5] to define simultaneously the theorems and antitheorems of system CΓ.


1962 ◽  
Vol 14 ◽  
pp. 597-601 ◽  
Author(s):  
J. Kiefer

The main object of this paper is to prove the following:Theorem. Let f1, … ,fk be linearly independent continuous functions on a compact space. Then for 1 ≤ s ≤ k there exist real numbers aij, 1 ≤ i ≤ s, 1 ≤ j ≤ k, with {aij, 1 ≤ i, j ≤ s} n-singular, and a discrete probability measure ε*on, such that(a) the functions gi = Σj=1kaijfj 1 ≤ i ≤ s, are orthonormal (ε*) to the fj for s < j ≤ k;(b)The result in the case s = k was first proved in (2). The result when s < k, which because of the orthogonality condition of (a) is more general than that when s = k, was proved in (1) under a restriction which will be discussed in § 3. The present proof does not require this ad hoc restriction, and is more direct in approach than the method of (2) (although involving as much technical detail as the latter in the case when the latter applies).


1969 ◽  
Vol 21 ◽  
pp. 1309-1318 ◽  
Author(s):  
James Stewart

Let G be an abelian group, written additively. A complexvalued function ƒ, defined on G, is said to be positive definite if the inequality1holds for every choice of complex numbers C1, …, cn and S1, …, sn in G. It follows directly from (1) that every positive definite function is bounded. Weil (9, p. 122) and Raïkov (5) proved that every continuous positive definite function on a locally compact abelian group is the Fourier-Stieltjes transform of a bounded positive measure, thus generalizing theorems of Herglotz (4) (G = Z, the integers) and Bochner (1) (G = R, the real numbers).If ƒ is a continuous function, then condition (1) is equivalent to the condition that2


1980 ◽  
Vol 32 (5) ◽  
pp. 1045-1057 ◽  
Author(s):  
Patrick J. Browne ◽  
Rodney Nillsen

Throughout this paper we shall use I to denote a given interval, not necessarily bounded, of real numbers and Cn to denote the real valued n times continuously differentiable functions on I and C0 will be abbreviated to C. By a differential operator of order n we shall mean a linear function L:Cn → C of the form1.1where pn(x) ≠ 0 for x ∊ I and pi ∊ Cj 0 ≦ j ≦ n. The function pn is called the leading coefficient of L.It is well known (see, for example, [2, pp. 73-74]) thai a differential operator L of order n uniquely determines both a differential operator L* of order n (the adjoint of L) and a bilinear form [·,·]L (the Lagrange bracket) so that if D denotes differentiation, we have for u, v ∊ Cn,1.2


Sign in / Sign up

Export Citation Format

Share Document