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 Θ′.

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.

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

Applications of trees to intermediate logics

1972 ◽  
Vol 37 (1) ◽  
pp. 135-138 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Kripke Model ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Geometric Properties ◽  
Intermediate Logics ◽  
Truth Value ◽  
Constant Domains ◽  
Completeness Theorems

We investigate extensions of Heyting's predicate calculus (HPC). We relate geometric properties of the trees of Kripke models (see [2]) with schemas of HPC and thus obtain completeness theorems for several intermediate logics defined by schemas. Our main results are:(a) ∼(∀x ∼ ∼ϕ(x) Λ ∼∀xϕ(x)) is characterized by all Kripke models with trees T with the property that every point is below an endpoint. (From this we shall deduce Glivenko type theorems for this extension.)(b) The fragment of HPC without ∨ and ∃ is complete for all Kripke models with constant domains.We assume familiarity with Kripke [2]. Our notation is different from his since we want to stress properties of the trees. A Kripke model will be denoted by (Aα, ≤ 0), α ∈ T where (T, ≤, 0) is the tree with the least member 0 ∈ T and Aα, α ∈ T, is the model standing at the node α. The truth value at α of a formula ϕ(a1 … an) under the indicated assignment at α is denoted by [ϕ(a1 … an)]α.A Kripke model is said to be of constant domains if all the models Aα, α ∈ T, have the same domain.

Another intuitionistic completeness proof

1976 ◽  
Vol 41 (3) ◽  
pp. 644-662 ◽  
Author(s):  
H. De Swart
Keyword(s):  
Slight Modification ◽  
Kripke Model ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Single Model ◽  
Completeness Proof ◽  
Definition Of

In March 1973, W. Veldman [1] discovered that, by a slight modification of a Kripke-model, it was possible to give an intuitionistic proof of the completeness-theorem for the intuitionistic predicate calculus (IPC) with respect to modified Kripke models. The modification was the following: Let f represent absurdity, then we allow the possibility that and we agree that, for all sentences ϕ, , if . Just one modified Kripke model is constructed such that validity in implies derivability in IPC. While usually one thinks of as some subset of ⋃nNatn and of as the discrete natural ordering in ⋃nNatn, in Veldman's model , is a spread and , where Γα and Γβ are sets of sentences associated with α, resp. β, is a nondiscrete ordering.In the completeness-proofs, both for Beth and for Kripke models that we present here, we consider only models over ⋃nNatn, with the natural discrete ordering and we need validity in all models, not just in one, to get derivability in IPC. Also we have to modify the definition of a model in a somewhat different way than Veldman did. We agree that if ∨s[M⊨sf], then M⊨sϕ for each s ∈ ⋃nNatn and for each sentence ϕ.One can view a single model of the type constructed in [1] as the result of throwing together all the models of (the type constructed in) this paper into one big model, which has the somewhat strange properties mentioned above.

scholarly journals Algebraic Solution to Constrained Bi-Criteria Decision Problem of Rating Alternatives through Pairwise Comparisons

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 303
Author(s):  
Nikolai Krivulin
Keyword(s):  
Decision Problem ◽  
Optimization Problem ◽  
Pareto Frontier ◽  
Sufficient Conditions ◽  
Approximation Error ◽  
Optimal Solution ◽  
Algebraic Solution ◽  
Pairwise Comparisons ◽  
Logarithmic Scale ◽  
Idempotent Algebra

We consider a decision-making problem to evaluate absolute ratings of alternatives from the results of their pairwise comparisons according to two criteria, subject to constraints on the ratings. We formulate the problem as a bi-objective optimization problem of constrained matrix approximation in the Chebyshev sense in logarithmic scale. The problem is to approximate the pairwise comparison matrices for each criterion simultaneously by a common consistent matrix of unit rank, which determines the vector of ratings. We represent and solve the optimization problem in the framework of tropical (idempotent) algebra, which deals with the theory and applications of idempotent semirings and semifields. The solution involves the introduction of two parameters that represent the minimum values of approximation error for each matrix and thereby describe the Pareto frontier for the bi-objective problem. The optimization problem then reduces to a parametrized vector inequality. The necessary and sufficient conditions for solutions of the inequality serve to derive the Pareto frontier for the problem. All solutions of the inequality, which correspond to the Pareto frontier, are taken as a complete Pareto-optimal solution to the problem. We apply these results to the decision problem of interest and present illustrative examples.

scholarly journals Jordan products of quantum channels and their compatibility

2021 ◽  
Vol 12 (1) ◽  
Author(s):  
Mark Girard ◽  
Martin Plávala ◽  
Jamie Sikora
Keyword(s):  
Quantum State ◽  
Sufficient Conditions ◽  
The Other ◽  
Independent Interest ◽  
Quantum Channels ◽  
Semidefinite Programs ◽  
Jordan Product ◽  
Marginal Problem ◽  
Jordan Products ◽  
Product Of Matrices

AbstractGiven two quantum channels, we examine the task of determining whether they are compatible—meaning that one can perform both channels simultaneously but, in the future, choose exactly one channel whose output is desired (while forfeiting the output of the other channel). Here, we present several results concerning this task. First, we show it is equivalent to the quantum state marginal problem, i.e., every quantum state marginal problem can be recast as the compatibility of two channels, and vice versa. Second, we show that compatible measure-and-prepare channels (i.e., entanglement-breaking channels) do not necessarily have a measure-and-prepare compatibilizing channel. Third, we extend the notion of the Jordan product of matrices to quantum channels and present sufficient conditions for channel compatibility. These Jordan products and their generalizations might be of independent interest. Last, we formulate the different notions of compatibility as semidefinite programs and numerically test when families of partially dephasing-depolarizing channels are compatible.

scholarly journals On a New Geometric Constant Related to the Euler-Lagrange Type Identity in Banach Spaces

Mathematics ◽  
2021 ◽  
Vol 9 (2) ◽  
pp. 116
Author(s):  
Qi Liu ◽  
Yongjin Li
Keyword(s):  
Banach Spaces ◽  
Product Space ◽  
Sufficient Conditions ◽  
Normal Structure ◽  
The Other ◽  
Inner Product ◽  
Equivalent Characterization ◽  
Geometric Constant ◽  
Geometric Constants

In this paper, we will introduce a new geometric constant LYJ(λ,μ,X) based on an equivalent characterization of inner product space, which was proposed by Moslehian and Rassias. We first discuss some equivalent forms of the proposed constant. Next, a characterization of uniformly non-square is given. Moreover, some sufficient conditions which imply weak normal structure are presented. Finally, we obtain some relationship between the other well-known geometric constants and LYJ(λ,μ,X). Also, this new coefficient is computed for X being concrete space.

APC: The Algorithmic Predicate Calculus

1981 ◽  
Vol 4 (2) ◽  
pp. 343-367
Author(s):  
Wojciech Przyłuski
Keyword(s):  
Time Scale ◽  
Predicate Calculus ◽  
Algorithmic Logic ◽  
Classical Predicate

The paper presents a logic which is an algorithmic extension of the classical predicate calculus and is based on the ideas given by F. Kröger. The programs and the effects of their execution are the formulas of this logic which are considered at any time scale. There are many interesting properties of the logic which are connected with the notion of time scale. These properties are examined in the paper. Moreover the problem of the formulas normalization is presented. Our logic is compared with the algorithmic logic introduced by A. Salwicki. Next, the usefulness of a new logic in the theory of programs is shown.

Sign in / Sign up

Export Citation Format

Share Document