scholarly journals Definability in the monadic second-order theory of successor

1969 ◽  
Vol 34 (2) ◽  
pp. 166-170 ◽  
Author(s):  
J. Richard Buchi ◽  
Lawrence H. Landweber
Keyword(s):  
Order Theory ◽  
Second Order ◽  
Predicate Calculus ◽  
Relational System ◽  
First Order ◽  
Individual Variables ◽  
Order Predicate Calculus

Let be a relational system whereby D is a nonempty set and P1 is an m1-ary relation on D. With we associate the (weak) monadic second-order theory consisting of the first-order predicate calculus with individual variables ranging over D; monadic predicate variables ranging over (finite) subsets of D; monadic predicate quantifiers; and constants corresponding to P1, P2, …. We will often use ambiguously to mean also the set of true sentences of .

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.

Embedding first order predicate logic in fragments of intuitionistic logic

1976 ◽  
Vol 41 (4) ◽  
pp. 705-718 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Logic ◽  
Propositional Calculus ◽  
Expressive Power ◽  
Predicate Calculus ◽  
First Order ◽  
Intuitionistic Propositional Calculus ◽  
Individual Variables ◽  
The One ◽  
Order Predicate Calculus

Some syntactically simple fragments of intuitionistic logic possess considerable expressive power compared with their classical counterparts.In particular, we consider in this paper intuitionistic second order propositional logic (ISPL) a formalisation of which may be obtained by adding to the intuitionistic propositional calculus quantifiers binding propositional variables together with the usual quantifier rules and the axiom scheme (Ex), where is a formula not containing x.The main purpose of this paper is to show that the classical first order predicate calculus with identity can be (isomorphically) embedded in ISPL.It turns out an immediate consequence of this that the classical first order predicate calculus with identity can also be embedded in the fragment (PLA) of the intuitionistic first order predicate calculus whose only logical symbols are → and (.) (universal quantifier) and the only nonlogical symbol (apart from individual variables and parentheses) a single monadic predicate letter.Another consequence is that the classical first order predicate calculus can be embedded in the theory of Heyting algebras.The undecidability of the formal systems under consideration evidently follows immediately from the present results.We shall indicate how the methods employed may be extended to show also that the intuitionistic first order predicate calculus with identity can be embedded in both ISPL and PLA.For the purpose of the present paper it will be convenient to use the following formalisation (S) of ISPL based on [3], rather than the one given above.

Two interpolation theorems for a predicate calculus

1971 ◽  
Vol 36 (2) ◽  
pp. 262-270
Author(s):  
Shoji Maehara ◽  
Gaisi Takeuti
Keyword(s):  
Normal Form ◽  
Completeness Theorem ◽  
Interpolation Theorem ◽  
Second Order ◽  
Predicate Calculus ◽  
Cut Elimination ◽  
First Order ◽  
Image Position ◽  
Order Predicate Calculus

A second order formula is called Π1 if, in its prenex normal form, all second order quantifiers are universal. A sequent F1, … Fm → G1 …, Gn is called Π1 if a formulais Π1If we consider only Π1 sequents, then we can easily generalize the completeness theorem for the cut-free first order predicate calculus to a cut-free Π1 predicate calculus.In this paper, we shall prove two interpolation theorems on the Π1 sequent, and show that Chang's theorem in [2] is a corollary of our theorem. This further supports our belief that any form of the interpolation theorem is a corollary of a cut-elimination theorem. We shall also show how to generalize our results for an infinitary language. Our method is proof-theoretic and an extension of a method introduced in Maehara [5]. The latter has been used frequently to prove the several forms of the interpolation theorem.

Some forms of completeness

1962 ◽  
Vol 27 (3) ◽  
pp. 344-352 ◽  
Author(s):  
P. C. Gilmore
Keyword(s):  
Predicate Symbol ◽  
Constant Term ◽  
Predicate Calculus ◽  
First Order ◽  
Individual Variables ◽  
The Individual ◽  
And Function ◽  
Order Predicate Calculus

By a theory is meant an applied first-order predicate calculus with at least one predicate symbol and perhaps some individual constants and function symbols and a specified set of axioms. In addition to the terms defined by means of the individual variables, constants, and function symbols a theory may also include among its terms those constructed by means of operators such as the epsilon or iota operators; that is, expressions like (εχΡ) or (οχΡ), where P is a well formed formula (wff) of the theory, may also be terms. A constant term of a theory F is then a term in which no variable occurs free. We are interested only in theories which have at least one constant term so that if a theory doesn't have any individual constants it must necessarily admit as terms expressions constructed by means of operators. A sentence of a theory F is a closed wff.

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.

A feasible theory for analysis

1994 ◽  
Vol 59 (3) ◽  
pp. 1001-1011 ◽  
Author(s):  
Fernando Ferreira
Keyword(s):  
Polynomial Time ◽  
Order Theory ◽  
Second Order ◽  
First Order ◽  
Weak König’S Lemma ◽  
König’S Lemma ◽  
Computable Functions

AbstractWe construct a weak second-order theory of arithmetic which includes Weak König's Lemma (WKL) for trees defined by bounded formulae. The provably total functions (with -graphs) of this theory are the polynomial time computable functions. It is shown that the first-order strength of this version of WKL is exactly that of the scheme of collection for bounded formulae.

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, ).

Sign in / Sign up

Export Citation Format

Share Document