[PRL] Bob Harper's new blog

[will at ccs.neu.edu]

Dave Herman wrote:
> I'm sorry, somebody has to say this. You might as well
> have just crypto-hashed your message and sent that instead.
> Your argument is completely opaque to me, and I'd wager, to
> the whole PRL.
> 
> David's point about heated assertions without evidence is germane.
> Maybe you're trying to let the irony of refuting a blog post about
> the difference between booleans and propositions by asserting its
> falsehood without proof somehow be the proof itself, but I'm afraid
> even after 8 (count 'em) years of studying PL theory, my brain
> doesn't go that meta.
> 
> So for us mortals... care to explain?

Harper's essays are at
http://existentialtype.wordpress.com/2011/03/

The essay in question is "Boolean Blindness".  The first sentence of
its sixth paragraph is

    In classical mathematics, where computability is not a concern,
    it is possible to conflate the notions of Booleans and propositions,
    so that there are only two propositions in the world, true and false.

That's flat-out wrong.  There are only two truth values in the domain of
Booleans, but classical mathematics would be completely trivial if there
were only two propositions.  Classical mathematics is far more complex
than propositional logic, but it includes propositional logic as a tiny
subset, and Harper's statement isn't even true of propositional logic.

That's easy to see.  In propositional logic, there's a countable infinity
of atomic propositions, but we usually deal with only a finite subset of
them at any one time.  Let Prop be the set of atomic propositions that
are mentioned by some compound proposition P.  The meaning of P is a
function in the domain

    D = (Prop -> {true, false}) -> {true, false}

There are 2^(2^n) functions in D, where n is the cardinality of D.  So
long as there is at least one atomic proposition A in the world, we can
use A to construct four propositions whose meanings are clearly distinct:

    A & not A
    A
    not A
    A or not A

According to Harper, there are only two propositions in the world, so
Harper is saying that at least two of the four propositions above are
not only equivalent, but identical.  Yet all four propositions have
distinct meanings, so they can't be identical.  Hence Harper's claim
is rubbish, even for propositional logic.

Will


every single one of those functions is a possible meaning for P.  There
are only two values in B = {true, false}.