Decidability of some intuitionistic predicate theories

1972 ◽  
Vol 37 (3) ◽  
pp. 579-587 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Reduction Method ◽  
Abelian Groups ◽  
Sufficient Conditions ◽  
Kripke Model ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Classical Counterpart ◽  
First Order ◽  
Intuitionistic Theory ◽  
Classical Predicate

Suppose T is a first order intuitionistic theory (more precisely, a theory of Heyting's predicate calculus, e.g., abelian groups, one unary function, dense linear order, etc.) presented to us by a set of axioms (denoted also by) T.Question. Is T decidable?One knows that if the classical counterpart of T (i.e., take the same axioms but with the classical predicate calculus as the underlying logic) is not decidable, then T cannot be decidable. The problem remains for theories whose classical counterpart is decidable. In [8], sufficient conditions for undecidability were given, and several intuitionistic theories such as abelian groups and unary functions (both with decidable equality) were shown to be undecidable. In this note we show decidability results (see Theorems 1 and 2 below), and compare these results with the undecidability results previously obtained. The method we use is the reduction-method, described fully in [12] and widely applied in [3], which is applied here roughly as follows:Let T be a given theory of Heyting's predicate calculus. We know that Heyting's predicate calculus is complete for the Kripke-model type of semantics. We choose a class M of Kripke models for which T is complete, i.e., all axioms of T are valid in any model of the class and whenever φ is not a theorem of T, φ is false in some model of M.

Sufficient conditions for the undecidability of intuitionistic theories with applications

1972 ◽  
Vol 37 (2) ◽  
pp. 375-384 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Decision Problem ◽  
Sufficient Conditions ◽  
Kripke Model ◽  
The Other ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Symmetric Relation ◽  
Undecidable Theory ◽  
Classical Models ◽  
Classical Predicate

Let Δ be a set of axioms of a theory Tc(Δ) of classical predicate calculus (CPC); Δ may also be considered as a set of axioms of a theory TH(Δ) of Heyting's predicate calculus (HPC). Our aim is to investigate the decision problem of TH(Δ) in HPC for various known theories Δ of CPC.Theorem I(a) of §1 states that if Δ is a finitely axiomatizable and undecidable theory of CPC then TH(Δ) is undecidable in HPC. Furthermore, the relations between theorems of HPC are more complicated and so two CPC-equivalent axiomatizations of the same theory may give rise to two different HPC theories, in fact, one decidable and the other not.Semantically, the Kripke models (for which HPC is complete) are partially ordered families of classical models. Thus a formula expresses a property of a family of classical models (i.e. of a Kripke model). A theory Θ expresses a set of such properties. It may happen that a class of Kripke models defined by a set of formulas Θ is also definable in CPC (in a possibly richer language) by a CPC-theory Θ′! This establishes a connection between the decision problem of Θ in HPC and that of Θ′ in CPC. In particular if Θ′ is undecidable, so is Θ. Theorems II and III of §1 give sufficient conditions on Θ to be such that the corresponding Θ′ is undecidable. Θ′ is shown undecidable by interpreting the CPC theory of a reflexive and symmetric relation in Θ′.

Resolution systems and their applications I

1980 ◽  
Vol 3 (2) ◽  
pp. 235-268
Author(s):  
Ewa Orłowska
Keyword(s):  
Theorem Proving ◽  
Sufficient Conditions ◽  
Predicate Calculus ◽  
Resolution Method ◽  
First Order ◽  
Deductive Systems ◽  
Resolution System ◽  
Resolution Principle ◽  
Necessary And Sufficient ◽  
Classical Predicate

The central method employed today for theorem-proving is the resolution method introduced by J. A. Robinson in 1965 for the classical predicate calculus. Since then many improvements of the resolution method have been made. On the other hand, treatment of automated theorem-proving techniques for non-classical logics has been started, in connection with applications of these logics in computer science. In this paper a generalization of a notion of the resolution principle is introduced and discussed. A certain class of first order logics is considered and deductive systems of these logics with a resolution principle as an inference rule are investigated. The necessary and sufficient conditions for the so-called resolution completeness of such systems are given. A generalized Herbrand property for a logic is defined and its connections with the resolution-completeness are presented. A class of binary resolution systems is investigated and a kind of a normal form for derivations in such systems is given. On the ground of the methods developed the resolution system for the classical predicate calculus is described and the resolution systems for some non-classical logics are outlined. A method of program synthesis based on the resolution system for the classical predicate calculus is presented. A notion of a resolution-interpretability of a logic L in another logic L ′ is introduced. The method of resolution-interpretability consists in establishing a relation between formulas of the logic L and some sets of formulas of the logic L ′ with the intention of using the resolution system for L ′ to prove theorems of L. It is shown how the method of resolution-interpretability can be used to prove decidability of sets of unsatisfiable formulas of a given logic.

scholarly journals Elementary-base cirquent calculus II: Choice quantifiers

2020 ◽  
Author(s):  
Giorgi Japaridze
Keyword(s):  
Proof Theory ◽  
Predicate Calculus ◽  
First Order ◽  
Complete Axiomatization ◽  
Calculus I ◽  
Soundness And Completeness ◽  
Classical Predicate

Abstract Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article ‘Elementary-base cirquent calculus I: Parallel and choice connectives’ built the sound and complete axiomatization $\textbf{CL16}$ of a propositional fragment of computability logic. The atoms of the language of $\textbf{CL16}$ represent elementary, i.e. moveless, games and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version $\textbf{CL17}$ of $\textbf{CL16}$, also enjoying soundness and completeness. The language of $\textbf{CL17}$ augments that of $\textbf{CL16}$ by including choice quantifiers. Unlike classical predicate calculus, $\textbf{CL17}$ turns out to be decidable.

The undecidability of intuitionistic theories of algebraically closed fields and real closed fields

1973 ◽  
Vol 38 (1) ◽  
pp. 86-92 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Classical Theory ◽  
Linear Order ◽  
Abelian Groups ◽  
Classical Model ◽  
Sufficient Conditions ◽  
Interesting Case ◽  
Real Closed Fields ◽  
Closed Fields ◽  
Intuitionistic Theory ◽  
Algebraically Closed Fields

Let T be a set of axioms for a classical theory TC (e.g. abelian groups, linear order, unary function, algebraically closed fields, etc.). Suppose we regard T as a set of axioms for an intuitionistic theory TH (more precisely, we regard T as axioms in Heyting's predicate calculus HPC).Question. Is TH decidable (or, more generally, if X is any intermediate logic, is TX decidable)? In [1] we gave sufficient conditions for the undecidability of TH. These conditions depend on the formulas of T (different axiomatization of the same TC may give rise to different TH) and on the classical model theoretic properties of TC (the method did not work for model complete theories, e.g. those of the title of the paper). For details see [1]. In [2] we gave some decidability results for some theories: The problem of the decidability of theories TH for a classically model complete TC remained open. An undecidability result in this direction, for dense linear order was obtained by Smorynski [4]. The cases of algebraically closed fields and real closed fields and divisible abelian groups are treated in this paper. Other various decidability results of the intuitionistic theories were obtained by several authors, see [1], [2], [4] for details.One more remark before we start. There are several possible formulations for an intuitionistic theory of, e.g. fields, that correspond to several possible axiomatizations of the classical theory. Other formulations may be given in terms of the apartness relation, such as the one for fields given by Heyting [5]. The formulations that we consider here are of interest as these systems occur in intuitionistic mathematics. We hope that the present methods could be extended to the (more interesting) case of Heyting's systems [5].

Undecidability of modal and intermediate first-order logics with two individual variables

1993 ◽  
Vol 58 (3) ◽  
pp. 800-823 ◽  
Author(s):  
D. M. Gabbay ◽  
V. B. Shehtman
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Calculus ◽  
Single Individual ◽  
First Order ◽  
Short Summary ◽  
Binary Predicate ◽  
Individual Variables ◽  
Image Position ◽  
Classical Predicate

The interest in fragments of predicate logics is motivated by the well-known fact that full classical predicate calculus is undecidable (cf. Church [1936]). So it is desirable to find decidable fragments which are in some sense “maximal”, i.e., which become undecidable if they are “slightly” extended. Or, alternatively, we can look for “minimal” undecidable fragments and try to identify the vague boundary between decidability and undecidability. A great deal of work in this area concerning mainly classical logic has been done since the thirties. We will not give a complete review of decidability and undecidability results in classical logic, referring the reader to existing monographs (cf. Suranyi [1959], Lewis [1979], and Dreben, Goldfarb [1979]). A short summary can also be found in the well-known book Church [1956]. Let us recall only several facts. Herein we will consider only logics without functional symbols, constants, and equality.(C1) The fragment of the classical logic with only monadic predicate letters is decidable (cf. Behmann [1922]).(C2) The fragment of the classical logic with a single binary predicate letter is undecidable. (This is a consequence of Gödel [1933].)(C3) The fragment of the classical logic with a single individual variable is decidable; in fact it is equivalent to Lewis S5 (cf. Wajsberg [1933]).(C4) The fragment of the classical logic with two individual variables is decidable (Segerberg [1973] contains a proof using modal logic; Scott [1962] and Mortimer [1975] give traditional proofs.)(C5) The fragment of the classical logic with three individual variables and binary predicate letters is undecidable (cf. Surańyi [1943]). In fact this paper considers formulas of the following typeφ,ψ being quantifier-free and the set of binary predicate letters which can appear in φ or ψ being fixed and finite.

scholarly journals An elimination theorem of uniqueness conditions in the intuitionistic predicate calculus

1982 ◽  
Vol 85 ◽  
pp. 223-230 ◽  
Author(s):  
Nobuyoshi Motohashi
Keyword(s):  
Free Variable ◽  
The Other ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Classical Predicate

This paper is a sequel to Motohashi [4]. In [4], a series of theorems named “elimination theorems of uniqueness conditions” was shown to hold in the classical predicate calculus LK. But, these results have the following two defects : one is that they do not hold in the intuitionistic predicate calculus LJ, and the other is that they give no nice axiomatizations of some sets of sentences concerned. In order to explain these facts more explicitly, let us introduce some necessary notations and definitions. Let L be a first order classical predicate calculus LK or a first order intuitionistic predicate calculus LJ. n-ary formulas in L are formulas F(ā) in L with a sequence ā of distinct free variables of length n such that every free variable in F occurs in ā.

scholarly journals On the Definitional Embeddability of Some Elementary Algebraic Theories into the First-Order Predicate Calculus

2015 ◽  
Vol 21 (2) ◽  
pp. 15-20
Author(s):  
В. И. Шалак
Keyword(s):  
Group Theory ◽  
Abelian Groups ◽  
Predicate Logic ◽  
Predicate Calculus ◽  
General Algebra ◽  
First Order ◽  
Algebraic Theories ◽  
Logical Content ◽  
Order Predicate Calculus ◽  
First Order Predicate Logic

In this article we prove a theorem on the definitional embeddability into first-order predicate logic without equality of such well-known mathematical theories as group theory and the theory of Abelian groups. This result may seem surprising, since it is generally believed that these theories have a non-logical content. It turns out that the central theory of general algebra are purely logical. Could this be the reason that we find them in many branches of mathematics? This result will be of interest not only for logicians and mathematicians but also for philosophers who study foundations of logic and its relation to mathematics.

scholarly journals Some weak fragments of HA and certain closure properties

2002 ◽  
Vol 67 (1) ◽  
pp. 91-103 ◽  
Author(s):  
Morteza Moniri ◽  
Mojtaba Moniri
Keyword(s):  
Kripke Model ◽  
The Other ◽  
Kripke Models ◽  
Closure Properties ◽  
Double Negation ◽  
Other Hand ◽  
Intuitionistic Theory ◽  
Open Formula ◽  
Open Induction ◽  
Universal Quantification

AbstractWe show that Intuitionistic Open Induction iop is not closed under the rule DNS(Ǝ1). This is established by constructing a Kripke model of iop + ¬Ly(2y > x), where Ly(2y > x) is universally quantified on x. On the other hand, we prove that iop is equivalent with the intuitionistic theory axiomatized by PA− plus the scheme of weak ¬¬ LNP for open formulas, where universal quantification on the parameters precedes double negation. We also show that for any open formula φ(y) having only y free. (PA−)i ⊢ Lyφ(y). We observe that the theories iop, i∀1 and iΠ1 are closed under Friedman's translation by negated formulas and so under VR and IP. We include some remarks on the classical worlds in Kripke models of iop.

Forcing and satisfaction in Kripke models of intuitionistic arithmetic

2018 ◽  
Vol 27 (5) ◽  
pp. 659-670
Author(s):  
Maryam Abiri ◽  
Morteza Moniri ◽  
Mostafa Zaare
Keyword(s):  
Predicate Logic ◽  
Kripke Model ◽  
Peano Arithmetic ◽  
Kripke Models ◽  
Classical Structure ◽  
First Order ◽  
Heyting Arithmetic ◽  
Intuitionistic Arithmetic

Abstract We define a class of first-order formulas $\mathsf{P}^{\ast }$ which exactly contains formulas $\varphi$ such that satisfaction of $\varphi$ in any classical structure attached to a node of a Kripke model of intuitionistic predicate logic deciding atomic formulas implies its forcing in that node. We also define a class of $\mathsf{E}$-formulas with the property that their forcing coincides with their classical satisfiability in Kripke models which decide atomic formulas. We also prove that any formula with this property is an $\mathsf{E}$-formula. Kripke models of intuitionistic arithmetical theories usually have this property. As a consequence, we prove a new conservativity result for Peano arithmetic over Heyting arithmetic.

Equality and lyndon's interpolation theorem

1984 ◽  
Vol 49 (1) ◽  
pp. 123-128 ◽  
Author(s):  
Nobuyoshi Motohashi
Keyword(s):  
Interpolation Theorem ◽  
Predicate Calculus ◽  
Original Form ◽  
Original Formulation ◽  
First Order ◽  
Classical Predicate

In this paper, we remark on some properties of equality that tend to be neglected and use them to give a proof of an extension of Lyndon's interpolation theorem. Let LK be a first order classical predicate calculus and LK= a first order classical predicate calculus with equality. We assume that LK and LK= have the propositional constant Τ (truth). For each formula F in LK=, let Rel+ (F), Rel− (F), Rel(F), and Fun(F) be the set of all the predicate symbols which occur in F positively, the set of all the predicate symbols which occur in F negatively, the set of all the predicate symbols which occur in F, and the set of all the function symbols which occur in F.Theorem A (Lyndon [5]). Suppose that A and B are sentences in LK such that A ⊃ B is provable in LK. Then there is a sentence C in LK such that:(i) A ⊃ C and C ⊃ B are provable in LK;(ii) and(iii) .The sentence C which satisfies (i), (ii), (iii) in Theorem A is said to be an interpolant for A ⊃ B in Theorem A. Note that condition (iii) is not included in the original form of Lyndon's interpolation theorem (cf. [5]), but we can easily add this condition. Also, there is some obscurity in the original formulation with regard to the equality symbol. For example, Lyndon writes: “The theorem takes the same form whether or not we admit a predicate denoting identity, with suitable axioms, to the predicate calculus” [5, p. 129].

Sign in / Sign up

Export Citation Format

Share Document