The undecidability of the disjunction property of propositional logics and other related problems

1993 ◽  
Vol 58 (3) ◽  
pp. 967-1002 ◽  
Author(s):  
Alexander Chagrov ◽  
Michael Zakharyaschev
Keyword(s):  
Interpolation Property ◽  
Modus Ponens ◽  
Algorithmic Problem ◽  
Finite Model ◽  
Inference Rules ◽  
Property A ◽  
Disjunction Property ◽  
Intermediate Logics ◽  
First Results ◽  
Finite Set

‘How can we recognize, given axioms and inference rules of a calculus, whether the calculus has such-and-such property?’ A question of this kind arises whenever we deal with a new logic system. For large families of logics, this question may be considered as an algorithmic problem, and a property is called decidable in a given family if there exists an algorithm which is capable of deciding, for a finite axiomatics of a calculus in the family, whether or not it has the property.In the class of intermediate propositional logics, for instance, nontrivial properties such as the tabularity, pretabularity, and interpolation property (Maksimova [1972, 1977]) are decidable. However, for many other important properties—decidability, finite model property, disjunction property, Halldén-completeness, etc.—effective criteria were not found in spite of considerable efforts.In this paper we show that the difficulties in investigating these properties in the classes of intermediate logics and normal modal logics containing S4 are of principal nature, since all of them turn out to be algorithmically undecidable. In other words, there are no algorithms which, given a finite set of axioms of an intermediate or modal calculus, can recognize whether or not it is decidable, Halldén-complete, has the finite model or disjunction property.The first results concerning the undecidability of properties of calculi seem to have been obtained by Linial and Post [1949], who proved the undecidability of the problem of equivalence to classical calculus in the class of all propositional calculi with the same language as the classical one and the two inference rules: modus ponens and substitution. Kuznetsov [1963] generalized this result having proved the undecidability of the problem of equivalence to any fixed intermediate calculus (for instance, to intuitionistic calculus or even the inconsistent one). However, these results will not hold if we confine ourselves only to the class of intermediate logics, though the problem of equivalence to the undecidable intermediate calculus of Shehtman [1978] is clearly undecidable in this class as well.

A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property

1974 ◽  
Vol 39 (1) ◽  
pp. 67-78 ◽  
Author(s):  
D. M. Gabbay ◽  
D. H. J. De Jongh
Keyword(s):  
Intuitionistic Logic ◽  
Finite Model ◽  
Ordered Sets ◽  
Disjunction Property ◽  
University Of Illinois ◽  
Finite Model Property ◽  
Intermediate Logics ◽  
Heyting Arithmetic ◽  
Image Position ◽  
System 1

The intuitionistic propositional logic I has the following (disjunction) property.We are interested in extensions of the intuitionistic logic which are both decidable and have the disjunction property. Systems with the disjunction property are known, for example the Kreisel-Putnam system [1] which is I + (∼ϕ → (ψ ∨ α))→ ((∼ϕ→ψ) ∨ (∼ϕ→α)) and Scott's system I + ((∼ ∼ϕ→ϕ)→(ϕ ∨ ∼ϕ))→ (∼∼ϕ ∨ ∼ϕ). It was shown in [3c] that the first system has the finite-model property.In this note we shall construct a sequence of intermediate logics Dn with the following properties:These systems are presented both semantically and syntactically, using the remarkable correspondence between properties of partially ordered sets and axiom schemata of intuitionistic logic. This correspondence, apart from being interesting in itself (for giving geometric meaning to intuitionistic axioms), is also useful in giving independence proofs and obtaining proof theoretic results for intuitionistic systems (see for example, C. Smorynski, Thesis, University of Illinois, 1972, for independence and proof theoretic results in Heyting arithmetic).

The decidability of the Kreisel-Putnam system

1970 ◽  
Vol 35 (3) ◽  
pp. 431-437 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Finite Model ◽  
Model Property ◽  
Intuitionistic Propositional Logic ◽  
Disjunction Property ◽  
Finite Model Property ◽  
Image Position

The intuitionistic propositional logic I has the following disjunction property This property does not characterize intuitionistic logic. For example Kreisel and Putnam [5] showed that the extension of I with the axiomhas the disjunction property. Another known system with this propery is due to Scott [5], and is obtained by adding to I the following axiom:In the present paper we shall prove, using methods originally introduced by Segerberg [10], that the Kreisel-Putnam logic is decidable. In fact we shall show that it has the finite model property, and since it is finitely axiomatizable, it is decidable by [4]. The decidability of Scott's system was proved by J. G. Anderson in his thesis in 1966.

scholarly journals Gaussoids are two-antecedental approximations of Gaussian conditional independence structures

2021 ◽  
Author(s):  
Tobias Boege
Keyword(s):  
Characteristic Zero ◽  
Conditional Independence ◽  
Inference Rule ◽  
Positive Definite ◽  
Inference Rules ◽  
Identity Matrix ◽  
Ordered Fields ◽  
Finite Set

AbstractThe gaussoid axioms are conditional independence inference rules which characterize regular Gaussian CI structures over a three-element ground set. It is known that no finite set of inference rules completely describes regular Gaussian CI as the ground set grows. In this article we show that the gaussoid axioms logically imply every inference rule of at most two antecedents which is valid for regular Gaussians over any ground set. The proof is accomplished by exhibiting for each inclusion-minimal gaussoid extension of at most two CI statements a regular Gaussian realization. Moreover we prove that all those gaussoids have rational positive-definite realizations inside every ε-ball around the identity matrix. For the proof we introduce the concept of algebraic Gaussians over arbitrary fields and of positive Gaussians over ordered fields and obtain the same two-antecedental completeness of the gaussoid axioms for algebraic and positive Gaussians over all fields of characteristic zero as a byproduct.

scholarly journals Finitely Presented Heyting Algebras

1998 ◽  
Vol 5 (30) ◽  
Author(s):  
Carsten Butz
Keyword(s):  
Simple Proof ◽  
Heyting Algebra ◽  
Distributive Lattices ◽  
Heyting Algebras ◽  
Model Property ◽  
Disjunction Property ◽  
Irreducible Elements ◽  
Finite Set ◽  
Finite Distributive Lattices ◽  
Finitely Presented

In this paper we study the structure of finitely presented Heyting<br />algebras. Using algebraic techniques (as opposed to techniques from proof-theory) we show that every such Heyting algebra is in fact co- Heyting, improving on a result of Ghilardi who showed that Heyting algebras free on a finite set of generators are co-Heyting. Along the way we give a new and simple proof of the finite model property. Our main technical tool is a representation of finitely presented Heyting algebras in terms of a colimit of finite distributive lattices. As applications we construct explicitly the minimal join-irreducible elements (the atoms) and the maximal join-irreducible elements of a finitely presented Heyting algebra in terms of a given presentation. This gives as well a new proof of the disjunction property for intuitionistic propositional logic.<br />Unfortunately not very much is known about the structure of Heyting algebras, although it is understood that implication causes the complex structure of Heyting algebras. Just to name an example, the free Boolean algebra on one generator has four elements, the free Heyting algebra on one generator is infinite.<br />Our research was motivated a simple application of Pitts' uniform interpolation theorem [11]. Combining it with the old analysis of Heyting algebras free on a finite set of generators by Urquhart [13] we get a faithful functor J : HAop<br />f:p: ! PoSet; sending a finitely presented Heyting algebra to the partially ordered set of its join-irreducible elements, and a map between Heyting algebras to its leftadjoint<br />restricted to join-irreducible elements. We will explore on the induced duality more detailed in [5]. Let us briefly browse through the contents of this paper: The first section<br />recapitulates the basic notions, mainly that of the implicational degree of an element in a Heyting algebra. This is a notion relative to a given set of generators. In the next section we study nite Heyting algebras. Our contribution is a simple proof of the nite model property which names in particular a canonical family of nite Heyting algebras into which we can<br />embed a given finitely presented one.<br />In Section 3 we recapitulate the standard duality between nite distributive lattices and nite posets. The `new' feature here is a strict categorical<br />formulation which helps simplifying some proofs and avoiding calculations. In the following section we recapitulate the description given by Ghilardi [8]<br />on how to adjoin implications to a nite distributive lattice, thereby not destroying a given set of implications. This construction will be our major technical ingredient in Section 5 where we show that every nitely presented<br />Heyting algebra is co-Heyting, i.e., that the operation (−) n (−) dual to implication is dened. This result improves on Ghilardi's [8] that this is true<br />for Heyting algebras free on a finite set of generators. Then we go on analysing the structure of finitely presented Heyting algebras<br />in Section 6. We show that every element can be expressed as a finite join of join-irreducibles, and calculate explicitly the maximal join-irreducible elements in such a Heyting algebra (in terms of a given presentation). As a consequence we give a new proof of the disjunction property for propositional intuitionistic logic. As well, we calculate the minimal join-irreducible elements, which are nothing but the atoms of the Heyting algebra. Finally, we show how all this material can be used to express the category of finitely presented Heyting algebras as a category of fractions of a certain category with objects morphism between finite distributive lattices.

Legal argumentation in Mesopotamia since Ur III

2020 ◽  
Vol 9 (2) ◽  
pp. 243-282
Author(s):  
Andrew Schumann
Keyword(s):  
Modus Ponens ◽  
Legal Argumentation ◽  
Inference Rules ◽  
Logical Inference ◽  
High Ranking ◽  
Ur Iii ◽  
Correct Application

Abstract In this paper, I show that we can find some foundations of logic and legal argumentation in the tablets of Mesopotamia at least since the dynasty of Ur III. In these texts, we see the oldest correct application of logical inference rules (e.g. modus ponens). As concerns the legal argumentation established in Mesopotamia, we can reconstruct on the basis of the tablets the following rules of dispute resolutions during trials: (1) There are two parties of disputants: (i) a protagonist who formulates a standpoint and (ii) an antagonist who disagrees with the protagonist’s standpoint and formulates an alternative statement. (2) There is a rational judge represented by high-ranking citizens who should follow only logical conclusions from facts and law articles as premises.

On spectra, and the negative solution of the decision problem for identities having a finite nontrivial model

1975 ◽  
Vol 40 (2) ◽  
pp. 186-196 ◽  
Author(s):  
Ralph Mckenzie
Keyword(s):  
Model Problem ◽  
Recursive Algorithm ◽  
Finite Model ◽  
Positive Direction ◽  
First Order ◽  
Sharp Form ◽  
Universal Sentence ◽  
Order Language ◽  
Finite Set ◽  
The Universe

An algorithm has been described by S. Burris [3] which decides if a finite set of identities, whose function symbols are of rank at most 1, has a finite, nontrivial model. (By “nontrivial” it is meant that the universe of the model has at least two elements.) As a consequence of some results announced in the abstracts [2] and [8], it is clear that if the restriction on the ranks of function symbols is relaxed somewhat, then this finite model problem is no longer solvable by an algorithm, or at least not by a “recursive algorithm” as the term is used today.In this paper we prove a sharp form of this negative result; showing, by the way, that Burris' result is in a sense the best possible result in the positive direction. Our main result is that in a first order language whose only function or relation symbol is a 2-place function symbol (the language of groupoids), the set of identities that have no nontrivial model, is recursively inseparable from the set of identities such that the sentence has a finite model. As a corollary, we have that each of the following problems, restricted to sentences defined in the language of groupoids, is algorithmically unsolvable: (1) to decide if an identity has a finite nontrivial model; (2) to decide if an identity has a nontrivial model; (3) to decide if a universal sentence has a finite model; (4) to decide if a universal sentence has a model. We note that the undecidability of (2) was proved earlier by McNulty [13, Theorem 3.6(i)], improving results obtained by Murskiǐ [14] and by Perkins [17]. The other parts of the corollary seem to be new.

Implicational formulas in intuitionistic logic

1974 ◽  
Vol 39 (4) ◽  
pp. 661-664 ◽  
Author(s):  
Alasdair Urquhart
Keyword(s):  
Propositional Calculus ◽  
Modus Ponens ◽  
Equivalence Classes ◽  
Alternative Proof ◽  
Hilbert Algebra ◽  
Hilbert Algebras ◽  
Free Generators ◽  
Finite Set ◽  
Image Position ◽  
The Right

In [1] Diego showed that there are only finitely many nonequivalent formulas in n variables in the positive implicational propositional calculus P. He also gave a recursive construction of the corresponding algebra of formulas, the free Hilbert algebra In on n free generators. In the present paper we give an alternative proof of the finiteness of In, and another construction of free Hilbert algebras, yielding a normal form for implicational formulas. The main new result is that In is built up from n copies of a finite Boolean algebra. The proofs use Kripke models [2] rather than the algebraic techniques of [1].Let V be a finite set of propositional variables, and let F(V) be the set of all formulas built up from V ⋃ {t} using → alone. The algebra defined on the equivalence classes , by settingis a free Hilbert algebra I(V) on the free generators . A set T ⊆ F(V) is a theory if ⊦pA implies A ∈ T, and T is closed under modus ponens. For T a theory, T[A] is the theory {B ∣ A → B ∈ T}. A theory T is p-prime, where p ∈ V, if p ∉ T and, for any A ∈ F(V), A ∈ T or A → p ∈ T. A theory is prime if it is p-prime for some p. Pp(V) denotes the set of p-prime theories in F(V), P(V) the set of prime theories. T ∈ P(V) is minimal if there is no theory in P(V) strictly contained in T. Where X = {A1, …, An} is a finite set of formulas, let X → B be A1 →····→·An → B (ϕ → B is B). A formula A is a p-formula if p is the right-most variable occurring in A, i.e. if A is of the form X → p.

scholarly journals NNIL-formulas revisited: Universal models and finite model property

2020 ◽  
Author(s):  
Julia Ilin ◽  
Dick de Jongh ◽  
Fan Yang
Keyword(s):  
Direct Proof ◽  
Finite Model ◽  
Kripke Models ◽  
Model Property ◽  
Finite Model Property ◽  
Universal Models ◽  
Heyting Arithmetic ◽  
First Results

Abstract NNIL-formulas, introduced by Visser in 1983–1984 in a study of $\varSigma _1$-subsitutions in Heyting arithmetic, are intuitionistic propositional formulas that do not allow nesting of implication to the left. The first results about these formulas were obtained in a paper of 1995 by Visser et al. In particular, it was shown that NNIL-formulas are exactly the formulas preserved under taking submodels of Kripke models. Recently, Bezhanishvili and de Jongh observed that NNIL-formulas are also reflected by the colour-preserving monotonic maps of Kripke models. In the present paper, we first show how this observation leads to the conclusion that NNIL-formulas are preserved by arbitrary substructures not necessarily satisfying the topo-subframe condition. Then, we apply it to construct universal models for NNIL. It follows from the properties of these universal models that NNIL-formulas are also exactly the formulas that are reflected by colour-preserving monotonic maps. By using the method developed in constructing the universal models, we give a new direct proof that the logics axiomatized by NNIL-axioms have the finite model property.

Probabilities on finite models

1976 ◽  
Vol 41 (1) ◽  
pp. 50-58 ◽  
Author(s):  
Ronald Fagin
Keyword(s):  
Rate Of Convergence ◽  
Finite Subset ◽  
Asymptotic Estimate ◽  
Predicate Symbol ◽  
Relational Structure ◽  
Finite Model ◽  
First Order ◽  
Finite Models ◽  
Model Following ◽  
Finite Set

Let be a finite set of (nonlogical) predicate symbols. By an -structure, we mean a relational structure appropriate for . Let be the set of all -structures with universe {1, …, n}. For each first-order -sentence σ (with equality), let μn(σ) be the fraction of members of for which σ is true. We show that μn(σ) always converges to 0 or 1 as n → ∞, and that the rate of convergence is geometrically fast. In fact, if T is a certain complete, consistent set of first-order -sentences introduced by H. Gaifman [6], then we show that, for each first-order -sentence σ, μn(σ) →n 1 iff T ⊩ ω. A surprising corollary is that each finite subset of T has a finite model. Following H. Scholz [8], we define the spectrum of a sentence σ to be the set of cardinalities of finite models of σ. Another corollary is that for each first-order -sentence a, either σ or ˜σ has a cofinite spectrum (in fact, either σ or ˜σ is “nearly always“ true).Let be a subset of which contains for each in exactly one structure isomorphic to . For each first-order -sentence σ, let νn(σ) be the fraction of members of which a is true. By making use of an asymptotic estimate [3] of the cardinality of and by our previously mentioned results, we show that vn(σ) converges as n → ∞, and that limn νn(σ) = limn μn(σ).If contains at least one predicate symbol which is not unary, then the rate of convergence is geometrically fast.

Sign in / Sign up

Export Citation Format

Share Document