Abstract:

It has been known since the 1920's that a classical metatheory can prove a form of completeness for classical propositional logic, while a strictly intuitionistic metatheory cannot do the same for its propositional case. Likewise, a similar phenomenon occurs with predicate logic, as known at least since 1962. This motivates the question of which intermediate logics between intuitionistic and classical (both in the propositional and the predicate case) are strong enough to prove their own completeness theorems; such self-sufficient logics are called reflexive. While making an overview of the evolution of these ideas, we will focus on a recent complete description of all reflexive logics due to Nathan Carter (2006 & 2008), which has also the interesting feature that it holds whether one uses Tarskian or Kripke semantics. We will later argue on up to which extent self-sufficiency is a way of telling how "satisfactory" a logic can be. In particular, we shall see that the definition relies upon notions of theories, models and completeness which are classically equivalent but different intuitionistically. For instance, by introducing a slight modification in the notion of model, we will see how Veldman was lead in 1976 to an intuitionistic completeness proof for intuitionistic predicate logic with respect to a (slightly) modified Kripke semantics, which therefore highlights the importance of the question of what should the correct definition of constructive model be.