[FOM] Fwd: Re: Reflections on Vienna Meeti
Jaap van Oosten
J.vanOosten at uu.nl
Wed May 18 09:35:49 EDT 2011
I would like to endorse Juliette's call for some moderation in this
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,
> FOM mailing list
> FOM at cs.nyu.edu
More information about the FOM