<p>For (propositional) <a href="http://en.wikipedia.org/wiki/Intermediate_logic" rel="nofollow noreferrer">intermediate logics</a>, a decision procedure for satisfiability cannot generally be turned into a decision procedure for (non)validity, because all intermediate logics happen to have the same set of satisfiable formulas, namely, the set of classically satisfiable formulas, whereas some (a majority of) intermediate logics are undecidable.</p>

<p>(To make sense of the juxtaposition, all of the intermediate logics should be considered in the language of the weakest one, i.e., $\land$, $\lor$, $\to$, and $\neg$ or $\bot$.)</p>

<p>The coincidence of SAT's for these logics is a consequence of <a href="http://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic" rel="nofollow noreferrer">Glivenko theorem</a> (which can be paraphrased by asserting that $\neg\varphi$ is provable classically iff it is provable intuitionistically, for any formula $\varphi$). See also <a href="https://mathoverflow.net/a/139296">this post</a>.</p>

CC BY-SA 3.0
2015-03-30T13:16:25.047Z
Any references on undecidability of the decision procedure for intermediate logics?
cody
CC BY-SA 3.0
2015-03-31T12:53:29.453Z
@cody I had no particular undecidability result in mind, actually. The quantification `a majority of' referred to the fact that the lattice of intermediate logics has the cardinality of the continuum, so we can't have decision procedures for all of these logics. The cardinality result for intermediate logics can be obtained by employing Jankov formulas.
anemone
CC BY-SA 3.0
2015-03-31T12:56:53.277Z
@cody Apparently Shehtman came up with a particular example of an undecidable propositional superintuitionistic logic (in a 1978 paper), but I'm not familiar with its particulars.
anemone
CC BY-SA 3.0
2015-03-31T13:55:52.493Z
It's a bit strange to give an undecidability argument by cardinality: I don't really consider something to be a logic if the axioms are not at least $\mathrm{r.e.}$! However I will gladly believe that there are undecidable intermediate logics, given how easy it is to build undecidable [propositional linear logics](http://www.csl.sri.com/users/lincoln/papers/llwork-complex.pdf).
cody
CC BY-SA 3.0
2015-03-29T21:20:07.080Z
2015-03-29T21:20:07.080Z
2017-04-13T12:57:54.777Z
anemone
<p>For propositional logic, a decision procedure for satisfiability can be turned
into a decision procedure for non-validity by giving it the negated
version of a formula.</p>

<p>Does this hold for all logics for which satisfiability is decidable? </p>

<p>More precisely:</p>

<p>Let $F$ be a set of well-formed formulas in some logic $L$. $F$ is closed under
negation, i.e. $f \in F \implies \neg f \in F$. Let $F'$ be a subset of $F$ such that
satisfiability of $F'$ is decidable. Let $F'' = \{ \neg f | f \in F' \}$. Is there a logic
$L$ for which satisfiability is decidable for $F'$ but not for $F''$?</p>

CC BY-SA 3.0
2015-03-25T21:08:30.190Z
Have you tried proving this statement one way or the other?
cody
CC BY-SA 3.0
2015-03-25T21:12:49.213Z
I believe there should be a logic for which satisfiability of F' is decidable but satisfiability of F'' is undecidable (but I can't come up with an example as my knowledge of different logics is limited).
Kobold
CC BY-SA 3.0
2015-03-25T21:31:47.280Z
Maybe you should consider the other possibility for a bit then :)
cody
CC BY-SA 3.0
2015-03-25T21:57:48.770Z
As an example, validity for the Bernays-Schoenfinkel fragment of first-order logic is decidable. Let that set be called $BS$. But does that mean that $BS' = \{ \neg f | f \in BS \}$ is decidable as well? I don't quite see it.
Kobold
CC BY-SA 3.0
2015-03-26T15:32:45.583Z
Hmmm. The answer seems to be negative, since I suspect that the $\forall^*\exists^*$ is undecidable. A careful examination of the proof should determine this. A quick google search comes up with [this](https://logic.rwth-aachen.de/~graedel/kalmar.pdf) survey.
cody
CC BY-SA 3.0
2015-03-26T15:33:17.977Z
I might add that this suggests that the question is on-topic on this site.
cody
<lo.logic><sat>
Deciding satisfiability and non-validity
Kobold
# Deciding satisfiability and non-validity

(Asked by: username_0 on 2015-03-25)

For propositional logic, a decision procedure for satisfiability can be turned
into a decision procedure for non-validity by giving it the negated
version of a formula.

Does this hold for all logics for which satisfiability is decidable?

More precisely:

Let $F$ be a set of well-formed formulas in some logic $L$. $F$ is closed under
negation, i.e. $f \in F \implies \neg f \in F$. Let $F'$ be a subset of $F$ such that
satisfiability of $F'$ is decidable. Let $F'' = \{ \neg f | f \in F' \}$. Is there a logic
$L$ for which satisfiability is decidable for $F'$ but not for $F''$?

**Tags:** lo.logic, sat

> **Comments:**
> **username_1**: Have you tried proving this statement one way or the other?  
> **username_0**: I believe there should be a logic for which satisfiability of F' is decidable but satisfiability of F'' is undecidable (but I can't come up with an example as my knowledge of different logics is limited).  
> **username_1**: Maybe you should consider the other possibility for a bit then :)  
> **username_0**: As an example, validity for the Bernays-Schoenfinkel fragment of first-order logic is decidable. Let that set be called $BS$. But does that mean that $BS' = \{ \neg f | f \in BS \}$ is decidable as well? I don't quite see it.  
> **username_1**: Hmmm. The answer seems to be negative, since I suspect that the $\forall^*\exists^*$ is undecidable. A careful examination of the proof should determine this. A quick google search comes up with [this](https://logic.rwth-aachen.de/~graedel/kalmar.pdf) survey.  
> **username_1**: I might add that this suggests that the question is on-topic on this site.  

---

## 1 answers

### Answer by username_2 on 2015-03-29. Score: 3

For (propositional) [intermediate logics](http://en.wikipedia.org/wiki/Intermediate_logic), a decision procedure for satisfiability cannot generally be turned into a decision procedure for (non)validity, because all intermediate logics happen to have the same set of satisfiable formulas, namely, the set of classically satisfiable formulas, whereas some (a majority of) intermediate logics are undecidable.

(To make sense of the juxtaposition, all of the intermediate logics should be considered in the language of the weakest one, i.e., $\land$, $\lor$, $\to$, and $\neg$ or $\bot$.)

The coincidence of SAT's for these logics is a consequence of [Glivenko theorem](http://en.wikipedia.org/wiki/Double-negation_translation#Propositional_logic) (which can be paraphrased by asserting that $\neg\varphi$ is provable classically iff it is provable intuitionistically, for any formula $\varphi$). See also [this post](https://mathoverflow.net/a/139296).

> **Comments:**
> **username_1**: Any references on undecidability of the decision procedure for intermediate logics?  
> **username_2**: @username_1 I had no particular undecidability result in mind, actually. The quantification `a majority of' referred to the fact that the lattice of intermediate logics has the cardinality of the continuum, so we can't have decision procedures for all of these logics. The cardinality result for intermediate logics can be obtained by employing Jankov formulas.  
> **username_2**: @username_1 Apparently Shehtman came up with a particular example of an undecidable propositional superintuitionistic logic (in a 1978 paper), but I'm not familiar with its particulars.  
> **username_1**: It's a bit strange to give an undecidability argument by cardinality: I don't really consider something to be a logic if the axioms are not at least $\mathrm{r.e.}$! However I will gladly believe that there are undecidable intermediate logics, given how easy it is to build undecidable [propositional linear logics](http://www.csl.sri.com/users/lincoln/papers/llwork-complex.pdf).  

---

