scholarly journals A decision procedure for a class of formulas of first order predicate calculus

1964 ◽  
Vol 14 (4) ◽  
pp. 1305-1319 ◽  
Author(s):  
Melven Krom
Keyword(s):  
Decision Procedure ◽  
Predicate Calculus ◽  
First Order ◽  
Order Predicate Calculus

On simplifying the matrix of a wff

1968 ◽  
Vol 33 (2) ◽  
pp. 180-192 ◽  
Author(s):  
Peter Andrews
Keyword(s):  
Normal Form ◽  
Decision Procedure ◽  
Conjunctive Normal Form ◽  
Predicate Calculus ◽  
First Order ◽  
The Matrix ◽  
Order Predicate Calculus

In [3], [4], and [5] Joyce Friedman formulated and investigated certain rules which constitute a semi-decision procedure for wffs of first order predicate calculus in closed prenex normal form with prefixes of the form ∀x1 … ∀xκ∃y1 … ∃ym∀z1 … ∀zn. Given such a wff QM, where Q is the prefix and M is the matrix in conjunctive normal form, Friedman's rules can be used, in effect, to construct a matrix M* which is obtained from M by deleting certain conjuncts of M.

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.

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 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

Sign in / Sign up

Export Citation Format

Share Document