A theorem on deducibility for second-order functions

1939 ◽  
Vol 4 (2) ◽  
pp. 77-79 ◽  
Author(s):  
C. H. Langford
Keyword(s):  
Second Order ◽  
Order Function ◽  
Usual Definition ◽  
First Order ◽  
Free Variables ◽  
Usual Convention ◽  
Definition Of ◽  
Image Position

It is known that the usual definition of a dense series without extreme elements is complete with respect to first-order functions, in the sense that any first-order function on the base of a set of postulates defining such a series either is implied by the postulates or is inconsistent with them. It is here understood, in accordance with the usual convention, that when we speak of a function on the base , the function shall be such as to place restrictions only upon elements belonging to the class determined by f; or, more exactly, every variable with a universal prefix shall occur under the hypothesis that its values satisfy f, while every variable with an existential prefix shall have this condition categorically imposed upon it.Consider a set of postulates defining a dense series without extreme elements, and add to this set the condition of Dedekind section, to be formulated as follows. Let the conjunction of the three functions,be written H(ϕ), where the free variables f and g, being parameters throughout, are suppressed. This is the hypothesis of Dedekind's condition, and the conclusion iswhich may be written C(ϕ).

The double function of the interpretant in Peirce’s theory of signs

Semiotica ◽  
2018 ◽  
Vol 2018 (225) ◽  
pp. 39-55
Author(s):  
Jimmy Aames
Keyword(s):  
Second Order ◽  
The Other ◽  
Logical Operation ◽  
Order Function ◽  
First Order ◽  
Formal Identity ◽  
Double Function ◽  
Hypostatic Abstraction ◽  
The One ◽  
Definition Of

AbstractThere seem to be two distinct aspects to the role played by the Interpretant in Peirce’s account of the sign relation. On the one hand, the Interpretant is said to establish the relation between the Sign and Object. That is, the Sign can “stand for” its Object, and thereby actually function as a Sign, only by virtue of its being interpreted as such by an Interpretant. On the other hand, the Interpretant is said to be “determined” by the Sign in such a way that it is thereby mediately determined by the Sign’s Object. How can we understand the relation between these two aspects of the Interpretant? This is the question with which this paper is concerned. I begin by drawing a distinction between what I call the first-order function and second-order function of the Interpretant, and illustrating this distinction using Peirce’s example of comparing the letters p and b in § 9 of the 1867 “On a New List of Categories.” I then show that this same distinction can be discerned in a significant passage in the second section of Peirce’s 1903 “A Syllabus of Certain Topics of Logic,” as well as in his early definition of the Interpretant in the “New List.” This double function of the Interpretant has been noted in the Peircean literature, specifically by Joseph Ransdell in his 1966 dissertation, and more recently by André De Tienne. However, an important aspect of what I call the second-order function of the Interpretant remains unclarified in Ransdell and De Tienne’s approaches, namely, its relation to the logical operation of hypostatic abstraction. I will show that the Interpretant, in its second-order function, plays a role formally identical in the sign process to the role played by hypostatic abstraction in Peirce’s demonstrations of the Reduction Thesis. This formal identity will afford us with a way of understanding the relation between the two aspects of the Interpretant in terms of hypostatic abstraction.

Abstraction Logic

2021 ◽  
Author(s):  
Steven Obua
Keyword(s):  
Binding Constants ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Algebraic Semantics ◽  
Variable Binding ◽  
First Order ◽  
Free Variables ◽  
Direct Support ◽  
Second Order Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.

The diversity of quantifier prefixes

1973 ◽  
Vol 38 (1) ◽  
pp. 79-85 ◽  
Author(s):  
H. Jerome Keisler ◽  
Wilbur Walkoe
Keyword(s):  
Positive Integer ◽  
Analogous Result ◽  
Predicate Logic ◽  
Finite Sequence ◽  
Arithmetical Hierarchy ◽  
First Order ◽  
Free Variables ◽  
The Standard Model ◽  
Image Position ◽  
Identity Symbol

The Arithmetical Hierarchy Theorem of Kleene [1] states that in the complete theory of the standard model of arithmetic there is for each positive integer r a Σr0 formula which is not equivalent to any Πr0 formula, and a Πr0 formula which is not equivalent to any Πr0 formula. A Πr0 formula is a formula of the formwhere φ has only bounded quantifiers; Πr0 formulas are defined dually.The Linear Prefix Theorem in [3] is an analogous result for predicate logic. Consider the first order predicate logic L with identity symbol, countably many n-placed relation symbols for each n, and no constant or function symbols. A prefix is a finite sequenceof quantifier symbols ∃ and ∀, for example ∀∃∀∀∀∃. By a Q formula we mean a formula of L of the formwhere v1, …, vr are distinct variables and φ has no quantifiers. A sentence is a formula with no free variables. The Linear Prefix Theorem is as follows.Linear Prefix Theorem. Let Q and q be two different prefixes of the same length r. Then there is a Q sentence which is not logically equivalent to any q sentence.Moreover, for each s there is a Q formula with s free variables which is not logically equivalent to any q formula with s free variables.For example, there is an ∀∃∀∀∀∃ sentence which is not logically equivalent to any ∀∃∃∀∀∃ sentence, and vice versa. Recall that in arithmetic two consecutive ∃'s or ∀'s can be collapsed; for instance all ∀∃∀∀∀∃ and ∀∃∃∀∀∃ formulas are logically equivalent to Π40 formulas. But the Linear Prefix Theorem shows that in predicate logic the number of quantifiers in each block, as well as the number of blocks, counts.

Development of the female flower and gynecandrous partial inflorescence of Myrica californica

1979 ◽  
Vol 57 (2) ◽  
pp. 141-151 ◽  
Author(s):  
Alastair D. Macdonald
Keyword(s):  
Fourth Order ◽  
Female Flower ◽  
Second Order ◽  
Third Order ◽  
First Order ◽  
Unique Structure ◽  
Inflorescence Axis ◽  
Definition Of ◽  
Fifth Order ◽  
Partial Inflorescence

Organogenesis of the female flower and gynecandrous partial inflorescence is described. Approximately 25 first-order inflorescence bracts are formed in an acropetal sequence. A second-order inflorescence axis, the partial inflorescence, develops in the axil of each bract. Third-, fourth-, and fifth-order axes arise in the axils of second-, third-, and fourth-order bracts. A gynoecium terminates a second-order axis and sometimes a distal third-order axis. A gynoecium consists of two stigmas and one basal, unitegmic, orthotropous ovule. The wall enclosing the ovule, the circumlocular wall, is comprised distally of gynoecial tissue and proximally of tissue of the inflorescence axis and its appendages. The latter portion of the wall is formed by zonal growth. Androecial members, formed proximal to the gynoecium on the partial inflorescence, are carried onto the circumlocular wall by zonal growth. A stamen may develop from the last-formed primordium before gynoecial inception or from a potentially stigmatic primordium. The papillae of the flower and fruit arise as emergences and from potentially bracteate, axial, and staminate primorida during the development of the circumlocular wall. The term circumlocular wall is used in a neutral sense to describe this unique structure. Since the gynoecium is composed of gynoecial appendages and inflorescence axis and appendages, a functional definition of gynoecium must be expanded to include any tissue, including an inflorescence, that surrounds the ovule(s) and forms the fruit(s).

The McKinsey axiom is not canonical

1991 ◽  
Vol 56 (2) ◽  
pp. 554-562 ◽  
Author(s):  
Robert Goldblatt
Keyword(s):  
Relational Semantics ◽  
Binary Relations ◽  
Order Condition ◽  
Modal Formula ◽  
First Order ◽  
Canonical Frame ◽  
Historical Importance ◽  
Definition Of ◽  
Image Position ◽  
Normal Modal Logics

The logic KM is the smallest normal modal logic that includes the McKinsey axiomIt is shown here that this axiom is not valid in the canonical frame for KM, answering a question first posed in the Lemmon-Scott manuscript [Lemmon, 1966].The result is not just an esoteric counterexample: apart from interest generated by the long delay in a solution being found, the problem has been of historical importance in the development of our understanding of intensional model theory, and is of some conceptual significance, as will now be explained.The relational semantics for normal modal logics first appeared in [Kripke, 1963], where a number of well-known systems were shown to be characterised by simple first-order conditions on binary relations (frames). This phenomenon was systematically investigated in [Lemmon, 1966], which introduced the technique of associating with each logic L a canonical frame which invalidates every nontheorem of L. If, in addition, each L-theorem is valid in , then L is said to be canonical. The problem of showing that L is determined by some validating condition C, meaning that the L-theorems are precisely those formulae valid in all frames satisfying C, can be solved by showing that satisfies C—in which case canonicity is also established. Numerous cases were studied, leading to the definition of a first-order condition Cφ associated with each formula φ of the formwhere Ψ is a positive modal formula.

An intuitionistically plausible interpretation of intuitionistic logic

1977 ◽  
Vol 42 (4) ◽  
pp. 564-578 ◽  
Author(s):  
H. C. M. de Swart
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Calculus ◽  
Mathematical Treatment ◽  
First Order ◽  
The Past ◽  
Definition Of ◽  
Image Position ◽  
Order Predicate Calculus ◽  
Made In

Let IPC be the intuitionistic first-order predicate calculus. From the definition of derivability in IPC the following is clear:(1) If A is derivable in IPC, denoted by “⊦IPCA”, then A is intuitively true, that means, true according to the intuitionistic interpretation of the logical symbols. To be able to settle the converse question: “if A is intuitively true, then ⊦IPCA”, one should make the notion of intuitionistic truth more easily amenable to mathematical treatment. So we have to look then for a definition of “A is valid”, denoted by “⊨A”, such that the following holds:(2) If A is intuitively true, then ⊨ A.Then one might hope to be able to prove(3) If ⊨ A, then ⊦IPCA.If one would succeed in finding a notion of “⊨ A”, such that all the conditions (1), (2) and (3) are satisfied, then the chain would be closed, i.e. all the arrows in the scheme below would hold.Several suggestions for ⊨ A have been made in the past: Topological and algebraic interpretations, see Rasiowa and Sikorski [1]; the intuitionistic models of Beth, see [2] and [3]; the interpretation of Grzegorczyk, see [4] and [5]; the models of Kripke, see [6] and [7]. In Thirty years of foundational studies, A. Mostowski [8] gives a review of the interpretations, proposed for intuitionistic logic, on pp. 90–98.

On an Ackermann-type set theory

1973 ◽  
Vol 38 (3) ◽  
pp. 410-412
Author(s):  
John Lake
Keyword(s):  
Set Theory ◽  
Measurable Cardinal ◽  
Large Cardinal ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Individual Constant ◽  
Image Position ◽  
Order Predicate Calculus ◽  
Universal Closure

Ackermann's set theory A* is usually formulated in the first order predicate calculus with identity, ∈ for membership and V, an individual constant, for the class of all sets. We use small Greek letters to represent formulae which do not contain V and large Greek letters to represent any formulae. The axioms of A* are the universal closures ofwhere all free variables are shown in A4 and z does not occur in the Θ of A2.A+ is a generalisation of A* which Reinhardt introduced in [3] as an attempt to provide an elaboration of Ackermann's idea of “sharply delimited” collections. The language of A+ is that of A*'s augmented by a new constant V′, and its axioms are A1–A3, A5, V ⊆ V′ and the universal closure ofwhere all free variables are shown.Using a schema of indescribability, Reinhardt states in [3] that if ZF + ‘there exists a measurable cardinal’ is consistent then so is A+, and using [4] this result can be improved to a weaker large cardinal axiom. It seemed plausible that A+ was stronger than ZF, but our main result, which is contained in Theorem 5, shows that if ZF is consistent then so is A+, giving an improvement on the above results.

Arithmetic and the theory of types

1984 ◽  
Vol 49 (2) ◽  
pp. 621-624 ◽  
Author(s):  
M. Boffa
Keyword(s):  
Peano Arithmetic ◽  
Positive Answer ◽  
Second Order ◽  
Countable Model ◽  
Natural Numbers ◽  
Conservative Extension ◽  
Logical Definition ◽  
Claude Bernard ◽  
Definition Of ◽  
Image Position

A hundred years ago, Frege proposed a logical definition of the natural numbers based on the following idea:He replaced this circular definition by the following one:He tried afterwards to found his theory over a notion of class satisfying a general comprehension principle:Russell quickly derived a contradiction from this principle (the famous Russell's paradox) but saved Frege's arithmetic with his theory of types based on the following comprehension principle:In 1979, talking at the Claude Bernard University in Lyon, I remarked that 3 types suffice to provide Frege's arithmetic, showing in fact that PA2 (second order Peano arithmetic) holds in TT3 + AI (theory of types 0, 1, 2 plus a suitable axiom of infinity). I asked whether TT3 + AI was a conservative extension of PA2. Pabion [3] gave a positive answer by a subtle use of the Fraenkel-Moskowski method. This result will be improved in the present paper, with a view to getting models of NF3 + AI in which Frege's arithmetic forms a model isomorphic to a given countable model of PA2.

Generalized interpolation theorems

1972 ◽  
Vol 37 (2) ◽  
pp. 343-351
Author(s):  
Stephen J. Garland
Keyword(s):  
Interpolation Theorem ◽  
Second Order ◽  
Cut Elimination ◽  
Real Numbers ◽  
Craig Interpolation ◽  
First Order ◽  
Order Variable ◽  
Analytic Sets ◽  
Image Position ◽  
Special Case

Chang [1], [2] has proved the following generalization of the Craig interpolation theorem [3]: For any first-order formulas φ and ψ with free first- and second-order variables among ν1, …, νn, R and ν1, …, νn, S respectively, and for any sequence Q1, …, Qn of quantifiers such that Q1 is universal whenever ν1 is a second-order variable, ifthen there is a first-order formula θ with free variables among ν1, …, νn such that(Note that the Craig interpolation theorem is the special case of Chang's theorem in which Q1, …, Qn are all universal quantifiers.) Chang also raised the question [2, Remark (k)] as to whether the Lopez-Escobar interpolation theorem [6] for the infinitary language Lω1ω possesses a similar generalization. In this paper, we show that the answer to Chang's question is affirmative and, moreover, that several interpolation theorems for applied second-order languages for number theory also possess such generalizations.Maehara and Takeuti [7] have established independently proof-theoretic interpolation theorems for first-order logic and Lω1ω which have as corollaries both Chang's theorem and its analog for Lω1ω. Our proofs are quite different from theirs and rely on model-theoretic techniques stemming from the analogy between the theory of definability in Lω1ω and the theory of Borel and analytic sets of real numbers, rather than the technique of cut-elimination.

Generalizing generalized tries

2000 ◽  
Vol 10 (4) ◽  
pp. 327-351 ◽  
Author(s):  
RALF HINZE
Keyword(s):  
Type System ◽  
Search Tree ◽  
Second Order ◽  
First Order ◽  
Programming Paradigm ◽  
Arbitrary Signature ◽  
One Step ◽  
Rank 2 ◽  
Definition Of

A trie is a search tree scheme that employs the structure of search keys to organize information. Tries were originally devised as a means to represent a collection of records indexed by strings over a fixed alphabet. Based on work by C. P. Wadsworth and others, R. H. Connelly and F. L. Morris generalized the concept to permit indexing by elements built according to an arbitrary signature. Here we go one step further, and define tries and operations on tries generically for arbitrary datatypes of first-order kind, including parameterized and nested datatypes. The derivation employs techniques recently developed in the context of polytypic programming and can be regarded as a comprehensive case study in this new programming paradigm. It is well known that for the implementation of generalized tries, nested datatypes and polymorphic recursion are needed. Implementing tries for first-order kinded datatypes places even greater demands on the type system: it requires rank-2 type signatures and second-order nested datatypes. Despite these requirements, the definition of tries is surprisingly simple, which is mostly due to the framework of polytypic programming.

Sign in / Sign up

Export Citation Format

Share Document