# [FOM] Computing roots of a polynomial

Vaughan Pratt pratt at cs.stanford.edu
Mon May 25 21:10:40 EDT 2009


On 5/25/2009 2:12 PM, Andrej Bauer wrote:
> [...] Here are some basic observations. Intuitionistically (and therefore
> classicaly) it follows from the definition of Turing machines that:
>
> T stops =>  not (T block) and not (T diverges) =>  not not (T stops)
> T blocks =>  not (T stops) and not (T diverges) =>  not not (T blocks)
> T diverges<=>  not (T stops or T blocks)

Ah, excellent.  This is the Rosetta stone I was missing when trying to
imagine how intuitionists think intuitively, which I was having trouble
doing despite familiarity with Heyting algebras.  (Those of us who write
software and build hardware in the US tend to get into the rut of
classical reasoning.)

To make the point that very little about Turing machines is involved
here, in the spirit of Hilbert's chairs, tables, and beer steins,
reinterpret S, B, and D as Slingshot, Boomerang, and Disarmed, in the
context of a crowded train, with perhaps even uncountably many
passengers.  Take S to mean s1 v s2 v ..., that is, someone has a
slingshot, with s3 asserting that passenger 3 has the slingshot.
Likewise take B to mean b1 v b2 v ..., someone has a boomerang. (For a
Turing machine T, reinterpret s3 as the proposition that T stops at step
3, b5 that T blocks at step 5, etc.)

The train cannot proceed from the station until Inspector Poirot has
pronounced the whole train Disarmed, meaning that no passenger has
either a slingshot or a boomerang (your third line, the equivalence).
The train is equipped with sensors that will trigger if two or more
banned items are on board, but to avoid false positives it does not
trigger on one, whence the need for the inspector, who is only called in
when the sensors detect nothing amiss.

Now for any element a of a Heyting algebra (in particular a = 0 when
defining intuitionistic negation), the unary operations \lambda x.(x -->
a) and \lambda x.(x & a) are adjoints.  The former therefore distributes
over arbitrary disjunctions, namely as (s1 v s2 v ...) --> a  =  (s1 -->
a) & (s2 --> a) & ...  We can therefore express not-S, meaning no one
has a slingshot, either as ~(s1 v s2 v ...) or as ~s1 & ~s2 & ...,

> "not exists, phi" is intuitionistically equivalent to "forall, not phi",

Likewise for ~B = ~(b1 v b2 v ...) = ~b1 & ~b2 & ...

Now if anyone has a slingshot, we know that no one has a boomerang (or
the sensors would have gone off) and the train is not disarmed (by
definition).  Furthermore if somehow it is determined that no one has a
boomerang, yet after Poirot's inspection he announces that the train is
not disarmed, someone must have a slingshot.  But until Poirot actually
produces the slingshot owner to witness the truth of S we cannot be sure
of this ourselves, though to assume otherwise would mean that we didn't
believe Poirot, an absurdity.  We conclude not not S, namely that surely
there is a slingshot since Poirot said that the train was not disarmed
yet we know for certain that there is no boomerang.

The symmetry of slingshots and boomerangs leads to the corresponding
conclusion in the case someone has a boomerang.  If no one has a
slingshot yet the train is not disarmed according to Poirot, surely
someone has a boomerang.

This accounts fully for your three lines.  Now I just have to retain
this scenario.  I travel enough that this should not be difficult: the
intuitionistic logic of modern travel will be reinforced by my every
trip, worrying about these possibilities.  Perhaps TSA agents can be
taught intuitionistic logic in this way.

>
> Well, one just has to be careful about how to say things
> intuitionistically. For example, assuming that the set
>
>    {0 | T stops} union {1 | T blocks} union {2 | T diverges}
>
> has a size measured as a natural number entails "T stops or T blocks
> or T diverges".

(I presume you meant "nonzero natural number," or did you intend the
definition of "diverges" to rule out that possibility?)

Thanks for clearing this up for me!

Vaughan