Presheaf semantics and independence results for some non-classical first- order logics (Q582278)

It is well-known that Kripke semantics for intuitionistic logic can be generalized by introducing interpretations of the logical language into toposes of set-valued functors defined on categories instead of preorders. Formally, a model is a triple \((C,X,{\mathcal I})\), where C is a small category, \(X: C\to Set\) is a functor and \({\mathcal I}\) is a map associating with every n-ary predicate letter a subobject of the product functor \(X^ n\) (the first order language considered is one-sorted). The critical clauses for implication and universal quantifiers are the following ones (let us use the letters \(\alpha,\beta,...\) in order to indicate the objects of C, the letters \(k,\ell,..\). in order to indicate the arrows of C and the letters \(\mu,\nu,...\) in order to indicate, given an object, say \(\alpha\), the \(\alpha\)-assignments, i.e. the functions \(N\to X_{\alpha})\) \(\mu\vDash_{\alpha}A_ 1\to A_ 2\) iff for every \(\beta\) and \(k: \alpha \to \beta,\) if \(X_ k\circ \mu \vDash_{\beta}A_ 1\) then \(X_ k\circ \mu \vDash_{\beta}A_ 2;\) \(\mu\vDash_{\alpha}\forall x_ iA\) iff for every \(\beta,\) \(k: \alpha \to \beta\) and \(b\in X_{\beta},\) \((X_ k\circ \mu)^{[b/i]}\vDash_{\beta}A.\) The core part of the paper deals with the intermediate logic D-J obtained by adding to intuitionistic logic the weak excluded middle schema \(\neg A\vee \neg \neg A\) and the constant domain schema \(\forall x_ i(A\vee B)\to (\forall x_ iA)\vee B\) (provided \(x_ i\) is not free in B). Necessary and sufficient conditions are easily found for a pair \(<C,X>\) to be such that these two schemata hold in \(<C,X,{\mathcal I}>\) for every \({\mathcal I}\). These conditions are used in order to show the independence of the formula \[ [\forall x_ 0((p_ 1\to (p_ 2\vee P(x_ 0)))\vee (p_ 2\to (p_ 1\vee P(x_ 0))))]\quad \wedge \quad [\neg \forall x_ 0P(x_ 0)]\quad \to \quad [(p_ 1\to p_ 2)\vee (p_ 2\to p_ 1)] \] valid in all the Kripke frames for the logic D-J, thus obtaining the incompleteness theorem for it with respect to Kripke semantics. In the last section of the paper, additional incompleteness results are found for modal logics (it is shown that the quantified extension of any normal modal propositional logic extending S4.1 and not collapsing the modalities is not Kripke complete).