Informal versus formal mathematics (Q885512): Difference between revisions

In order to illustrate the differences between the formal and informal approaches to mathematics, the author presents two striking examples. First, he presents a short discussion of Kunen's algorithmic implementation [see \textit{K. Kunen}, ``A Ramsey theorem in Boyer-Moore logic'', J. Autom. Reasoning 15, No.~2, 217--235 (1995; Zbl 0836.03031)], based on the Boyer-Moore theorem prover, of a proof of the Paris-Harrington theorem (see [\textit{J. Paris} and \textit{L. Harrington}, ``A mathematical incompleteness in Peano arithmetic'', in: J. Barwise (ed.), Handbook of mathematical logic. Amsterdam: North-Holland, 1133--1142 (1977; Zbl 0443.03001)]). Then, the author's proposal, with \textit{N. C. A. da Costa} [``Consequences of an exotic definition for \(\text{P}=\text{NP}\)'', Appl. Math. Comput. 145, No.~2--3, 655--665 (2003; Zbl 1046.68060); addendum ibid. 172, No.~2, 1364--1367 (2006)], of an `exotic' formalization of the \(\text{P}=\text{NP}\) hypothesis in Zermelo-Fraenkel set theory is presented and elaborated.