FOM: Pratt has humor!!

[Soren Riis]

-----------------------------------------------------------------------
Pratt has humor!!
-----------------------------------------------------------------------
Vaughan Pratt wrote:

> For myself I fully support the thesis that intuitionistic logic is no less
> meaningful a logic than classical, as I hope my recent postings in this
> thread made clear (but my support could have been phrased more crisply).
>
> I also don't see intuitionistic logic as the end of the line in that
> progression.  *The* end of the line is linear logic, there is nothing
> beyond it in the same sense that, going in the other direction, there
> is nothing beyond classical logic.  Classical and linear logic are the
> endpoints in a spectrum of logics that range from the logic of pure
> separation to its dual logic of pure connection.  Intuitionistic logic
> lives within that interval, close to the classical end.

I have been staring at this in disbelief trying to make sense of it. 
Then it struck me - Pratt has humor!! This  explains everything!! 
What I read must be meant as a joke :-)

------------------------
Instead of

> Classical and linear logic are the endpoints in a spectrum of logics

one should perhaps sharpen Pratts view: 

"!Classical ?!!and !!??? ?linear !logic are ??the !?!endpoints?? 
in !a ?!spectrum of !?logics"

Do I understand Pratt right? Is Pratt's latest suggestion that
linear logic should be a part of fom? 

Concerning the statement:
> I fully support the thesis that intuitionistic logic is no less
> meaningful a logic than classical  

Perhaps you ment:

"I NOT NOT fully support the thesis that intuitionistic logic is 
NOT NOT strictly more meaningful a logic than classical" 

or was it

"NOT NOT I NOT NOT fully support the thesis that intuitionistic 
logic is NOT NOT strictly NOT NOT effectively less meaningful a 
logic than classical"

---------------------
A. Wiles Proof
---------------------
A. Wiles proof of the Tanijama-Shimura conjecture (settling FLT) begins:
"Let p be an odd prime. Let \Sigma be a finite set of primes including p 
and let Q_\Sigma be the maximal extension of Q unramified outside the set 
and infinity."

Perhaps Pratt will show us how to formalize this in Linear 
Logic. Or perhaps McLarty will show how to formalize it in Topos Theory 
(without implicit smuggling in axioms from set theory)? I now realize 
that the suggestion that Category Theory can serve as fom without building 
on set theory perhaps was another joke?
 
Carsten Butz have advocated himself sympathetic to a position of 
intuitionism from which it seems to follow that Wiles proof is incorrect 
(or perhaps I should say NOT NOT incorrect (=NOT correct)). 
If Butz (and the friend he refered to) is so certain about this why do 
they not submit a short note to Annals of Mathematics pointing out 
the flaw in Wiles reasoning. Also Wiles apparently do not realize that he 
only proved a huge disjunction of FLT (with some gigantic distribution of 
!s and ?s). Wiles failing to recognize his implicit use of another 
newly discovered illegitimate rule of inference - the contraction rule.

> *The* end of the line is linear logic, there is nothing
> beyond it in the same sense that, going in the other direction, there
> is nothing beyond classical logic.

At one end of the line we have brilliance. One the other end absolute
maximal stupidity. Pratt is right that there is nothing beyond absolute
maximal stupidity.

And this is for real as Hersh one of this lists other great humorists can 
tell:

?linear !logic and (or should I say ?!and) !linear? logic?! do indeed 
exists. 
Like Mickey Mouse, Donald Duck, and Hersh's bank account.  
A comforting view though not based on linear logic. 

-----------------
DISCLAIMER:
-----------------
** Let me make this VERY clear: I am ONLY voicing strongly loaded 
value statements against Linear Logic and Category Theory etc. as 
FOUNDATION OF MATHEMATICS. I think both areas are fundamental 
topic's. Linear logic and all the other logics can perfectly be 
described and dealt with within ZFC. In this discussion (which I 
regret I ever entered) the category fom advocates seems to make a 
confusion between the object area (linear logic, intuitionistic
logic, number theory etc), and the meta theory ZFC, (the boolean 
topos SET). 

Wiles proof can be carried out in some Toposes and not in others. I am 
lacking an clear account of which Toposes are legitimate and which 
are not. If you CLEAR AND LOUD answer "the boolean topos SET" I do 
not see a major problem and more interesting discussions can begin. 
If you however try to avoid reference to sets I see a serious 
problem. Is a Boolean Topos with a natural number object sufficient 
as fom? Certainly not. Probably not even sufficient if we want a 
direct translation of Wiles proof. Which Topos are legitimate in 
the sense they give correct answers for statements concerning the 
natural numbers? Which Topos are legitimate to use for Wiles? For 
the rest of us? Is it legitimate to iterate the power-set axiom 
uncountable many times? You cannot claim Category Theory 
is fom, until questions like these have been answered. 
You can of course copy the traditional ZFC answer, but then YOU are 
not doing fom, only coping it.

I am not an absolutist and are open for other foundations than ZFC. 
Pratt and others might call me an old-fashioned rationalist. I 
think of myself as a critical rationalist (very sympathetic to Carl 
Popper's ideals for Science and Democracy). For me relativism is 
reactionary and undemocratic. 
If we cannot resort our different views by rational means history 
have shown that FORCE and VIOLENCE is just around the corner. And 
so is absolutism and the thought police (by this is a different
issue).

Soren Riis