scholarly journals The decidability of dependency in intuitionistic propositional logic

1995 ◽  
Vol 60 (2) ◽  
pp. 498-504 ◽  
Author(s):  
Dick de Jongh ◽  
L. A. Chagrova
Keyword(s):  
Propositional Logic ◽  
Infinite Sequence ◽  
Propositional Calculus ◽  
Interpolation Theorem ◽  
Intuitionistic Propositional Logic ◽  
Uniform Interpolation

AbstractA definition is given for formulae A1, …, An in some theory T which is formalized in a propositional calculus S to be (in)dependent with respect to S. It is shown that, for intuitionistic propositional logic IPC, dependency (with respect to IPC itself) is decidable. This is an almost immediate consequence of Pitts’ uniform interpolation theorem for IPC. A reasonably simple infinite sequence of IPC-formulae Fn (p, q) is given such that IPC-formulae A and B are dependent if and only if at least on of the Fn (A, B) is provable.

scholarly journals On an interpretation of second order quantification in first order intuitionistic propositional logic

1992 ◽  
Vol 57 (1) ◽  
pp. 33-52 ◽  
Author(s):  
Andrew M. Pitts
Keyword(s):  
Propositional Logic ◽  
Heyting Algebra ◽  
Propositional Calculus ◽  
Interpolation Theorem ◽  
Second Order ◽  
Heyting Algebras ◽  
Intuitionistic Propositional Logic ◽  
First Order ◽  
Intuitionistic Propositional Calculus ◽  
Algebraic Counterpart

AbstractWe prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, ϕ, built up from propositional variables (p, q, r, …) and falsity (⊥) using conjunction (∧), disjunction (∨) and implication (→). Write ⊢ϕ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula ϕ there exists a formula Apϕ (effectively computable from ϕ), containing only variables not equal to p which occur in ϕ, and such that for all formulas ψ not involving p, ⊢ψ → Apϕ if and only if ⊢ψ → ϕ. Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions.An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra.

The metatheory of the classical propositional calculus is not axiomatizable

1985 ◽  
Vol 50 (2) ◽  
pp. 451-457 ◽  
Author(s):  
Ian Mason
Keyword(s):  
Propositional Logic ◽  
Propositional Calculus ◽  
Interpolation Property ◽  
Interpolation Theorem ◽  
Order Logic ◽  
First Order Logic ◽  
Elementary Property ◽  
Classical Propositional Logic ◽  
Open Problems ◽  
First Order

In this paper we investigate the first order metatheory of the classical propositional logic. In the first section we prove that the first order metatheory of the classical propositional logic is undecidable. Thus as a mathematical object even the simplest of logics is, from a logical standpoint, quite complex. In fact it is of the same complexity as true first order number theory.This result answers negatively a question of J. F. A. K. van Benthem (see [van Benthem and Doets 1983]) as to whether the interpolation theorem in some sense completes the metatheory of the calculus. Let us begin by motivating the question that we answer. In [van Benthem and Doets 1983] it is claimed that a folklore prejudice has it that interpolation was the final elementary property of first order logic to be discovered. Even though other properties of the propositional calculus have been discovered since Craig's orginal paper [Craig 1957] (see for example [Reznikoff 1965]) there is a lot of evidence for the fundamental nature of the property. In abstract model theory for example one finds that very few logics have the interpolation property. There are two well-known open problems in this area. These are1. Is there a logic satisfying the full compactness theorem as well as the interpolation theorem that is not equivalent to first order logic even for finite models?2. Is there a logic stronger than L(Q), the logic with the quantifierthere exist uncountably many, that is countably compact and has the interpolation property?

scholarly journals On density of truth of the intuitionistic logic in one variable

2008 ◽  
Vol DMTCS Proceedings vol. AI,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Propositional Logic ◽  
Propositional Variable ◽  
Intuitionistic Propositional Logic ◽  
International Audience

International audience In this paper we focus on the intuitionistic propositional logic with one propositional variable. More precisely we consider the standard fragment $\{ \to ,\vee ,\bot \}$ of this logic and compute the proportion of tautologies among all formulas. It turns out that this proportion is different from the analog one in the classical logic case.

scholarly journals An ASP Approach to Generate Minimal Countermodels in Intuitionistic Propositional Logic

2019 ◽  
Author(s):  
Camillo Fiorentini
Keyword(s):  
Propositional Logic ◽  
Answer Set Programming ◽  
Kripke Model ◽  
Kripke Semantics ◽  
Minimal Models ◽  
Intuitionistic Propositional Logic ◽  
Answer Set

Intuitionistic Propositional Logic is complete w.r.t. Kripke semantics: if a formula is not intuitionistically valid, then there exists a finite Kripke model falsifying it. The problem of obtaining concise models has been scarcely investigated in the literature. We present a procedure to generate minimal models in the number of worlds relying on Answer Set Programming (ASP).

UNIFORM INTERPOLATION IN SUBSTRUCTURAL LOGICS

2014 ◽  
Vol 7 (3) ◽  
pp. 455-483 ◽  
Author(s):  
MAJID ALIZADEH ◽  
FARZANEH DERAKHSHAN ◽  
HIROAKIRA ONO
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Substructural Logics ◽  
Substructural Logic ◽  
Sequent Calculi ◽  
Structural Rule ◽  
Modal Propositional Logic ◽  
Uniform Interpolation ◽  
Classical Predicate

AbstractUniform interpolation property of a given logic is a stronger form of Craig’s interpolation property where both pre-interpolant and post-interpolant always exist uniformly for any provable implication in the logic. It is known that there exist logics, e.g., modal propositional logic S4, which have Craig’s interpolation property but do not have uniform interpolation property. The situation is even worse for predicate logics, as classical predicate logic does not have uniform interpolation property as pointed out by L. Henkin.In this paper, uniform interpolation property of basic substructural logics is studied by applying the proof-theoretic method introduced by A. Pitts (Pitts, 1992). It is shown that uniform interpolation property holds even for their predicate extensions, as long as they can be formalized by sequent calculi without contraction rules. For instance, uniform interpolation property of full Lambek predicate calculus, i.e., the substructural logic without any structural rule, and of both linear and affine predicate logics without exponentials are proved.

Sign in / Sign up

Export Citation Format

Share Document