scholarly journals On the admissible rules of intuitionistic propositional logic

2001 ◽  
Vol 66 (1) ◽  
pp. 281-294 ◽  
Author(s):  
Rosalie Iemhoff
Keyword(s):  
Propositional Logic ◽  
Proof System ◽  
Intuitionistic Propositional Logic ◽  
Admissible Rules

AbstractWe present a basis for the admissible rules of intuitionistic propositional logic. Thereby a conjecture by de Jongh and Visser is proved. We also present a proof system for the admissible rules, and give semantic criteria for admissibility.

scholarly journals A Syntactic Characterization of the Gabbay-de Jongh Logics

10.29007/1mcd ◽  
2018 ◽  
Author(s):  
Jeroen Goudsmit
Keyword(s):  
Propositional Logic ◽  
Sufficient Conditions ◽  
Intuitionistic Propositional Logic ◽  
Admissible Rules ◽  
Intermediate Logics ◽  
Refutation Systems ◽  
Refutation System

Skura syntactically characterised intuitionistic propositional logic among all intermediate logics by means of a Łukasiewicz-style refutation system. Another such syntactic characterisation is given by Iemhoff in terms of admissible rules. Here we offer a bridge between these results. That is to say, we provide sufficient conditions under which admissible rules yield a refutation system fully characterising the logic. In particular, we give a characterisation of the Gabbay–de Jongh logics by means of refutation systems employing ideas from admissibility.

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

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.

Sign in / Sign up

Export Citation Format

Share Document