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)
Notice:
-
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 🙂
Best Answer
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.