[FOM] the debate with Professor Kanovei

[podnieks@latnet.lv]

Reply to Martin Davis <martin at eipye.com>:

Prof.Davis> This is where Kanovei is stuck: he can only see "many formal 
systems"; the possibility of speaking meaningfully of some assertion 
being "true" independent of provability in a specific formal system, he 
dismisses as a kind of mysticism, incompatible with science. His position is 
perfectly consistent and there is no arguing him out of it. <Prof.Davis

Thank you for an extremely clear formulation of the core problem in the 
foundations of mathematics. It would be hard to put it better. I would propose 
voting of all FOM members for or against "formalism" (against or 
for "mysticism") according to the above definition by Prof.Davis. Let us 
establish two parliament groups and elect speakers? I would vote 
for "formalism". Of course, Godel, Post and Penrose would vote "against". But, 
I suspect, Einstein, von Neumann and Kolmogorov would vote "for". Let us try 
using the creative potential of both parties? Or, must all "true" formalists 
resign?

Prof.Davis> He is like one devoted to the Ptolemaic system in which the sun 
and planets revolve about the earth: his account will have to put up with 
baroque complexities (the famous epicycles) but he cannot be dislodged from 
his view by pure reason. <Prof.Davis

Simply, the 75 years after Hilbert and Ackermann published the axioms of the 
first order functional calculus did no produce neither Copernicus, nor a 
Copernican idea...

(For me, in our movie, "Copernicus" is featured by Frege, "Galileo" - by 
Russell and Hilbert, "a collective Newton" - by Post, Godel, Turing and other 
creators of the formal concept of algorithm.)

Prof.Davis> ... It may be worth considering what this position (unassailable 
as it is) entails. An assertion that some particular tuple of numbers 
satisfies the equation involves nothing more complicated than addition and 
multiplication of integers. To claim that it is meaningless to say that there 
is no solution is really remarkable. <Prof.Davis

Here we have, indeed, the key point. Thank you, again. I would only correct 
the "claim": it is meaningless to say that the statement "there is no 
solution" possess some "objective truth value" independent of provability in a 
specific formal system. Unfortunately, this is the well-known old Platonist-
Formalist controversy.

Prof.Davis>It is particularly remarkable given that Kanovei somehow regards 
formal syntax as immune from his philosophical objections. The assertion that 
a particular theory is consistent is no simpler than what we have been 
discussing... <Prof.Davis

I believe, he does not regard formal syntax as immune. But, of course, only by 
using "many formal systems" (many theories - several metatheories - a few 
metametatheories) we can understand all the complicated things that are 
discussed on the FOM.

Best regards,
Karlis.Podnieks at mii.lu.lv