In his article “Present State of Research into the Foundations of Mathematics,” Gentzen briefly talks about Goedel’s incompleteness results. He says that it is not an alarming result because it says “that for number theory no adequate system of forms of inference can be specified once and for all, but that, on the contrary, new theorems can always be found whose proof requires new forms of inference.” This is interesting because Gentzen worked with Hilbert on his proof-theoretic projects and created two of the three main proof-theoretic frameworks, natural deduction and the sequent calculus. The incompleteness theorems are often taken as stating a sort of limit on proof-theoretic means. (I’m treading on shaky ground here, so correct me if my story goes astray.) That is to say, any sufficiently strong proof system will be unable to prove certain consequences of its axioms and rules. Adding more rules in an attempt to fix it can result in being able to prove some of the old unprovable statements, but new ones (maybe just more?) statements will arise.

Gentzen’s reaction to this is to shrug his philosophical shoulders. There may be consequences that we can’t capture using our current forms of inference, but that just means we need new forms of inference. To these we will need to add further forms of inference. And so on.

I thought this was, by itself, an interesting position whose foundational worth I haven’t figured out. But, in reading Logical Syntax of Language, I found some things that surprised me. First, Carnap read Gentzen. He cites the consistency of arithmetic article. I had thought that Gentzen was mostly unknown or ignored in Europe sort of like Frege. This doesn’t dispel that possibility though. The other thing was that Carnap has a similar reaction to Goedel’s incompleteness theorems. At least, he has a similar reaction to their consequences for his work. He says, “[E]verything mathematical can be formalized, but mathematics cannot be exhausted by one system; it requires an infinite series of ever richer languages.” (LSL 60d)

The parallel with Gentzen should be clear. The reaction seems to come from a common philosophical position with respect to mathematics. I’d like to call that an inferentialist one, although I’m a little hesitant. I’m unclear what Carnap’s views about inference are exactly, but it seems like it may be apt. It will depend on whether the inference forms are part of the richer language for Carnap. If that turns out not to work, the common thread might be the syntactic orientation of the two logicians. I think they have different philosophical views about syntax though, so that might not be entirely happy either. I’m not familiar enough with Gentzen to say how Carnap’s view of syntax’s role in science would strike him. In Carnap there doesn’t seem to be the talk of defining the logical constants syntactically or inferentially in the way that is alluded to in Gentzen’s papers. Still, it seems like the right sort of response from a certain orientation, one I want to call inferentialist. What Goedel’s results show is that the inferentialist can’t be satisfied with a static or final system for mathematics. An interesting question would be whether the same sort of “dynamic” would carry over to the non-mathematical. I have no clue if there is a lesson for inferentialist semantics generally lying in there.

A separate question is whether the above view is satisfactory as a foundational position. One reason to think that it isn’t is that there seems to be some slack between an inferential system at any one time and the consequences of the axioms. The latter is always outrunning the former which tries to play catch-up. One might want their foundational position to explain what is going on with the latter, or at least the slack between the two. Although, that might stack the deck in favor of classical logic against something like intuitionism or constructivist positions.

Advertisements