Intuitionistic validity in T-normal Kripke structures
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?
- scientific article; zbMATH DE number 4195940
- Intuitionistic axiomatizations for bounded extension Kripke models.
- Kripke semantics for intuitionistic Łukasiewicz logic
- Publication:3027002
- Decidable Kripke models of intuitionistic theories
- scientific article; zbMATH DE number 1907113
- scientific article; zbMATH DE number 1823848
- scientific article; zbMATH DE number 3323814
- Constants in Kripke Models for Intuitionistic Logic
- Intuitionistic model constructions and normalization proofs
- Constructivism in mathematics. An introduction. Volume I
- Finite Kripke models of HA are locally PA
- scientific article; zbMATH DE number 4152338 (Why is no real title available?)
- scientific article; zbMATH DE number 176198 (Why is no real title available?)
- scientific article; zbMATH DE number 3614784 (Why is no real title available?)
- Interpretations of intuitionist logic in non-normal modal logics
- Intuitionistic axiomatizations for bounded extension Kripke models.
- Not all Kripke models of \(\mathsf{HA}\) are locally \(\mathsf{PA}\)
- A semantic approach to conservativity
- scientific article; zbMATH DE number 1463152 (Why is no real title available?)
- 2003 Annual Meeting of the Association for Symbolic Logic
- 1999 European Summer Meeting of the Association for Symbolic Logic
- Homomorphisms and chains of Kripke models
- Intuitionistic open induction and least number principle and the Buss operator
- Intermediate logics and the de Jongh property
- The provably total functions of basic arithmetic and its extensions
- Finite sets and infinite sets in weak intuitionistic arithmetic
This page was built for publication: Intuitionistic validity in \(T\)-normal Kripke structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685055)
