Michał Stronkowski

Admissibility

A common way of presenting a logic is by giving a proof system: a set of axioms and rules from which proofs and theorems may be derived. But what is usually regarded as essential is not a particular proof system, but rather the set of theorems of a logic. This perspective is particularly visible in the study of propositional logics, which are often identified with their sets of theorems.

From this perspective, we have a certain freedom in choosing a proof system for a logic. For instance, one may prefer a short list of rules while someone else may prefer ease in finding proofs. But there are restrictions: axioms must be theorems, and rules must be admissible—that is, when applied to theorems, they preserve theoremhood.

The study of admissibility in propositional logics was brought into focus by Friedman's problem, which asks for the decidability of admissibility in intuitionistic propositional logic, and the various approaches to its solution.

This series of lectures is intended as a gentle introduction to this active area of research. We plan to discuss the following topics:

1. the distinction between derivability and admissibility,
2. actively and passively admissible rules (informally, depending on whether their premises can meaningfully occur together in a proof),
3. structurally complete and actively structurally complete logics (i.e., logics where every admissible rule is derivable, or every active admissible rule is derivable, respectively),
4. the connection with unification theory.

We will mainly use semantic tools such as algebras and Kripke frames.