[FOM] Fwd: Re: Reflections on Vienna Meeti

[Jaap van Oosten]

I would like to endorse Juliette's call for some moderation in this 
discussion.
I am personally excited by the fact that Voevodsky takes an active 
interest in Foundations,
and I am curious to see what will develop.

Although I have trouble taking the view that PA might be inconsistent 
seriously (and actually, doubt very much that it was put forward in dead 
earnestness), here is a thought that has not yet appeared in the discussion.

There are two ways in which one can consider PA to be inconsistent:
1. From the axioms of PA and the axioms/rules in first order logic, one 
can derive a contradiction
2. PA has no models

Note, that for the straight intuitionist, these two are NOT equivalent.
In the first case, as has been remarked before, we have the same for HA, 
type theory, Coq and various other programming languages. Note also that 
Godel's theorem has become meaningless, so there is no point in invoking it.

However regarding the second case, I believe that intuitionistic set 
theory IZF does not prove that PA has a model. My argument would be that 
otherwise, there would be a model of PA in the Friedman-McCarthy 
realizability interpretation of IZF, hence a recursive realizability 
model of PA. I don't think this is possible: it would lead to 
decidability of the Halting Problem.

Best wishes to all, Jaap van Oosten

by way of Martin Davis <martin at eipye.com> wrote:
> Having posted the link, I feel some responsibility for weighing in on
> the Voevodsky lecture.
>
> I am not really in a position to evaluate this work, being more
> interested in the set theory side of things. But judging from a brief
> look at some of the papers and lectures on Voevodsky's homotopy
> interpretation of type theory, it looks both very interesting and very
> sound. That Voevodsky's coworkers in Univalent Foundations are Awodey
> and Coquand seals the deal for me.
>
> So perhaps logicians should be more charitable about some of the
> imprecision in the lecture on inconsistency.
>
> All the best,
>
> Juliette
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom