\documentstyle[12pt]{article}
\newcommand{\A}{\mbox{$\cal A$}}
\newcommand{\B}{\mbox{$\cal B$}}
\newcommand{\D}{\mbox{$\cal D$}}
\newcommand{\C}{\mbox{$\cal C$}}
\newcommand{\F}{\mbox{$\cal F$}}
\newcommand{\T}{\mbox{$\cal T$}}
\newcommand{\M}{\mbox{$\cal M$}}
\newcommand{\G}{\mbox{$\cal G$}}
\newcommand{\R}{\mbox{$\cal R$}}
\newcommand{\E}{\mbox{$\cal E$}}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{definition}{Definition}
\begin{document}

\begin{center}{{\bf COMPUTABLE KRIPKE MODELS AND COMPLETENESS\\

\

Hajime Ishihara \  and \  Bakhadyr Khoussainov}}
\end{center}

In classical computable model theory the completeness theorem
states that every computable complete theory has a decidable model, 
that is, a model whose satisfaction predicate is computable.
In intuitionistic predicate logic ($IPL$), the completeness 
theorem states that every theory $T$ has a Kripke model $\M$
such that for all sentences $\phi$, 
$\phi$ is forced in $\M$ iff $T$ proves $\phi$ [4] [8] [9].  We call 
such models {\bf adequate}. We investiagte effectiveness of this 
completeness result and its versions.  \  

Let $\M=(W,\leq, D,V)$ be a Kripke model, where $(W,\leq)$ is a p.o. set 
(base),  $D$ is a domain function, $V$ is a valuation, and $(W,\leq, D)$ 
is the frame of $\M$ [4] [8]. Gabbay proved that if a theory 
 $T$ is computable and finitely axiomatized in $IPL$, 
then $T$ has a Kripke model $\M=(W,\leq, D,V)$ 
in which the forcing of atomic sentences and the base $(W,\leq)$  are c.e. [3]. In [5] it is shown that if $T$ is a computable theory, then $T$ 
has an adequate Kripke model with 
computable forcing and a $\Pi_2^0$--base. 

\begin{definition}
A Kripke model $(W,\leq, D,V)$ is {\bf decidable ($X$--decidable)} 
if the forcing in $\M$ and the base $(W,\leq)$ are computable 
(computable in $X$). 
\end{definition} 

A Kripke model is  a {\bf $K$--model} if its frame belongs to a fixed 
class $K$ of frames.  Let $S$ be a logic between 
$IPL$ and the classical predicate logic ($CPL$).  \  $S$ is {\bf $K$--complete} if: 
\ 1) Every $K$--model satisfies all sentences from $S$; 
\  2) If a sentence 
$\phi$ is not deducible from $S$, then there is a $K$--model 
which does not force $\phi$.  \  $S$ is {\bf complete} if it is 
$K$--complete for some $K$.  $IPL$, $CPL$, 
$CD=IPL+\forall x (\alpha(x) \vee \beta) \rightarrow 
\forall x \alpha(x) \vee \beta,$
where $x$ is not free in $\beta$, 
$DL=IPL+(\alpha \rightarrow \beta) \vee (\beta \rightarrow \alpha)$, 
$QJ=IPL+\neg \alpha  \vee \neg \neg \alpha$, 
$KJ=QJ+\forall x \neg \neg \alpha  \rightarrow \neg \neg \forall x \alpha$,
$KJC=QJ+KJ+CD$ and many more are examples of complete logics 
[1] [2] [3] [4] [8].  There exist incomplete logics as well. 
A theory in logic $S$ is {\bf saturated} if the condition 
$\alpha \vee \beta \in T$ implies that either $\alpha \in T$ or 
$\beta \in T$,
and if $\exists x \alpha(x) \in T$, then $\alpha(c) \in T$ 
for some constant $c$. Every (computable) theory can be 
expanded to a (computable) 
saturated theory.  A frame $(W,\leq, D)$ is a  
{\bf frame with maximum element}
if there is a $w \in W$ such that for all $v \in W$, $w\geq v$.
\begin{definition}
A theory $T$ in $S$ is {\bf complete for $K$} if 
for every $\phi$ not deducible from $T$ there is an adequate 
$K$--model of $T$  which does not force $\phi$. 
\end{definition}
Here is a list of some results.
\begin{theorem} \  
1) Any computable theory in $CPL$ is complete for the class 
of decidable Kripke models over antichains. \\ 
2) Any computable theory in $IPL$ is complete for the class of 
decidable Kripke models over trees.\\
3)  Any computable theory in $CD$ is complete for the class of 
decidable Kripke models over constant domain frames.\\
4)  Any computable and saturated  theory  
in $DL$ is complete for the class of decidable Kripke models 
over linearly ordered frames.\\
5)  Any computable and saturated  theory 
in $KJ$ is complete for the class of ${\bf 0}'$--decidable 
Kripke models over frames with maximum elements.\\
6)  Any computable and saturated theory in 
$QJ$ is complete for the class of ${\bf 0}^{\omega}$--decidable 
Kripke models over directed frames.\\
7) Any computable and saturated theory in 
$KJC$ is complete for the class of ${\bf 0}'$--decidable Kripke models
over constant domain frames with maximum elements.
\end{theorem}
The proofs of these results are in [6] and obtained by effectiveizing
completeness proofs from [1] [2] [3] [7].

\

{\bf References} \  \ [1] \  G. Corsi and S. Ghilardi, Directed Frames, 
Archive for Mathematical Logic, v.29, N.3, p. 53-67, 1989.\  \ 
[2] \ G. Corsi, Completeness Theorem for Dummett's LC 
Quantified and Some of Its Extensions, Studia Logica, 51, 
p.318--335, 1992. \  \ 
[3] \ D. Gabbay, Sematical Investigations in Heyting's 
Intuitionistic Logic, D. Reidel, Dordrecht, 1981. 
\  \ [4]  \  
D.van Dalen, Intuitionistic Logic, in Handbook of Philosofical
Logic, edited by D. Gabbay and F. Guenthner, Kluwer Academic Publishers, 
1981.\  \  [5]  \ H. Ishihara, B. Khoussainov, A. Nerode, 
Decidable Kripke Models of Intuitinistic Theories, to appear. \   \ 
[6]  \  H. Ishihara, B. Khoussainov, A. Nerode, 
Computable Kripke Models and  Intermediate Logics, in preparation. \   
\ [7] \ H. Ono, 
Model Extension Theorem and Craig's Interpolation Theorem for 
Intermediate Predicate Logics, Reports on Mathematical Logic, 15, p. 41-58. \   \ 
[8]  \  C. A. Smorynski, Applications of Kripke Models, in Mathematical 
Investigation of Intuitionstic Arithmetic and Analysis, ed. A.S. Troelstra, 
Lecture Notes in Math., Springer Verlag, 1983. \  \  [9] \  A.S. Troelstra,
 D. van Dalen, Constructivism in Mathematics, vol. 1, North--Holland, 1988.
\end{document}