[FOM] Predicativity and parametric polymorphism of Brouwerian implication

[WILLIAM TAIT]

Dear Mark,

I could not obtain the paper from the address you provided, even after going through the dance of opening an account, etc. It should be easier to obtain a paper than that.

Although I haven’t read the paper, let me make a remark about the subject. I did not think that the historical problem about implication concerned impredicativity. Rather it was this: the constructive meaning of (A \implies B) according to Heyting was that we have at hand a means of transforming any proof of A into a proof of B. But this does not tell us what a proof of A \implies B is and so, in particular, fails to explain the meaning of (A \implies B) \implies C).  This conclusion is explicit in the original (unpublished) consistency proof of Gentzen and it can be avoided only by admitting as proofs higher order objects, such as an operation that transforms a proof of A into a proof of B. But Gentzen's conception of finitism seems to have been closed to this idea. G\"odel also seems to have believed that intuitionism was restricted to the lowest order and so also felt that  implication was a serious problem for intuitionistic logic. (See the Lecture at Zilsel’s.) 

We can be thankful for this, since otherwise the double-negation interpretation of PA would have satisfied both Gentzen and G\”odel and we would not have had \epsilon_0 on Gentzen’s part nor the Dialectica interpretation (nor maybe the subject of provability logic) on G\”odel’s.

Bill Tait



> On Oct 20, 2017, at 6:39 AM, Mark van Atten <vanattenmark at gmail.com> wrote:
> 
> A preprint of this paper is now available at
> https://halshs.archives-ouvertes.fr/halshs-01619110
> 
> Abstract:
> 
> A common objection to the definition of intuitionistic implication in
> the Proof Interpretation is that it is impredicative. I discuss the
> history of that objection, argue that in Brouwer's writings
> predicativity of implication is ensured through parametric
> polymorphism of functions on species, and compare this construal with
> the alternative approaches to predicative implication of Goodman,
> Dummett, Prawitz, and Martin-Löf.
> 
> Best wishes,
> Mark.
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom