Preprints by Rosalie Iemhoff

338

«Questions and dependency in intuitionistic logic»

igitur archive I. Ciardelli R. Iemhoff F. Yang April 5, 2017

In recent years, the logic of questions and dependencies has been investigated in the closely related frameworks of inquisitive logic and dependence logic. These investigations have assumed classical logic as the background logic of statements, and added formulas expressing questions and dependencies to this classical core. In this paper, we broaden the scope of these investigations by studying questions and dependency in the context of intuitionistic logic. We propose an intuitionistic team semantics, where teams are embedded within intuitionistic Kripke models. The associated logic is a conservative extension of intuitionistic logic with questions and dependence formulas. We establish a number of results about this logic, including a normal form result, a completeness result, and translations to classical inquisitive logic and modal dependence logic.

337

«Uniform interpolation and the existence of sequent calculi»

igitur archive R. Iemhoff February 20, 2017

General conditions on sequent calculi are formulated under which the intermediate and modal logics corresponding to the calculi have uniform interpolation. It follows that the intuitionistic versions of K and KD, as well as several other intuitionistic modal logics, have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying the general conditions. Thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.

336

«Intuitionistic modal logics and Dyckhoff's calculus»

igitur archive R. Iemhoff February 20, 2017

In 1992 Dyckhoff developed a sequent calculus for intuitionistic propositional logic in which proof search is terminating. In this paper this result is extended to several intuitionistic modal logics, including intuitionistic versions of the modal logics K and KD. Cut-free sequent calculi that are extensions of Dyckhoff's calculus are developed for these logics and are shown, by proof-theoretic means, to be equal to the more common sequent calculi for the intuitionistic modal logics considered here.

335

«Structural completeness in propositional logics of dependence»

igitur archive R. Iemhoff F. Yang September 10, 2015

In this paper we prove that three of the main propositional logics of dependence (including propositional dependence logic and inquisitive logic), none of which is structural, are structurally complete with respect to a class of substitutions under which the logics are closed. We obtain an analogous result with respect to stable substitutions, for the negative variants of some well-known intermediate logics, which are intermediate theories that are closely related to inquisitive logic.

334

«On the existence of alternative Skolemization methods»

igitur archive R. Iemhoff August 30, 2016

It is shown that no intermediate predicate logic that is sound and complete with respect to a class of frames, admits a strict alternative Skolemization method. In particular, this holds for intuitionistic predicate logic and several other well-known intermediate predicate logics. The result is proved by showing that the class of formulas without strong quantifiers as well as the class of formulas without weak quantifiers is sound and complete with respect to the class of constant domain Kripke models.

328

«Remarks on simple proofs»

igitur archive R. Iemhoff March 15, 2015

This note consists of a collection of observations on the notion of simplicity in the setting of proofs. It discusses its properties under formalization and its relation to the length of proofs, showing that in certain settings simplicity and brevity exclude each other. It is argued that when simplicity is interpreted as purity of method, different foundational standpoints may affect which proofs are considered to be simple and which are not.

325

«Uniform interpolation and sequent calculi in modal logic»

igitur archive R. Iemhoff March 28, 2015

A method is presented that connects the existence of uniform interpolants to the existence of certain sequent calculi. This method is applied to several modal logics and is shown to cover known results from the literature, such as the existence of uniform interpolants for the modal logic K. The results imply that for modal logics K4 and S4, which are known not to have uniform interpolation, certain sequent calculi cannot exist.

323

«Skolemization in intermediate logics of finite width»

igitur archive R. Iemhoff M. Baaz 22 January 2015

An alternative Skolemization method, which removes strong quantifiers from formulas, is presented that is sound and complete with respect to intermediate predicate logics of finite width. For logics without constant domains the method makes use of an existence predicate, while for logics with constant domains no additional predicate is necessary. In both cases an analogue of Hebrand's theorem is obtained as well. It is shown that for constant domain logics of finite width these results imply that interpolation holds for the logic once it holds for its propositional fragment.

314

«A note on consequence»

igitur archive R. Iemhoff September 2013

This paper contains a detailed account of the notion of admissibility in the setting of consequence relations. It is proved that the two notions of admissibility used in the literature coincide and provides and an extension to multi-conclusion consequence relations is provided that is more general than the one usually encountered in the literature on admissibility. The notion of a rule scheme is introduced to cover rules with side conditions, and it is shown that what is generally understood under the extension of a consequence relation by a rule can be extended naturally to rule schemes. It is shown that such extensions correctly capture the intuitive idea of extending a theory by a rule.

304

«On Rules»

igitur archive R. Iemhoff March 18 2013

This paper consists of a brief overview of the study of admissible rules.

297

«On unification and admissible rules in Gabbay-de Jongh logics»

igitur archive J. Goudsmit R. Iemhoff June 25 2012

In this paper we study the admissible rules of intermediate logics. We establish some general results on extension of models and sets of formulas. These general results are then employed to provide a basis for the admissible rules of the Gabbay–de Jongh logics and to show that these logics have finitary unification type.

296

«Unification in intermediate logics»

igitur archive R. Iemhoff P. Rozière April 3 2012

This paper contains a proof theoretic treatment of some aspects of unification in intermediate logics. It is shown that many existing results can be extended to fragments that at least contain implication and conjunction. For such fragments the connection between valuations and most general unifiers is clarified, and it is shown how from the closure of a formula under the Visser rules a proof of the formula under a projective unifier can be obtained. This implies that in the logics considered, for the n-unification type to be finitary it suffices that the m-th Visser rule is admissible for a sufficiently large m. At the end of the paper it is shown how these results imply several well-known results from the literature.

295

«Unification in transitive reflexive modal logics»

igitur archive R. Iemhoff February 2 2012

This paper contains a proof-theoretic account of unification in (fragments of) transitive reflexive modal logics, which means that the reasoning is syntactic and uses as little semantics as possible. New proofs of theorems on unification types are given and these results are extended to fragments. It is shown that transitive reflexive fragments that contain at least implication and conjunction have finitary unification, and that in the absence of disjunction they have unitary unification. The relation between classical valuations and projective unifiers is clarified, and it is shown that also in fragments the Visser rules form a basis for the admissible rules once they are admissible.

291

«Krachtige Bewijzen»

igitur archive R. Iemhoff November 2011

In 2009 werd mij door de Nederlandse Wetenschaps Organisatie een Vidi beurs toegekend voor het project “The power of constructive proofs”. Het project is wiskundig van aard en valt binnen het NWO gebiedsbestuur Exacte Wetenschappen. Op uitnodiging van het ANTW heb ik een artikel geschreven dat gaat over die vakgebieden in de wiskundige logica, de Bewijstheorie en het Constructivisme, waarop het project betrekking heeft. Het is geen alomvattend overzicht van die gebieden, maar belicht die thema’s die voor het project van belang zijn.

277

«The eskolemization of universal quantifiers»

igitur archive R. Iemhoff June 2009

This paper is a sequel to the papers [4,6] in which an alternative skolemization method called ekolemization was introduced that, when applied to the strong existential quantifiers in a formula, is sound and complete for constructive theories. Based on that method an analogue of Herbrand’s theorem was proved to hold as well. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property the method is sound and complete for all formulas. We prove a Herbrand theorem and, as an example, apply the method to several constructive theories. We show that for the theories with decidable quantifier-free fragment, also the strong existential quantifier fragment is decidable.

276

«Kripke models for subtheories of CZF»

igitur archive R. Iemhoff June 2009

In this paper a method to construct Kripke models for subtheories of constructive set theory is introduced that uses constructions from classical model theory such as constructible sets and generic extensions. Under the main construction all axioms except the collection axioms can be shown to hold in the constructed Kripke model. It is shown that by carefully choosing the classical models various instances of the collection axioms, such as exponentiation, can be forced to hold as well. The paper does not contain any deep results. It consists of first observations on the subject, and is meant to introduce some notions that could serve as a foundation for further research.

274

«Proof theory for admissible rules»

igitur archive R. Iemhoff G. Metcalfe April 2009

Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. With minor restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the logics.

273

«Eskolemization in intuitionistic logic»

igitur archive M. Baaz R. Iemhoff April 2009

In [2] an alternative skolemization method called eskolemization was introduced that is sound and complete for existence logic with respect to existential quantifiers. Existence logic is a conservative extension of intuitionistic logic by an existence predicate. Therefore eskolemization provides a skolemization method for intuitionistic logic as well. All proofs in [2] were semantical. In this paper a proof-theoretic proof of the completeness of eskolemization with respect to existential quantifiers is presented.

270

«Hypersequent systems for the admissible rules of modal and intermediate logics»

igitur archive R. Iemhoff G. Metcalfe November 2008

The admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In a previous paper by the authors, formal systems for deriving the admissible rules of Intuitionistic Logic and a class of modal logics were defined in a proof-theoretic framework where the basic objects of the systems are sequent rules. Here, the framework is extended to cover derivability of the admissible rules of intermediate logics and a wider class of modal logics, in this case, by taking hypersequent rules as the basic objects.

263

«On Skolemization in constructive theories»

igitur archive M. Baaz R. Iemhoff February 2008

In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand’s theorem for intuitionistic logic. The orderization method is applied to the constructive theories of equality and groups.

256

«On Skolemization in constructive theories»

igitur archive M. Baaz R. Iemhoff February 2008

In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand’s theorem for intuitionistic logic. The orderization method is applied to the constructive theories of equality and groups.

250

«Proof theory for admissible rules»

igitur archive R. Iemhoff G. Metcalfe February 2007

The admissible rules of a logic are the rules under which the set of theorems of the logic is closed. In this paper a Gentzen-style framework is introduced for defining analytic proof systems that derive the admissible rules of various non-classical logics. Just as Gentzen systems for derivability treat sequents as basic objects, for admissibility, sequent rules are basic. Proof systems are defined here for the admissible rules of classes of both modal logics, including K4, S4, and GL, and intermediate logics, including Intuitionistic logic IPC, De Morgan (or Jankov) logic KC, and logics BCn (n = 1, 2, . . .) with bounded cardinality Kripke models. With minor restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the corresponding logics.

201

«On the admissible rules of intuitionistic propositional logic»

igitur archive R. Iemhoff January 2000

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

193

«A modal analysis of some principles of the provability logic of Heyting Arithmetic»

igitur archive R. Iemhoff January 1999

Besides the well-known principles K, K4 and L, the Leivant principle (AVВ)→ (AVB) and the Formalized Markov scheme  ¬¬ (A→ VBi) → (A→ VВi) are principles of the Provability Logic of (intuitionistic) Heyting Arithmetic. In this paper they are studied from a modal logical point of view. They are characterized, separate as well as in combination with the other principles, in terms of frame properties, and the finite model property is established. In order to make the paper self-contained intuitionistic modal logic is introduced and similar results for K4 and L, which were already known, are proved again.