We prove that the first-order logic of CZF is intuitionistic first-order logic. To do so, we introduce a new model of transfinite computation (Set Register Machines) and combine the resulting notion of realisability with Beth semantics. On the way, we also show that the propositional admissible rules of CZF are exactly those of intuitionistic propositional logic.

The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules.

We investigate the computational complexity of deciding whether a given inference rule is admissible for some modal and superintuitionistic logics. We state a broad condition under which the admissibility problem is coNEXP-hard. We also show that admissibility in several well-known systems (including GL, S4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems.

We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia (...) theorem and the theory of modal companions to systems of multiple-conclusion rules or (finitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property. (shrink)

This paper contains a brief overview of the area of admissible rules with an emphasis on results about intermediate and modal propositional logics. No proofs are given but many references to the literature are provided.

This paper contains a proof-theoretic account of unification in 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 presented and these results are extended to negationless fragments. In particular, a syntactic proof of Ghilardi’s result that $\mathsf {S4}$ has finitary unification is provided. In this approach the relation between classical valuations, projective unifiers, and admissible rules is clarified.

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 it provides an extension to multi–conclusion consequence relations that is more general than the one usually encountered in the literature on admissibility. The notion of a rule scheme is introduced to capture 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, and that such extensions capture the intuitive idea of extending a logic by a rule. (shrink)

If the Visser rules are admissible for an intermediate logic, they form a basis for the admissible rules of the logic. How to characterize the admissible rules of intermediate logics for which not all of the Visser rules are admissible is not known. In this paper we give a brief overview of results on admissible rules in the context of intermediate logics. We apply these results to some well-known intermediate logics. We provide natural examples of logics for which the Visser (...) rule are derivable, admissible but nonderivable, or not admissible. (shrink)

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

The Visser rules form a basis of admissibility for the intuitionistic propositional calculus. We show how one can characterize the existence of covers in certain models by means of formulae. Through this characterization, we provide a new proof of the admissibility of a weak form of the Visser rules. Finally, we use this observation, coupled with a description of a generalization of the disjunction property, to provide a basis of admissibility for the intermediate logics BD2 and GSc.

In this paper we study the admissible rules of intermediate logics. We establish some general results on extensions 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.

Many intermediate logics, even extremely well-behaved ones such as IPC, lack the finite model property for admissible rules. We give conditions under which this failure holds. We show that frames which validate all admissible rules necessarily satisfy a certain closure condition, and we prove that this condition, in the finite case, ensures that the frame is of width 2. Finally, we indicate how this result is related to some classical results on finite, free Heyting algebras.

Rybakov proved that the admissible rules of $\mathsf {IPC}$ are decidable. We give a proof of the same theorem, using the same core idea, but couched in the many notions that have been developed in the mean time. In particular, we illustrate how the argument can be interpreted as using refinements of the notions of exactness and extendibility.

Refutation systems are formal systems for inferring the falsity of formulae. These systems can, in particular, be used to syntactically characterise logics. In this paper, we explore the close connection between refutation systems and admissible rules. We develop technical machinery to construct refutation systems, employing techniques from the study of admissible rules. Concretely, we provide a refutation system for the intermediate logics of bounded branching, known as the Gabbay–de Jongh logics. We show that this gives a characterisation of these logics (...) in terms of their admissible rules. To illustrate the technique, we also provide a refutation system for Medvedev’s logic. (shrink)

Propositional logic is understood as a set of theorems defined by a deductive system: a set of axioms and a set of rules. Superintuitionistic logic is a logic extending intuitionistic propositional logic \. A rule is admissible for a logic if any substitution that makes each premise a theorem, makes the conclusion a theorem too. A deductive system \ is structurally complete if any rule admissible for the logic defined by \ is derivable in \. It is known that any (...) logic can be defined by a structurally complete deductive system—its structural completion. The main goal of the paper is to study the following problem: given a superintuitionistic logic L, is the structural completion of L hereditarily structurally complete? It is shown that, on the one hand, there is continuum many of such logics, including \, and many of its standard extensions. On the other hand, there is continuum many superintutitionistic logics structural completion of which is not hereditarily structurally complete. It is observed that the class of hereditarily structurally complete superintuitionistic consequence relations does not have the smallest element and it contains continuum many members lacking the finite model property. The following statement is instrumental in obtaining negative results: if a Lindenbaum algebra of formulas on one variable is finite and has more than 15 elements, then a structural completion of such a logic is not hereditarily structurally complete. (shrink)

Uniform infinite bases are defined for the single-conclusion and multiple-conclusion admissible rules of the implication–negation fragments of intuitionistic logic and its consistent axiomatic extensions . A Kripke semantics characterization is given for the structurally complete implication–negation fragments of intermediate logics, and it is shown that the admissible rules of this fragment of form a PSPACE-complete set and have no finite basis.

A deductive system is said to be structurally complete if its admissible rules are derivable. In addition, it is called hereditarily structurally complete if all its extensions are structurally complete. Citkin (1978) proved that an intermediate logic is hereditarily structurally complete if and only if the variety of Heyting algebras associated with it omits five finite algebras. Despite its importance in the theory of admissible rules, a direct proof of Citkin’s theorem is not widely accessible. In this paper we offer (...) a self-contained proof of Citkin’s theorem, based on Esakia duality and the method of subframe formulas. As a corollary, we obtain a short proof of Citkin’s 2019 characterization of hereditarily structurally complete positive logics. (shrink)