An improved prenex normal form1

1962 ◽  
Vol 27 (3) ◽  
pp. 317-326 ◽  
Author(s):  
C. C. Chang ◽  
H. Jerome Keisler
Keyword(s):  
Positive Integer ◽  
Predicate Logic ◽  
Atomic Formula ◽  
First Order ◽  
Empty String ◽  
Image Position ◽  
First Order Predicate Logic

Let ℒ be the set of all formulas of a given first order predicate logic (with or without identity). For each positive integer n, let ℒn be the set of all formulas φ in ℒ logically equivalent to a formula of the form where Q is a (possibly empty) string of quantifiers, m is a positive integer, and each αij is either an atomic formula or the negation of an atomic formula.

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.

Extensional interpretations of modal logics

1966 ◽  
Vol 31 (1) ◽  
pp. 23-45 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Predicate Logic ◽  
Modal Logics ◽  
Predicate Calculus ◽  
First Order ◽  
Image Position ◽  
Order Predicate Calculus ◽  
First Order Predicate Logic

By ΡL we shall mean the first order predicate logic based on S4. More explicitly: Let Ρ0 stand for the first order predicate calculus. The formalisation of Ρ0 used in the present paper will be given later. ΡL is obtained from Ρ0 by adding the rules the propositional constant □ and

scholarly journals Predicate functors revisited

1981 ◽  
Vol 46 (3) ◽  
pp. 649-652 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Set Theory ◽  
Predicate Logic ◽  
Combinatory Logic ◽  
Homogeneous Case ◽  
Quantification Theory ◽  
Present Scheme ◽  
First Order ◽  
Image Position ◽  
First Order Predicate Logic

Quantification theory, or first-order predicate logic, can be formulated in terms purely of predicate letters and a few predicate functors which attach to predicates to form further predicates. Apart from the predicate letters, which are schematic, there are no variables. On this score the plan is reminiscent of the combinatory logic of Schönfinkel and Curry. Theirs, however, had the whole of higher set theory as its domain; the present scheme stays within the bounds of predicate logic.In 1960 I published an apparatus to this effect, and an improved version in 1971. In both versions I assumed two inversion functors, major and minor; also a cropping functor and the obvious complement functor. The effects of these functors, when applied to an n-place predicate, are as follows:The variables here are explanatory only and no part of the final notation. Ultimately the predicate letters need exponents showing the number of places, but I omit them in these pages.A further functor-to continue now with the 1971 version-was padding:Finally there was a zero-place predicate functor, which is to say simply a constant predicate, namely the predicate ‘I’ of identity, and there was a two-place predicate functor ‘∩’ of intersection. The intersection ‘F ∩ G’ received a generalized interpretation, allowing ‘F’ and ‘G’ to be predicates with unlike numbers of places. However, Steven T. Kuhn has lately shown me that the generalization is unnecessary and reducible to the homogeneous case.

Syllogism and quantification

1962 ◽  
Vol 27 (1) ◽  
pp. 58-72 ◽  
Author(s):  
Timothy Smiley
Keyword(s):  
Predicate Logic ◽  
Modern Logic ◽  
First Order ◽  
First Order Predicate Logic

Anyone who reads Aristotle, knowing something about modern logic and nothing about its history, must ask himself why the syllogistic cannot be translated as it stands into the logic of quantification. It is now more than twenty years since the invention of the requisite framework, the logic of many-sorted quantification.In the familiar first-order predicate logic generality is expressed by means of variables and quantifiers, and each interpretation of the system is based upon the choice of some class over which the variables may range, the only restriction placed on this ‘domain of individuals’ being that it should not be empty.

Some logical and syntactical observations concerning the first-order dependent type system λP

1999 ◽  
Vol 9 (4) ◽  
pp. 335-359 ◽  
Author(s):  
HERMAN GEUVERS ◽  
ERIK BARENDSEN
Keyword(s):  
Predicate Logic ◽  
Type System ◽  
Logical Framework ◽  
First Order ◽  
Logical Derivation ◽  
Dependent Type ◽  
First Order Predicate Logic

We look at two different ways of interpreting logic in the dependent type system λP. The first is by a direct formulas-as-types interpretation à la Howard where the logical derivation rules are mapped to derivation rules in the type system. The second is by viewing λP as a Logical Framework, following Harper et al. (1987) and Harper et al. (1993). The type system is then used as the meta-language in which various logics can be coded.We give a (brief) overview of known (syntactical) results about λP. Then we discuss two issues in some more detail. The first is the completeness of the formulas-as-types embedding of minimal first-order predicate logic into λP. This is a remarkably complicated issue, a first proof of which appeared in Geuvers (1993), following ideas in Barendsen and Geuvers (1989) and Swaen (1989). The second issue is the minimality of λP as a logical framework. We will show that some of the rules are actually superfluous (even though they contribute nicely to the generality of the presentation of λP).At the same time we will attempt to provide a gentle introduction to λP and its various aspects and we will try to use little inside knowledge.

First order predicate logic

1986 ◽  
pp. 155-183
Author(s):  
Igor Aleksander ◽  
Henri Farreny ◽  
Malik Ghallab
Keyword(s):  
Predicate Logic ◽  
First Order ◽  
First Order Predicate Logic

A Test of a Two-Stage Model of the Evaluation of Hypotheses from Quantified First-Order Predicate Logic in Information Use Tasks

1992 ◽  
Vol 71 (3_suppl) ◽  
pp. 1091-1104 ◽  
Author(s):  
Peter E. Langford ◽  
Robert Hunting
Keyword(s):  
Predicate Logic ◽  
Information Use ◽  
Stage Model ◽  
Two Stage ◽  
First Order ◽  
Alternative Hypotheses ◽  
Age Range ◽  
Hypothesis Evaluation ◽  
Universe Of Discourse ◽  
First Order Predicate Logic

480 adolescents and young adults between the ages of 12 and 29 years participated in an experiment in which they were asked to evaluate hypotheses from quantified first-order predicate logic specifying that certain classes of event were necessarily, possibly, or certainly not included within a universe of discourse. Results were used to test a two-stage model of performance on hypothesis evaluation tasks that originated in work on the evaluation of conditionals. The two-stage model, unlike others available, successfully predicted the range of patterns of reply observed. In dealing with very simple hypotheses subjects in this age range tended not to make use of alternative hypotheses unless these were explicitly or implicitly suggested to them by the task. This tells against complexity of hypothesis as an explanation of the reluctance to use alternative hypotheses in evaluating standard conditionals.

Sign in / Sign up

Export Citation Format

Share Document