Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels (Q1923579): Difference between revisions

The authors study classical interpretations of the negation-free part of intuitionistic propositional logic. They maintain that a ``correct'' interpretation of intuitionistic logic should in some sense reflect the perhaps somewhat vague notions one had in mind when setting up the calculus. The authors compare Kripke's and Läuchli's completeness theorems and argue that the second one is ``correct'' but the first one is not. In their view, Läuchli's semantics is the better one, as it is a realizability semantics, that keeps rather close to the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic. They do not find convincing the usual ``explanation'' of Kripke models by means of ``stages of knowledge''. The authors use a classical metalanguage. It is not to be expected that the intuitionist's intentions may be rendered faithfully in a classical language but the authors do not discuss this problem. I found the paper a bit long, somewhat repetitive, and not accurate in every detail. For instance, Definition 3.1 presupposes Definition 4.3, and Definition 3.2, as it stands, is not comprehensible. The argument is sometimes muddled, as on page 191, lines 13-23. In Section 2, the authors treat ``proof formulae'' simultaneously as ``character strings'' and as ``abstract formal objects''. They thus fail to make a distinction between a syntactic object and its intended meaning. I also found it impossible to understand the authors' description of the operation ``lambda-abstraction''.