**Ended Competition:** What is the shortest proof of $\exists x \forall y (D(x) \to D(y)) $?

The competition has ended 6 june 2014 22:00 GMT
The winner is Bryan

Well done !

When I was rereading the proof of the drinkers paradox (see Proof of Drinker paradox I realised that $\exists x \forall y (D(x) \to D(y)) $ is also a theorem.

I managed to proof it in 21 lines (see below), but I am not sure if this is the shortest possible proof.
And I would like to know are there shorter versions?

That is the reason for this competition (see also below)

Competition rules

  • This is a small competition, I will give the person who comes with the shortest proof (shorter than the proof below ) a reward of 200 (unmarked) reputation points. ( I can only add a bounty in a couple of days from now , but you may already start to think about how to prove it, and you may allready post your answer.

  • The length of a proof is measured by the number of numbered lines in the proof (see the proof below as example, the first formula is at line number 2, and end proof lines are not counted)

  • If there is more than one person with the shortest answer the reward goes to the first poster. (measured with the last substantional edit of the proof)

  • The answer must be in the form of a complete Fitch-style natural deduction style
    typed in a answer box as below. proofs formatted in $\LaTeX$ is even better, but I just don’t know how to do that.

  • The proofsystem is the Fitch style natural deduction system as described in “Language proof and Logic” by Barwise cs, ( LPL, http://ggweb.stanford.edu/lpl/ ) except that the General Conditional proof rule is not allowed. (I just don’t like the rule, not sure if using this rule would shorten the proof either)

  • Maybe I will also give an extra prize for the most beautiful answer, or the shortest proof in another style/ method of natural deduction. it depends a bit on the answers I get, others may also set and give bounties as they see fit.

  • you may give more than one answer, answers in more than one proof method ect, but do post them as seperate answers, and be aware that only the proof that uses the fitch method described above is competing, and other participants can peek at your answers.

    • GOOD LUCK, and may the best one win.

Proof system:

For participants that don’t have the LPL book the only allowed inference rules are the rules I used in the proof:

  • the $\bot$ (falsum , contradiction) introduction and elimination rules
  • the $\lnot \lnot$ elimination rules
  • the $\lnot $ , $\to$ , $\exists$ and $\forall$ introduction rules

(also see the proof below for examples of how to use them.)

Also the following rules are allowable :

  • the $\land$ , $\lor$ and $\leftrightarrow$ introduction and elimination rules.
  • the $\to$ , $\exists$ and $\forall$ elimination rules
  • the reiteration rule.

(This is just to be complete, I don’t think they are useful in this proof)


  • line 1 is empty (in the Fitch software that accompanies the book line 1 is for premisses only and there are no premisses in this proof)

  • the end subproof lines have no line number. (and they don’t count in the all important the number of lines)

  • the General Conditional proof rule is not allowed

  • there is no $\lnot$ elimination rule (only an double negation elimination rule)

My proof: (and example on how to use the rules, and how your answer should be formatted)

1  |
.  |----------------- 
2  | |____________  ~Ex Vy (D(x) -> D(y))    New Subproof for ~ Introduction
3  | | |_________a                           variable for Universal Introduction
4  | | | |________  D(b)                     New Subproof for -> Introduction
5  | | | | |______  ~D(a)                    New Subproof for ~ Introduction 
6  | | | | | |___c                           variable for Universal Introduction
7  | | | | | | |__  D(a)                     New Subproof for -> Introduction
8  | | | | | | |    _|_                      5,7 _|_ introduction
9  | | | | | | |    D(c)                     8   _|_ Elimination
.. | | | | | | <-------------------------   end subproof
10 | | | | | |      D(a) -> D(c)             7-9 -> Introduction
.. | | | | | <---------------------------   end subproof
11 | | | | |        Vy(D(a) -> D(y))         6-10 Universal Introduction
12 | | | | |        Ex Vy (D(x) -> D(y))     11 Existentional Introduction 
13 | | | | |        _|_                      2,12 _|_ introduction
.. | | | | <-----------------------------   end subproof
14 | | | |          ~~D(a)                   5-13 ~ introduction
15 | | | |          D(a)                     14 ~~ Elimination
.. | | | <-------------------------------   end subproof   
16 | | |            D(b) -> D(a)             4-15 -> Introduction
.. | | <---------------------------------   end subproof   
17 | |              Vy(D(b) -> D(y))         3-16 Universal Introduction
18 | |              ExVy(D(x) -> D(y))       17 Existentional Introduction
19 | |              _|_                      2,18 _|_ introduction
.. | <-----------------------------------   end subproof
20 |                ~~Ex Vy (D(x) -> D(y))   2-19 ~ introduction
21 |                Ex Vy (D(x) -> D(y))     20 ~~ Elimination

Allowable Question and other meta stuff

I did ask on http://meta.math.stackexchange.com/questions/13855/are-small-competitions-allowed if this is an allowable question, I was not given an answer yet (28 may 2014) that such questions were not allowable, outside the scope of this forum or any other negative remark, I did not get any comment that this was an improper question, or under which circumstances such competitions are allowed.

(the most negative comment was that it should be unmarked reputation points. 🙂 and that comment was later removed…

If you disagree with this please add that as answer to the question on at the meta math stackexchange site. (or vote such an answer up)

If on the other hand you do like competitions, also show your support on the meta site, ( by adding it as answer, or voting such an answer up)

PS don’t think all logic is all simple , I will make a shorter proof in no time, the question is rather hard and difficult, but proof that I am wrong 🙂

Solutions Collecting From Web of "**Ended Competition:** What is the shortest proof of $\exists x \forall y (D(x) \to D(y)) $?"

Well, here’s my solution even though I’ve used 4 ‘unallowed’ rules.

  1. $\neg\exists x\forall y(Dx\implies Dy)\quad$ assumption for $\neg$ introduction
  2. $\forall x\neg\forall y(Dx\implies Dy)\quad$ DeMorgan’s for quantifiers
  3. $\forall x\exists y \neg(Dx\implies Dy)\quad$ DeMorgan’s for quantifiers
  4. $\forall x\exists y\neg(\neg Dx\vee Dy)\quad$ Conditional exchange
  5. $\forall x\exists y(\neg\neg Dx\wedge \neg Dy)\quad$ DeMorgan’s
  6. $\forall x \exists y(Dx\wedge\neg Dy)\quad$ Double negation
  7. $\exists y(Da\wedge\neg Dy)\quad$ Universal instantiation
  8. $Da\wedge \neg Db\quad$ Existential instantiation (flag $b$)
  9. $\neg Db\quad$ Simplification
  10. $\exists y(Db\wedge \neg Dy)\quad$ Universal instantiation
  11. $Db\wedge \neg Dc\quad$ Existential instantiation (flag $c$)
  12. $Db\quad$ Simplification
  13. $\bot\quad$ Contradiction 9, 12
  14. $\neg\neg\exists x\forall y(Dx\implies Dy)\quad$ Proof by contradiction 1-13
  15. $\exists x\forall y(Dx\implies Dy)\quad$ Double negation

I guess there are 16 lines in all if we include the empty premise line. I do have a couple comments though.

First, I highly doubt this proof can be attained by the last applied rule being Existential Generalization. This statement is a logical truth precisely because we can change our $x$ depending on whether the domain has or has not a member such that $Dx$ holds. If $D$ holds for all members of the domain, any choice of $x$ will make the statement true. If $D$ does not hold for some member of the domain, choosing that as our $x$ will make the statement true. Saying that we can reach the conclusion by one final use of E.G. means that the member $b$ which appears in the precedent somehow handled both cases while the only thing we are supposed to know about $b$ is that it is a member of the domain. We still don’t know anything of the domain.

With that said, after I got a copy of your book and read the rules, it appears the only way we can get to the conclusion is by an application of double negation. And the only way to get there is a proof by contradiction. Thus I believe your lines 1, 2, 19, 20, and 21 belong to the minimal solution. So far, I haven’t found anything simpler for the middle.

Although outside the scope of what is asked, it is perhaps amusing to note that a proof in a tableau system is markedly shorter, and writes itself (without even having to split the tree and consider cases):

$$\neg\exists x\forall y(Dx\implies Dy)$$
$$\forall x\neg\forall y(Dx\implies Dy)$$
$$\neg\forall y(Da\implies Dy)$$
$$\exists y\neg(Da\implies Dy)$$
$$\neg(Da\implies Db)$$
$$\neg Db$$
$$\neg\forall y(Db\implies Dy)$$
$$\exists y\neg(Db\implies Dy)$$
$$\neg(Db\implies Dc)$$

This isn’t quite an answer, since it’s about the Drinker’s paradox, and not the slightly different version here, but it may help for developing a shorter proof of the variant here. The line count might not be acceptable though, because it uses Taut Con, but only to get $A$ and $\lnot B$ from $\lnot (A \to B)$, not for any quantifier exchange or anything like that. The accepted answer uses some DeMorgan’s with quantifers though, so I think this might be within bounds.

Using the Fitch software that’s distributed with the LPL book, you can get the Drinker’s Paradox down to 14 lines, because of the way that $\forall$-introduction is allowed to cite any intermediate result in the proof, not just the last one.

Note: The image says “bird” because when I first heard this, it was phrased as “there’s something such that if it’s a bird, then everything is a bird.” I made this proof back in 2009 and don’t have access to the original files anymore, so sorry about the image quality.

enter image description here

Maybe this can help shorten a proof of the variant.

Using my trusty Hokus Ponens Lemma:

enter image description here

I like this one (The FO Con is applying some basic equivalences, not unlike the beginning of Bryan’s proof):

enter image description here

OK, enough fun. I really don’t think Willemien’s proof can be shortened if we stick to the rules. Here is Willemien’s proof in Fitch:

enter image description here

Using equivalences:

$\top \equiv \forall y D(y) \rightarrow \forall y D(y) \equiv \forall x D(x) \rightarrow \forall y D(y) \equiv \exists x (D(x) \rightarrow \forall y D(y)) \equiv \exists x \forall y (D(x) \rightarrow D(y)) $