Informal proof, formal proof, formalism (Q2804472)

This paper consists of the author's attempt to save a metaphysically motivated formalism -- one stemming from ``a desire to avoid commitment to a platonistic ontology'' one believing ``that this can be effected either by replacing the notion of truth, as applied to mathematical sentences, by that of proof, or by closely identifying truth with formal proof'' -- from \textit{Y. Rav}'s objections to what he calls in [Philos. Math. (3) 7, No. 1, 5--41 (1999; Zbl 0941.03003)] ``Hilbert's thesis'', stating that ``every mathematical proof can be converted into a formal derivation in a suitable formal system.''NEWLINENEWLINETo this end, the author introduces the following modified version, called Hilbert's thesis II (HT II): ``In any cogent mathematical practice there is a systematic process of transformation (not necessarily known to the practitioners) which turns any correct proof into a (suitably related) finite derivation in a formal system \(S\). The system \(S\) in question is determined by the informal practice and its transformation process; in particular, the formal rules of \(S\) are rules which are implicit in the mathematical practice.'' While rejecting HT II, and thus agreeing with a part of Rav's criticism of formalism, the author does not accept Rav's anti-formalism, by assigning a role to idealisation, replacing the claim that ``truth is determined by concrete provability'' by ``formal idealisation of truth coincides with the formal idealisation of provability.''