4
$\begingroup$

See moderator's note in the comments.

I just came across the following. In intuitionistic logic
and classical logic we have the following consequences:

∃x¬φ → ¬∀xφ  
∀x¬φ → ¬∃xφ  
¬∃xφ → ∀x¬φ

But the following consequence is only generally valid
in classical logic but not in intuitionistic logic:

¬∀xφ → ∃x¬φ                         (Q)

Are there intermediate logics where the last consequence
doesn't fail? I mean a logic where φ v ¬φ doesn't hold
in general but (Q) does.

Bye

| cite | |
$\endgroup$
  • $\begingroup$ What kind of logics? Obviously, you can just take intuitionistic logic with (Q) as an extra axiom. $\endgroup$ – Emil Jeřábek Jun 18 '15 at 14:47
  • $\begingroup$ Because, as I already wrote below, the resulting system is conservative over intuitionistic propositional logic: deleting all quantifiers and variables from a proof and turning all predicates into propositional variables results in a valid propositional proof, and specifically, translates (Q) to a tautology $\neg\phi'\to\neg\phi'$. (In other words, (Q) holds in Kripke models with 1-element object domains.) $\endgroup$ – Emil Jeřábek Jun 18 '15 at 18:05
  • 1
    $\begingroup$ I have rolled back the last edit. The original question was fine and two users have provided useful information. $\endgroup$ – Todd Trimble Jun 19 '15 at 0:58
  • $\begingroup$ @ToddTrimble I made an error in the original question. I don't want to know whether there is a logic which entails (Q). Its clear that when I add (Q) that it entails (Q). I want to know whether there is an (X), such that (X)+(Q) entails (LEM). If I change the question now all the answers are wrong anyway. So it needs to be deleted. $\endgroup$ – Mostowski Collapse Jun 19 '15 at 1:03
  • $\begingroup$ @ToddTrimble My question is inspired by publish.uwo.ca/~jbell/Epsilon.pdf There fore example the author shows that (X)=(Epsilon) does not entail (LEM). But actually I didn't expect to get answers so quickly. But for example Henry Towsner is only a literature reference. So basically there is only the answer of Andreas Blass which is not relevant to what I need to know, since he doesn't use (Q), something else. $\endgroup$ – Mostowski Collapse Jun 19 '15 at 1:05
8
$\begingroup$

As Emil pointed out in a comment, the answer to this question will depend on what else is available in your intuitionistic logic. If that background logic is strong enough, then (Q) will imply the law of the excluded middle. Specifically, suppose we're working in a higher-order intuitionistic logic (also called intuitionistic type theory) such as arises as the internal logic of topoi, and suppose we adjoin (Q) as a general principle, i.e., with arbitrary formulas $\phi$ and with the variable $x$ ranging over an arbitrary type. Then we get classical logic, in the form $(\neg\neg\alpha)\to\alpha$ (which is known to imply the law of the excluded middle) as follows.

Given $\alpha$, let $A=\{x\in1:\alpha\}$. That is, $A$ is the subset of the singleton 1 that contains the unique element of 1 iff $\alpha$ is true. Then, for any formula $\phi$, we have that $(\exists x\in A)\,\phi$ is equivalent to $\alpha\land\phi$ and that $(\forall x\in A)\,\phi$ is equivalent to $\alpha\to\phi$. In particular, if we apply (Q) with $\bot$ (the always false proposition) in the role of $\phi$ and with the quantifiers ranging over $A$, then the left side of (Q) is equivalent to $\neg(\alpha\to\bot)$ and thus to $\neg\neg\alpha$, while the right side of $Q$ becomes equivalent to $\alpha\land\neg\bot$ and thus to $\alpha$. So this particular instantiation of (Q) says $(\neg\neg\alpha)\to\alpha$.

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ This is interesting. However, what I actually wanted to point out was the opposite: if we adjoin (Q) as a schema to ordinary first-order intuitionistic logic, it does not prove the law of excluded middle, and in fact it’s a conservative extension of intuitionistic propositional logic (as can be seen by striking out all quantifiers). $\endgroup$ – Emil Jeřábek Jun 18 '15 at 16:07
  • 1
    $\begingroup$ Though your argument does not actually use higher-order logic: it only needs closure under quantifier relativization. $\endgroup$ – Emil Jeřábek Jun 18 '15 at 16:10
  • 3
    $\begingroup$ I don't think it's wise to delete everything here. Even if it's not what you wanted, your question, Emil's comment, and my answer may be of interest or even of use to others. So I would prefer that these things remain on the site, perhaps with an addition to the question saying that it's not really what you wanted. If you start over, then that should be posted as a new question, perhaps with links to and from this one. $\endgroup$ – Andreas Blass Jun 19 '15 at 2:17
  • 2
    $\begingroup$ It’s actually not derivable from (Q) (there is a simple finite counter-model), but that’s besides the point, as $\neg(a=b)$ is not a propositional formula. I didn’t mention equality in the translation, but it is supposed to translate to $\top$ (which should be obvious from the semantic interpretation of the translation). See also begthequestion.info . $\endgroup$ – Emil Jeřábek Jun 20 '15 at 14:56
  • 2
    $\begingroup$ Bell additionally assumes $\forall x\,(x=a\lor x\ne a)$, which you omitted. For all I know, his paper is correct. The model looks as follows. The underlying Kripke frame is a tree with a root and two leaves. The first-order domains in all three worlds are $\{a,b,c,d\}$; one leaf satisfies $a=c$ and $b=d$, and the other leaf satisfies $a=d$ and $b=c$. One leaf satisfies $p$. After unwinding the definitions, the validity of (Q) in the model boils down to the property that each equivalence class in one leaf intersects each equivalence class in the other leaf. $\endgroup$ – Emil Jeřábek Jun 20 '15 at 16:16
4
$\begingroup$

I'm not sure if there's a system short of classical logic where (Q) holds for all formulas, however the principle $$\forall x(\phi\vee\neg\phi)\rightarrow(\neg \forall x\neg\phi\rightarrow\exists x\phi)$$ (or sometimes $$\forall x(\phi\vee\neg\phi)\rightarrow(\neg \neg\exists x\phi\rightarrow\exists x\phi)$$ instead) is Markov's principle, and there's a great deal of work on constructive logics with Markov's principle.

| cite | improve this answer | |
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.