Kripke Models for Intuitionistic Theories with Decidable Atomic Formulas
Publications de l'Institut Mathématique, _N_S_36 (1984) no. 50, p. 3
Some intuitionistic theories, notably Heyting's Arithmetic,
have decidable atomic formulas. We show that in Kripke models of such
theories, classical structures at the nodes of a Kripke model satisfy a
significant fragment of corresponding theories. In particular, all
consequences which are in prenex normal form hold classically.
Classification :
03B50 03C40
@article{PIM_1984_N_S_36_50_a0,
author = {Zoran Markovi\'c},
title = {Kripke {Models} for {Intuitionistic} {Theories} with {Decidable} {Atomic} {Formulas}},
journal = {Publications de l'Institut Math\'ematique},
pages = {3 },
year = {1984},
volume = {_N_S_36},
number = {50},
language = {en},
url = {http://geodesic.mathdoc.fr/item/PIM_1984_N_S_36_50_a0/}
}
Zoran Marković. Kripke Models for Intuitionistic Theories with Decidable Atomic Formulas. Publications de l'Institut Mathématique, _N_S_36 (1984) no. 50, p. 3 . http://geodesic.mathdoc.fr/item/PIM_1984_N_S_36_50_a0/