Journal article:
Samuel R. Buss.
"Intuitionistic validity in T-normal Kripke structures."
Annals of Pure and Applied Logic 59 (1993) 159-173.
Download conference article: postscript or PDF.
Abstract: Let T be a first-order theory. A T-normal Kripke structure is one in which every world is a classical model of T. This paper gives a characterization of the intuitionistic theory $\calH T$ of sentences intuitionistically valid (forced) in all $T$-normal Kripke structures and proves the corresponding soundness and completeness theorems. For Peano arithmetic (PA), the theory $\HPA$ is a proper subtheory of Heyting arithmetic (HA), so HA is complete but not sound for PA-normal Kripke structures..