Hi Vaughan, On 5 Mar 2008, at 09:11, Vaughan Pratt wrote:
My feeling about these recommended Brouwerian modes of thoughts is that they are something like locker room accounts of social and other conquests: great stories about things that never actually happened, but which with sufficient repetition convince one that they must surely have occurred.
The self-evident is merely an hypothesis that is so convenient, and that has been assumed for so long, that we can no longer imagine it false. This is just as true for Excluded Middle itself as for its negation. I happen to find Excluded Middle more convenient than its negation, but that's just me and perhaps others have had the opposite experience.
Indeed, being a computer scientist the BHK interpretation (see wikipedia) of logical connectives (which I can implement on a finite machine) makes more sense to me than the idea of infinite truth tables. You seem to think that the only alternative to excluded middle (forall P:Prop. P \/ not P) is (exists P:Prop. not (P \/ not P))? However, I'd say that "forall n:Nat. Halt n \/ not Halt n" is clearly invalid in the BHK interpretation without claiming that there is a particular statement which will never be decided, or a Turing machine which can be never shown to be terminating or not, i.e. even if we accepts Church's thesis, we arrive at "not (forall n:Nat. Halt n \/ not Halt n)" but not "exists n:Nat.not (Halt n \/ not Halt n)". To summarize, your reasoning seems to already presupposes that we accept Excluded Middle.
Then there are those who accept neither Excluded Middle nor its negation, which takes us into the Hall of Mirrors that I always find myself in when I go down this particular rabbit-hole.
Maybe this is related to my reply? Thorsten This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.