Monday, 12 August 2013

101 Dalmatians

Here is an example of applied mathematical reasoning, similar to a couple of examples in a paper "Some More Curious Inferences" (Analysis, 2005), about the phenomenon (discovered by Gödel 1936) of proof speed-up. It's a modification of the kind of arithmetic examples given in the work of Putnam and Field (Science Without Numbers, 1980).
(1) There are exactly 100 food bowls
(2) There are exactly 101 dalmatians
(3) For each dalmatian $d$, there is exactly one food bowl $b$ that $d$ uses.
--------------------------------------
(C) So, there least two dalmatians $d_1, d_2$ that use the same food bowl.
To apply mathematics, we apply Comprehension and Hume's Principle, which allow us to reformulate the premises (1)-(3) and conclusion (C), referring to two mixed sets, $B$ and $D$ and one mixed function $u$:
(1)* $|B| = 100$
(2)* $|D| = 101$
(3)* $u : D \to B$.
--------------------------------------
(C)* So, there are $d_1, d_2 \in D$, with $d_1 \neq d_2$ such that $u(d_1) = u(d_2)$.
To show that this is correct, note first that $100 < 101$. So, $|B| < |D|$. Next, note that the Pigeonhole Principle implies that if $u : D \to B$ and $|B| < |D|$, then $u$ is not injective. So, $u$ is not injective. So, there are distinct $d_1, d_2 \in D$ such that $u(d_1) = u(d_2)$. This is the required conclusion (C)*, which takes us back to (C).

2 comments:

  1. Hi Jeff, this is nice. A couple of observations, I'd be curious to know what you think:

    1. The argument is valid even if u is not a function. You can weaken the third premise to say that each Dalmatian uses a food bowl, and it is still true that there must be distinct Dalmatians using the same bowl.

    2. For fixed |B| and |D| the argument does not require anything as strong as PHP, or FOL for that matter. It can be carried out in propositional logic, by writing down 101 premises, each one one of which is a disjunction of 100 atoms Uxy (intuitively saying that Dalmatian x uses bowl y). It will validly follow that two Dalmatians use the same bowl (this will also be some very long disjunction). The proof will then be ginormous, but it will not employ any high-power mathematics.

    3. For variable |B| and |D|, then you do need some mathematical machinery. PHP is, in fact, equivalent to the principle of induction (over some weak theory, although as far as I can tell it still requires some weak form of comprehension). So you already have full PA, for all practical purposes. But this does not seem to invalidate any of your arguments, does it?

    ReplyDelete
  2. Hi Aldo, many thanks.

    On points 2 & 3, yes, right - that's more or less the point of the 2005 paper, "Some More Curious Inferences", that I linked to. That is, the "101 Dalmatians Inference" is valid in logic alone; but the length of proof is fairly horrible: if I recall right, my calculation was that the proof length in symbols goes like $O(n^3 log n)$ (the $log n$ comes from variable subscripts being coded in binary) for a tableau; so, the purely logical proof would fill a 200 page book! But, ascending, using Comprehension, HP, and PHP, we get a much quicker proof, and then instantiate with decimal numerals. We might even say that PHP *explains* why the 101 Dalmatians Inference is valid ... (that is, we invert logicism: we use mathematics to explain certain validities)

    The paper was influenced by an earlier 1987 paper "A Curious Inference" by Boolos. At the end of the paper, I asked how the nominalist would justify this reasoning. I planned to follow up the paper with a longer one on speed-up, but didn't bother in the end. But Richard Pettigrew has written a very nice and interesting reply,

    "Indispensability Arguments and Instrumental Nominalism" (RSL 2011)

    http://eis.bris.ac.uk/~rp3959/papers/nomadequacy.pdf

    Yes, I agree on point 1 - it just makes the example a bit more vivid and easier to apply PHP.

    I use this example in teaching, along with "There are 20 people here, but I've only made 14 handouts, so a few of you have to share".

    Cheers,

    Jeff

    ReplyDelete