[FOM] Short technical questions about meaninfulness, truth, and induction

[Andre.Rodin at ens.fr]

> Precisely! This was my analysis too. Indeed, this theorem of Godel
> that Voevodsky, Rodin and others
> use so happily, and  without any reservation, is at least  \Pi_3 in nature.
> Hence anyone who takes it as true (and so, presumably, meaningful)
> admits that at least  \Pi_3 claims are perfectly meaningful
> and so (presumably) the induction principle is valid for them.
> Of course some people may now maintain that they doubt induction
> even for meaningful statements.

In your argument you straightforwardly identify an (informal) mathematical proof
(like that given by Godel) with a formal analysis of this proof (I mean the
analysis according to which Godel's proof at least  \Pi_3 in nature). Your way
of putting this suggests that you assume that this formal analysis reveals the
"nature" of a given informal mathematical proof. Notice that this is your
epistemic assumption, which is not mathematical in nature. It is rather your
understanding what mathematics is and how it works. Unless one takes this
epistemic assumption for granted your argument doesn't work.

 My reason to take seriously the possibility of the in-consistency of PA is my
doubt that properties of formal counterparts of informal mathematical theories,
including (in)-consistency of formal theories, tell us much about the informal
mathematical theories themselves. I don't rule out the possibility that they
tell us something but I believe we should better understand *what* they tell
exactly and how formalisation really works. Given such a doubt it doesn't seem
me inconceivable that PA is in-consistent while theorems of (the informal)
arithmetic are all true and their proofs are all sound (not in the technical
sense). It is possible that PA provides a wrong analysis of these informal
theorems. It seems me that Vladimir Voevodsky's reason to take seriously the
possibility of the in-consistency of PA is similar but I may be wrong, so in
order to understand better Vladimir's view one has to ask him directly.

In a separate posting I'll try to give some more precise reasons for doubting
the usual epistemic assumptions about formalisation.

Andrei