Some remarks concerning theories with recursively enumerable complements

1963 ◽  
Vol 28 (1) ◽  
pp. 72-74 ◽  
Author(s):  
Alan Cobham
Keyword(s):  
Predicate Calculus ◽  
Effective Procedure ◽  
First Order ◽  
Recursively Enumerable ◽  
Decidable Theories ◽  
Mechanical Procedure ◽  
Order Predicate Calculus

A system formalized within the first order predicate calculus either with or without the identity but without predicate or function variables we call simply a theory. We say that a theory T has a recursively enumerable complement (r.e. Comp.) if the set of all sentences of T not valid in T is recursively enumerable. This is equivalent to saying that there exists an effective, purely mechanical procedure for establishing the non-validity in T of precisely those sentences of T which are in fact not theorems of T. If in addition T is recursively enumerable, that is, if there is an effective procedure for establishing the validity in T of its theorems, then T is decidable. It will be shown here that several well-known results concerning decidable theories can be extended to cover theories with r.e. comps. In this respect it should be observed that there exist theories having r.e. comps. which are not decidable. An example is the theory which has as valid sentences just those which contain a given two-place predicate and which are valid in all non-void finite universes [3], [4].

Recursion theory and formal deducibility

1970 ◽  
Vol 35 (4) ◽  
pp. 556-558
Author(s):  
E. M. Kleinberg
Keyword(s):  
Recursion Theory ◽  
Order Logic ◽  
Negative Integer ◽  
Predicate Calculus ◽  
First Order Logic ◽  
Recursively Enumerable Set ◽  
First Order ◽  
Recursively Enumerable ◽  
Order Predicate Calculus

The enumeration, given a first-order sentence , of all sentences deducible from in the first-order predicate calculus, and the enumeration, given a non-negative integer n, of the recursively enumerable set Wn, are two well-known examples of effective processes. But are these processes really distinct? Indeed, might there not exist a Gödel numbering of the sentences of first-order logic such that for each n, if n is the number assigned to the sentence , then Wn is the set of numbers assigned to all sentences deducible from ? If this were the case, the first sort of enumeration would just be a particular instance of the second.

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