The λ-calculus is ω-incomplete

1974 ◽  
Vol 39 (2) ◽  
pp. 313-317 ◽  
Author(s):  
G. D. Plotkin
Keyword(s):  
The Other ◽  
Free Variables ◽  
Syntactic Identity ◽  
Image Position

The ω-rule in the λ-calculus (or, more exactly, the λK-β, η calculus) isIn [1] it was shown that this rule is consistent with the other rules of the λ-calculus. We will show the rule cannot be derived from the other rules; that is, we will give closed terms M and N such that MZ = NZ can be proved without using the ω-rule, for each closed term Z, but M = N cannot be so proved. This strengthens a result in [4] and answers a question of Barendregt.The language of the λ-calculus has an alphabet containing denumerably many variables a, b, c, … (which have a standard listing e1, e2, …), improper symbolsλ, ( , ) and a single predicate symbol = for equality.Terms are defined inductively by the following:(1) A variable is a term.(2) If M and N are terms, so is (MN); it is called a combination.(3) If M is a term and x is a variable, (λx M) is a term; it is called an abstraction.We use ≡ for syntactic identity of terms.If M and N are terms, M = N is a formula.BV(M), the set of bound variables in M, and FV(M), its free variables, are defined inductively byA term M is closed iff FV(M) = ∅.

Arithmetic with creative definitions by induction

1953 ◽  
Vol 18 (2) ◽  
pp. 115-118 ◽  
Author(s):  
John Myhill
Keyword(s):  
Functional Calculus ◽  
The Other ◽  
Central Feature ◽  
Natural Numbers ◽  
Free Variables ◽  
Image Position

The purpose of this paper is to present a system of arithmetic stronger than those usually employed, and to prove some syntactical theorems concerning it.We presuppose the lower functional calculus with identity and functions, and we start with three of Peano's axioms.The other two (0 ϵ N and x ϵ N .⊃. x′ ϵ N) we do not need since our variables are anyhow restricted to natural numbers. Sometimes in the interest of a uniform notation for functions, we write Sx instead of x′.Next we have two axioms for μ (the smallest number such that) as follows.A third axiom for μ must wait until we have defined ≤.Now we introduce the central feature of the system, the following rule of definition.RD. Let Φ be a previously unused symbol. Then we can introduce it by a pair of definitions of the following form (n ≥ 0),where F(x1, …, xn) is a wff in which no symbol occurs which was not previously defined (in particular, not Φ), and in which no free variables occur other than x1, …, xn (and possibly not all of these), and G(x1, …, xn, y) is a wff in which no free variables occur other than x1, …, xn, y (and possibly not all of these), and in which no symbol occurs which was not previously defined, except that Φ may occur but only if its last argument is y.

Term models for weak set theories with a universal set

1987 ◽  
Vol 52 (2) ◽  
pp. 374-387 ◽  
Author(s):  
T. E. Forster
Keyword(s):  
Boolean Algebra ◽  
Set Theory ◽  
Axiom Of Choice ◽  
The Other ◽  
Free Variables ◽  
Image Position ◽  
The Axiom Of Choice ◽  
Axiomatic Systems ◽  
The Universe

We shall be concerned here with weak axiomatic systems of set theory with a universal set. The language in which they are expressed is that of set theory—two primitive predicates, = and ϵ, and no function symbols (though some function symbols will be introduced by definitional abbreviation). All the theories will have stratified axioms only, and they will all have Ext (extensionality: (∀x)(∀y)(x = y· ↔ ·(∀z)(z ϵ x ↔ z ϵ y))). In fact, in addition to extensionality, they have only axioms saying that the universe is closed under certain set-theoretic operations, viz. all of the formand these will always include singleton, i.e., ι′x exists if x does (the iota notation for singleton, due to Russell and Whitehead, is used here to avoid confusion with {x: Φ}, set abstraction), and also x ∪ y, x ∩ y and − x (the complement of x). The system with these axioms is called NF2 in the literature (see [F]). The other axioms we consider will be those giving ⋃x, ⋂x, {y: y ⊆x} and {y: x ⊆ y}. We will frequently have occasion to bear in mind that 〈 V, ⊆ 〉 is a Boolean algebra in any theory extending NF2. There is no use of the axiom of choice at any point in this paper. Since the systems with which we will be concerned exhibit this feature of having, in addition to extensionality, only axioms stating that V is closed under certain operations, we will be very interested in terms of the theories in question. A T-term, for T such a theory, is a thing (with no free variables) built up from V or ∧ by means of the T-operations, which are of course the operations that the axioms of T say the universe is closed under.

On derivability

1937 ◽  
Vol 2 (3) ◽  
pp. 113-119 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Formal System ◽  
Free Variable ◽  
The Other ◽  
Free Variables ◽  
Image Position ◽  
Positive Integers

1. The notion of derivability. Italic capitals, with or without subscripts, will be used as variables. They are to take as values some manner of elements which may for the present be left undetermined. Now let us consider abstractly the notion of the derivability of an element X from one or more specified elements by a series of steps of a specified kind. This involves reference to two conditions upon elements. One of these conditions, expressible by some statement form containing a single free variable, determines the elements from which X is said to be derivable. The other condition, expressed say by a statement form containing k + 1 free variables, determines the kind of steps by which the derivation is to proceed; it is the condition which any elements Z1, … Zk, Y must fulfill if progress from Zi, …, Zk to Y is to constitute a step of derivation in the intended sense. Supposing “f(Y)” supplanted by the first of these statement forms, whatever it may be, and “g(Z1, …, Zk, Y)” supplanted by the other, let us adopt the form of notationto express derivability of X in the suggested sense. The meaning of (1) can be formulated more accurately as follows:(i) There are elements Y1 to Ym (for some m) such that Ym = X and, for each i≦m, either f(Yi) or else there are numbers j1 to Ym, each less than i, for which g(Yj1, …, Yjk, Yi).(Variable subscripts are to be understood, here and throughout the paper, as referring only to positive integers.)The notion (1) is illustrated in the ancestral R* of a relation R;1 for,Another illustration is afforded by metamathematics. Suppose our elements are the expressions used in some formal system; suppose we have defined “Post(Y)”, meaning that Y is a postulate of that system; and suppose we have defined “Inf(ZI, …, Zk, Y)” (for some fixed k large enough for all purposes of the system in question), meaning that Y proceeds from Z1, …, Zk by one application of one or another of the rules of inference of the system. Thenwould mean that X is a theorem of the system.

scholarly journals The Dissociation of the Compound of Iodine and Thio-urea

1904 ◽  
Vol 24 ◽  
pp. 233-239 ◽  
Author(s):  
Hugh Marshall
Keyword(s):  
Nitric Acid ◽  
General Formula ◽  
Free Acid ◽  
The Other ◽  
Image Position

When thio-urea is treated with suitable oxidising agents in presence of acids, salts are formed corresponding to the general formula (CSN2H4)2X2:—Of these salts the di-nitrate is very sparingly soluble, and is precipitated on the addition of nitric acid or a nitrate to solutions of the other salts. The salts, as a class, are not very stable, and their solutions decompose, especially on warming, with formation of sulphur, thio-urea, cyanamide, and free acid. A corresponding decomposition results immediately on the addition of alkali, and this constitutes a very characteristic reaction for these salts.

Extremely undecidable sentences

1982 ◽  
Vol 47 (1) ◽  
pp. 191-196 ◽  
Author(s):  
George Boolos
Keyword(s):  
Modal Logic ◽  
The Other ◽  
Propositional Modal Logic ◽  
Image Position

Let ‘ϕ’, ‘χ’, and ‘ψ’ be variables ranging over functions from the sentence letters P0, P1, … Pn, … of (propositional) modal logic to sentences of P(eano) Arithmetic), and for each sentence A of modal logic, inductively define Aϕ by[and similarly for other nonmodal propositional connectives]; andwhere Bew(x) is the standard provability predicate for PA and ⌈F⌉ is the PA numeral for the Gödel number of the formula F of PA. Then for any ϕ, (−□⊥)ϕ = −Bew(⌈⊥⌉), which is the consistency assertion for PA; a sentence S is undecidable in PA iff both and , where ϕ(p0) = S. If ψ(p0) is the undecidable sentence constructed by Gödel, then ⊬PA (−□⊥→ −□p0 & − □ − p0)ψ and ⊢PA(P0 ↔ −□⊥)ψ. However, if ψ(p0) is the undecidable sentence constructed by Rosser, then the situation is the other way around: ⊬PA(P0 ↔ −□⊥)ψ and ⊢PA (−□⊥→ −□−p0 & −□−p0)ψ. We call a sentence S of PA extremely undecidable if for all modal sentences A containing no sentence letter other than p0, if for some ψ, ⊬PAAψ, then ⊬PAAϕ, where ϕ(p0) = S. (So, roughly speaking, a sentence is extremely undecidable if it can be proved to have only those modal-logically characterizable properties that every sentence can be proved to have.) Thus extremely undecidable sentences are undecidable, but neither the Godel nor the Rosser sentence is extremely undecidable. It will follow at once from the main theorem of this paper that there are infinitely many inequivalent extremely undecidable sentences.

On functional Nörlund methods

1970 ◽  
Vol 67 (1) ◽  
pp. 47-60 ◽  
Author(s):  
B. Choudhary
Keyword(s):  
The Other ◽  
Integral Transformations ◽  
Other Hand ◽  
Nörlund Means ◽  
The One ◽  
Image Position

Integral transformations analogous to the Nörlund means have been introduced and investigated by Kuttner, Knopp and Vanderburg(6), (5), (4). It is known that with any regular Nörlund mean (N, p) there is associated a functionregular for |z| < 1, and if we have two Nörlund means (N, p) and (N, r), where (N, pr is regular, while the function is regular for |z| ≤ 1 and different) from zero at z = 1, then q(z) = r(z)p(z) belongs to a regular Nörlund mean (N, q). Concerning Nörlund means Peyerimhoff(7) and Miesner (3) have recently obtained the relation between the convergence fields of the Nörlund means (N, p) and (N, r) on the one hand and the convergence field of the Nörlund mean (N, q) on the other hand.

scholarly journals Distribution of rational points on the real line

1973 ◽  
Vol 15 (2) ◽  
pp. 243-256 ◽  
Author(s):  
T. K. Sheng
Keyword(s):  
Algebraic Number ◽  
Rational Number ◽  
Real Line ◽  
Rational Points ◽  
The Other ◽  
Liouville Numbers ◽  
The Real ◽  
Other Hand ◽  
Image Position

It is well known that no rational number is approximable to order higher than 1. Roth [3] showed that an algebraic number is not approximable to order greater than 2. On the other hand it is easy to construct numbers, the Liouville numbers, which are approximable to any order (see [2], p. 162). We are led to the question, “Let Nn(α, β) denote the number of distinct rational points with denominators ≦ n contained in an interval (α, β). What is the behaviour of Nn(α, + 1/n) as α varies on the real line?” We shall prove that and that there are “compressions” and “rarefactions” of rational points on the real line.

3. Laboratory Notes by Professor Tait (a.) Measurement of the Potential, required to produce Sparks of various lengths, in Air at different pressures, by a Holtz Machine

1878 ◽  
Vol 9 ◽  
pp. 332-333
Author(s):  
Messrs Macfarlane ◽  
Paton
Keyword(s):  
General Result ◽  
The Other ◽  
Considerable Distance ◽  
Image Position

The general result of these strictly preliminary experiments appears to show that for sparks not exceeding a decimetre in length (L), taken in air at different pressures (P), between two metal balls of 7mm·5 radius, the requisite potential (V), is expressed by the formulaThe Holtz machine employed is a double one, made by Ruhmkorff, and it was used with its small Leyden jars attached. The measurements had to be made with a divided-ring electrometer, so that two insulated balls, at a considerable distance from one another, were connected, one with the machine, the other with the electrometer.

scholarly journals Certain Mathematical Instruments for Graphically Indicating the Direction of Refracted and Reflected Light Rays

1906 ◽  
Vol 25 (2) ◽  
pp. 806-812
Author(s):  
J.R. Milne
Keyword(s):  
Optical System ◽  
The Other ◽  
Reflected Light ◽  
Light Rays ◽  
Image Position

The refraction equation sin i == μ sin r, though simple in itself, is apt to give rise, in problems connected with refraction, to formulæ too involved for arithmetical computation. In such cases it may be necessary to trace the course through the optical system in question of a certain number of arbitrarily chosen rays, and thence to find the course of the other rays by interpolation. Thelinkage about to be described affords a rapid and accurate means of determining the paths of the rays through any optical system.

Note on a Theorem regarding a Series of Convergents to the Roots of a Number

1893 ◽  
Vol 19 ◽  
pp. 15-19
Author(s):  
Thomas Muir
Keyword(s):  
The Other ◽  
Image Position

If the positive integral powers of be taken, and the expansion of each be separated into two parts, rational and irrational, thus—then the ratio of the rational portion to the coefficient of in the other portion is approximately equal to , the convergence being perfect when the power of the binomial is infinite. This is the simplest case of a theorem discovered by the late Dr Sang, and enunciated by him as the result of a process of induction in his paper “On the Extension of Brouncker's Method to the Comparison of several Magnitudes” (Proc. Roy. Soc. Edin., vol. xviii. p. 341, 1890–91).

Sign in / Sign up

Export Citation Format

Share Document