Intuitionistic Logic and Computability
Radboud University Nijmegen
Intuitionistic logic is a logic formalised by Heyting, based on Brouwer’s programme of intuitionism. Roughly speaking, intuitionistic logic is what one obtains if one drops the so-called “law of excluded middle”, stating that for every statement P either P holds or P does not hold, from classical logic. There are various ways to provide a semantics for this formalism, of which we are particularly interested in the ones which are somehow connected to computation.
In this talk we will look at the Medvedev and Muchnik lattices, which are algebraic structures naturally arising in computability theory. These algebraic structures are so-called ‘Brouwer algebras’, which are structures to which we can assign a non-classical propositional logic in a natural way. It turns out that, unfortunately, the theory assigned to the Medvedev and Muchnik lattices is not intuitionistic propositional logic (IPC): in fact, their theory is IPC plus the “weak law of the excluded middle” stating that for every statement P either P does not hold or P does not not hold.
However, quite remarkably it turns out that this deficiency can be repaired, a fact first proven by Skvortsova. We will sketch how this works, discussing recent extensions of Skvortsova’s result.