Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels (Q1923579)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels |
scientific article |
Statements
Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels (English)
0 references
12 March 1998
0 references
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''.
0 references
Kripke semantics
0 references
Läuchli semantics
0 references
classical interpretations of the negation-free part of intuitionistic propositional logic
0 references
intuitionistic logic
0 references
realizability semantics
0 references
Brouwer-Heyting-Kolmogorov interpretation
0 references
classical metalanguage
0 references