[FOM] Eradicating Evil?

[Joseph Shipman]

Steve,

I'm sorry to see you go, but I'm even sorrier to see you dismiss my contributions to the discussion as having "no informational value". My previous posts, especially the last long one, frame questions in a cordial manner and do not pose extremely difficult "challenges".

Harvey is being provocative, but the core dispute is quite plain to state: whether HoTT is 
1) A better foundation than ZFC for an active and valuable area of mathematics, because it is easier to work with and easier to mechanically formalize
2) A better foundation than ZFC for mathematics in general 
3) No better than ZFC because it can be modeled within ZFC foundations in a straightforward way, so that a metatheorem can be established which assures that anything HoTT theorists do is also formalizable in ZFC, thus enabling HoTT researchers and set theorists to ignore each other from now on.

I am reacting to what I perceive is the unnecessarily strong claim (2) by asking HoTT researchers a simple question about very standard theorems of "ordinary mathematics", and I am also trying to distinguish between the weaker claim (1) and Harvey's deflationary claim (3) by asking either for HoTT theorists to give an argument that what they do can't be modeled easily in ZFC, or for set theorists to show that it can be so modeled.

-- JS

Sent from my iPhone

> On Oct 28, 2014, at 9:28 AM, Steve Awodey <awodey at cmu.edu> wrote:
> 
>> On Oct 27, 2014, at 6:01 AM, Harvey Friedman <hmflogic at gmail.com> wrote:
>> 
>> My back channels tell me that there is a crusade to "eradicate evil"
>> spearheaded by the HoTT community.
> 
> Dear Harvey (and FOM),
> 
> This is absolute rubbish and a good example of what is wrong with FOM.
> It is impossible to have a civil discussion here about anything *new* in foundations 
> without being accused of being a “crazy”, “radical”, “zealot”, etc.
> 
> Why does everything on this list have to be a fight?
> I’m tired of the gauntlets, challenges, accusations, personal attacks, etc., 
> especially the ones beginning “without knowing anything about X, here is what I think about X …”.
> 
> Those who are honestly interested in learning about Homotopy Type Theory 
> — and I recommend it to readers of this list as a new area of foundational research 
> with many interesting connections to mathematics, logic, and computer science — 
> should have no trouble finding resources online, particularly the already cited:
> 
>    www.homotopytypetheory.org
> 
> and the book available there.  
> The current discussion, by contract, has no informational value, and shows no signs of heading in that direction.
> 
> After many years on this list, I have finally had enough.  
> When you have finally succeeded in driving out everyone with a different point of view, 
> then you will be free to vilify them without rebuttal.
> 
> Good bye, and good luck with this forum,
> 
> Steve Awodey
> Professor of Philosophy and Mathematical Sciences
> Carnegie Mellon Unviersity
> 
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom