Provability Logic and Admissible Rules
Rosalie Iemhoff
Abstract:
%Nr: DS-2001-04
%Author: Rosalie Iemhoff
%Title: Provability Logic and Admissible Rules
This thesis consists of two parts. In the first part the provability and
preservativity logic of Heyting Arithmetic are studied, and the second part
contains results in intuitionistic propositional logic. The two parts are
connected via admissible rules; they play a central role in the provability
logic of Heyting Arithmetic and are the main topic of the second part of the
thesis.
Up till now there are no axiomatizations known for provability logics of
constructive theories. However, in the first part of the thesis it is shown
that for many well-known properties of Heyting Arithmetic that are
expressible in provability logic, it is known whether they belong to the
logic or not. Therefore, it is argued that the system studied in the thesis
forms at least a very natural fragment, if not all, of the provability logic
of Heyting Arithmetic. The principles of this system are studied from the
modal point of view. Therefore, this part of the thesis can also be viewed
as a study in intuitionistic modal logic, in which surprising frame
properties become visible. It is shown that the given system is complete
with respect to a certain class of frames. The principles are also studied
separately and proved to be independent.
The second part of the thesis is about intuitionistic propositional logic.
First, a basis for the admissible rules of this logic is established. Then
it is shown that intuitionistic propositional logic is characterized by these
rules plus the Disjunction Property. In a similar way it is shown that every
finite part of the basis plus the Disjunction Property characterizes one of
the Gabbay-de Jongh logics. This shows that the characterization of
intuitionistic propositional logic is optimal; no finite part of the basis
characterizes it.