[FOM] Frank Quinn article in January Notices

[Vaughan Pratt]

On 12/27/2011 7:44 AM, Timothy Y. Chow wrote:
> By "excluded-middle reasoning," I think Quinn does*not*  mean
>
>    the principle that if we know that "not P" is false, then we know
>    that "P" is true
>
> but rather
>
>    the principle that we cannot know that "P" is true unless we can
>    prove that "not P" cannot be true.

How can the latter principle constitute "excluded-middle reasoning?"

In the three-valued logic F < M < T (false, middle, true), with 
respective negations T, F, F, the first principle fails when P is 
middle.  However the second succeeds because if we know that P is true 
then we can prove that not-P is false and therefore cannot be true.

(This is of course the smallest non-Boolean Heyting algebra.)

Phrasing the two principles as respectively ~~P --> P and P --> ~~P, we 
can recognize both as intuitionistic but only the former as Boolean.

(I like to pronounce "~~" as "surely.")

Did you have a different phrasing in mind?  Or perhaps a different 
principle?

Vaughan Pratt