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)
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.
For participants that don’t have the LPL book the only allowed inference rules are the rules I used in the proof:
(also see the proof below for examples of how to use them.)
Also the following rules are allowable :
(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
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 🙂
Well, here’s my solution even though I’ve used 4 ‘unallowed’ rules.
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\forall y(Db\implies Dy)$$
$$\exists y\neg(Db\implies Dy)$$
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.
Maybe this can help shorten a proof of the variant.
Using my trusty Hokus Ponens Lemma:
I like this one (The FO Con is applying some basic equivalences, not unlike the beginning of Bryan’s proof):
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:
$\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)) $