[FOM] Computing roots of a polynomial

[Vaughan Pratt]

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 & ..., 
corresponding to your point,

> "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