A Free Variable Version of the First-Order Predicate Calculus

1991 ◽  
Vol 1 (4) ◽  
pp. 431-451 ◽  
Author(s):  
MARTIN DAVIS ◽  
RONALD FECHTER
Keyword(s):  
Free Variable ◽  
Predicate Calculus ◽  
First Order ◽  
Order Predicate Calculus

Solution of a problem of Leon Henkin

1955 ◽  
Vol 20 (2) ◽  
pp. 115-118 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Number Theory ◽  
Recursive Function ◽  
Formal System ◽  
Free Variable ◽  
Formal Proof ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Order Predicate Calculus

If Σ is any standard formal system adequate for recursive number theory, a formula (having a certain integer q as its Gödel number) can be constructed which expresses the proposition that the formula with Gödel number q is provable in Σ. Is this formula provable or independent in Σ? [2].One approach to this problem is discussed by Kreisel in [4]. However, he still leaves open the question whether the formula (Ex)(x, a), with Gödel-number a, is provable or not. Here (x, y) is the number-theoretic predicate which expresses the proposition that x is the number of a formal proof of the formula with Gödel-number y.In this note we present a solution of the previous problem with respect to the system Zμ [3] pp. 289–294, and, more generally, with respect to any system whose set of theorems is closed under the rules of inference of the first order predicate calculus, and satisfies the subsequent five conditions, and in which the function (k, l) used below is definable.The notation and terminology is in the main that of [3] pp. 306–326, viz. if is a formula of Zμ containing no free variables, whose Gödel number is a, then ({}) stands for (Ex)(x, a) (read: the formula with Gödel number a is provable in Zμ); if is a formula of Zμ containing a free variable, y say, ({}) stands for (Ex)(x, g(y)}, where g(y) is a recursive function such that for an arbitrary numeral the value of g() is the Gödel number of the formula obtained from by substituting for y in throughout. We shall, however, depart trivially from [3] in writing (), where is an arbitrary numeral, for (Ex){x, ).

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

scholarly journals On a Propositional Calculus Whose Decision Problem is Recursively Unsolvable

1970 ◽  
Vol 38 ◽  
pp. 145-152
Author(s):  
Akira Nakamura
Keyword(s):  
Decision Problem ◽  
Propositional Calculus ◽  
Predicate Calculus ◽  
Reduction Theorem ◽  
List Type ◽  
First Order ◽  
Order Predicate Calculus

The purpose of this paper is to present a propositional calculus whose decision problem is recursively unsolvable. The paper is based on the following ideas: (1) Using Löwenheim-Skolem’s Theorem and Surányi’s Reduction Theorem, we will construct an infinitely many-valued propositional calculus corresponding to the first-order predicate calculus.(2) It is well known that the decision problem of the first-order predicate calculus is recursively unsolvable.(3) Thus it will be shown that the decision problem of the infinitely many-valued propositional calculus is recursively unsolvable.

Infinitary logic and admissible sets

1969 ◽  
Vol 34 (2) ◽  
pp. 226-252 ◽  
Author(s):  
Jon Barwise
Keyword(s):  
Second Order ◽  
Order Logic ◽  
Predicate Calculus ◽  
Generalized Quantifiers ◽  
Infinitary Logic ◽  
First Order ◽  
Admissible Sets ◽  
Classical Language ◽  
Second Order Logic ◽  
Order Predicate Calculus

In recent years much effort has gone into the study of languages which strengthen the classical first-order predicate calculus in various ways. This effort has been motivated by the desire to find a language which is(I) strong enough to express interesting properties not expressible by the classical language, but(II) still simple enough to yield interesting general results. Languages investigated include second-order logic, weak second-order logic, ω-logic, languages with generalized quantifiers, and infinitary logic.

A complete infinitary logic

1976 ◽  
Vol 41 (4) ◽  
pp. 730-746
Author(s):  
Kenneth Slonneger
Keyword(s):  
Natural Extension ◽  
Predicate Calculus ◽  
Cut Elimination ◽  
Infinitary Logic ◽  
Logical System ◽  
Natural Numbers ◽  
First Order ◽  
Ordinal Numbers ◽  
Power Set ◽  
Order Predicate Calculus

This paper is concerned with the proof theoretic development of certain infinite languages. These languages contain the usual infinite conjunctions and disjunctions, but in addition to homogeneous quantifiers such as ∀x0x1x2 … and ∃y0y1y2 …, we shall investigate particular subclasses of the dependent quantifiers described by Henkin [1]. The dependent quantifiers of Henkin can be thought of as partially ordered quantifiers defined by a function from one set to the power set of another set. This function assigns to each existentially bound variable, the set of universally bound variables on which it depends.The natural extension of Gentzen's first order predicate calculus to an infinite language with homogeneous quantifiers results in a system that is both valid and complete, and in which a cut elimination theorem can be proved [2]. The problem then arises of devising, if possible, a logical system dealing with general dependent quantifiers that is valid and complete. In this paper a system is presented that is valid and complete for an infinite language with homogeneous quantifiers and dependent quantifiers that are anti-well-ordered, for example, … ∀x2∃y2∀x1∃y1∀x0∃y0.Certain notational conventions will be employed in this paper. Greek letters will be used for ordinal numbers. The ordinal ω is the set of all natural numbers, and 2ω is the set of all ω -sequences of elements of 2 = {0,1}. The power set of S is denoted by P(S). μα[A(α)] stands for the smallest ordinal α such that A (α) holds.

On the formalisation of indirect discourse

1958 ◽  
Vol 23 (4) ◽  
pp. 417-419 ◽  
Author(s):  
R. L. Goodstein
Keyword(s):  
Predicate Logic ◽  
Logical Truth ◽  
Predicate Calculus ◽  
Inference Rules ◽  
First Order ◽  
Indirect Discourse ◽  
Image Position ◽  
Order Predicate Calculus

Mr. L. J. Cohen's interesting example of a logical truth of indirect discourse appears to be capable of a simple formalisation and proof in a variant of first order predicate calculus. His example has the form:If A says that anything which B says is false, and B says that something which A says is true, then something which A says is false and something which B says is true.Let ‘A says x’ be formalised by ‘A(x)’ and let assertions of truth and falsehood be formalised as in the following table.We treat both variables x and predicates A (x) as sentences and add to the familiar axioms and inference rules of predicate logic a rule permitting the inference of A(p) from (x)A(x), where p is a closed sentence.We have to prove that from

A formalization of the theory of ordinal numbers

1965 ◽  
Vol 30 (3) ◽  
pp. 295-317 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Set Theory ◽  
Natural Extension ◽  
Mathematical Induction ◽  
Predicate Calculus ◽  
Transfinite Induction ◽  
First Order ◽  
Recursive Functions ◽  
Ordinal Numbers ◽  
Primitive Recursive ◽  
Order Predicate Calculus

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

Sign in / Sign up

Export Citation Format

Share Document