Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
type: Item
instance of: scholarly article
title: Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
zbMATH Open document ID: 0882.03056
DOI: 10.1016/0168-0072(96)00002-4
author: James Lipton
author: Michael J. O'Donnell
published in: Annals of Pure and Applied Logic
publication date: 1998-03-12T00:00:00Z
review text: 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''.
reviewed by: Wim Veldman
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 933095
zbMATH Keywords: Kripke semantics
zbMATH Keywords: Läuchli semantics
zbMATH Keywords: classical interpretations of the negation-free part of intuitionistic propositional logic
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: realizability semantics
zbMATH Keywords: Brouwer-Heyting-Kolmogorov interpretation
zbMATH Keywords: classical metalanguage
MaRDI profile type: Publication
full work available at URL: 0168-0072(96)00002-4
OpenAlex ID: W2062936207
cites work: Q3914980
cites work: The foundations of mathematics. A study in the philosophy of science
cites work: Linear Läuchli semantics
cites work: Q4133603
cites work: Q3882452
cites work: The system CΔ of combinatory logic
cites work: Q5582318
cites work: Q3995720
cites work: Q3994895
cites work: Lambek's categorical proof theory and Läuchli's abstract realizability
cites work: The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1
cites work: The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
cites work: On the interpretation of intuitionistic number theory
cites work: Q3261419
cites work: Q5343325
cites work: Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
cites work: Q5509675
cites work: Connecting formal semantics to constructive intuitions
cites work: Q3727946
cites work: Q5619069
cites work: Q4010362
cites work: Intuitive counterexamples for constructive fallacies
cites work: Q4283246
cites work: Classical recursion theory. Vol. II
cites work: Q5559220
cites work: Propositional Calculus and Realizability
cites work: Q3310620
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Logical relations and the typed λ-calculus
cites work: Combinators, \(\lambda\)-terms and proof theory
cites work: Q4126323
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Well-foundedness in realizability
description: scientific article; zbMATH DE number 933095