Intuitionistic validity in \(T\)-normal Kripke structures
type: Item
instance of: scholarly article
title: Intuitionistic validity in \(T\)-normal Kripke structures
zbMATH Open document ID: 0802.03006
DOI: 10.1016/0168-0072(93)90091-Q
author: Samuel R. Buss
published in: Annals of Pure and Applied Logic
publication date: 1993-09-22T00:00:00Z
review text: Given any classical first-order theory \(T\), the author considers the set \({\mathcal H} T\) of all first-order sentences that are valid in every \(T\)- normal Kripke structure. A Kripke structure may be considered as a partially ordered set of classical structures and it is called \(T\)-normal iff each of these classical structures is a classical model of \(T\). The author's main motivation for studying such structures is his wish to extend model-theoretic techniques from classical logic to intuitionistic logic. He gives a very nice and surprising characterization of \({\mathcal H} T\): it is the set of all sentences that may be proved by intuitionistic logic from formulas of the form \(\theta^ \phi \to \phi\) where \(\theta\) is a semipositive formula (that is, each subformula of the form \(\theta_ 1\to \theta_ 2\) has \(\theta_ 1\) atomic; observe that \(\neg\psi\) abbreviates \(\psi\to \perp)\), \(\neg\theta\) follows by classical logic from \(T\), and \(\theta^ \phi\) is obtained from \(\theta\) by replacing each atomic subformula \(\chi\) of \(\theta\) by \(\chi\vee \phi\). In fact, \(\theta^ \phi\) is H. Friedman's \(\phi\)-translation of \(\theta\) [see \textit{H. Friedman}, Lect. Notes Math. 669, 21-27 (1978; Zbl 0396.03045)]. As a special case the author considers Peano arithmetic PA. He shows that \({\mathcal H}\text{PA}\) proves (intuitionistically) \(\Sigma_ 1^ 0\)-induction, and, using a very nice argument, that \({\mathcal H}\text{PA}\) does not prove \(\Pi_ 1^ 0\)-induction: \({\mathcal H}\text{PA}\) is a proper subtheory of Heyting arithmetic HA. The author concludes his paper with some questions. I have one more to ask: is it possible to make sense of the notion of a \(T\)-normal Kripke structure from an intuitionistic point of view, that is, if one uses an intuitionistic metalanguage?
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03C90
zbMATH DE Number: 416872
zbMATH Keywords: \(T\)-normal Kripke structure
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: Friedman's \(\phi\)- translation
zbMATH Keywords: Peano arithmetic
reviewed by: Wim Veldman
MaRDI profile type: Publication
cites work: Q4035302
cites work: Q4179016
cites work: Q3481670
cites work: Constructivism in mathematics. An introduction. Volume I
cites work: Finite Kripke models of HA are locally PA
full work available at URL: 0168-0072(93)90091-q
OpenAlex ID: W2092214433
Recommended article: Q5202656
Recommended article: Intuitionistic axiomatizations for bounded extension Kripke models.
Recommended article: Kripke semantics for intuitionistic Łukasiewicz logic
Recommended article: Q3027002
Recommended article: Decidable Kripke models of intuitionistic theories
Recommended article: Q4805536
Recommended article: Q3153244
Recommended article: Q5603863
Recommended article: Constants in Kripke Models for Intuitionistic Logic
Recommended article: Intuitionistic model constructions and normalization proofs
description: scientific article; zbMATH DE number 416872