RE: Mathematicians who are finitists.
June 30, 2019 at 1:23 pm
(This post was last modified: June 30, 2019 at 1:42 pm by A Toy Windmill.)
Here is some recent research in finitistic mathematics.
Like all such research, it is metamathematics. The goal is to find methods to translate ordinary classical mathematical proofs to finistic ones, so that mathematicians don't have to make too many changes to their practice. The Hilbert Programme had the boldest ambition, to show that mathematicians needn't make any changes, in effect showing that mathematics was already, at least methodologically, finitistic. With that done, any further arguments could be relegated to the philosophy department. However, various results in proof theory showed that this goal was unachievable.
Goodstein, by the way, came up with a very beautiful computable function that bears his name. It can be written in about half a page of computer code, but you won't get it to terminate with anything but trivial inputs. The proof that it does terminate given enough memory and time requires induction up to ε0, making it one of the first interesting results to be shown outside the scope of Peano Arithmetic.
Like all such research, it is metamathematics. The goal is to find methods to translate ordinary classical mathematical proofs to finistic ones, so that mathematicians don't have to make too many changes to their practice. The Hilbert Programme had the boldest ambition, to show that mathematicians needn't make any changes, in effect showing that mathematics was already, at least methodologically, finitistic. With that done, any further arguments could be relegated to the philosophy department. However, various results in proof theory showed that this goal was unachievable.
Goodstein, by the way, came up with a very beautiful computable function that bears his name. It can be written in about half a page of computer code, but you won't get it to terminate with anything but trivial inputs. The proof that it does terminate given enough memory and time requires induction up to ε0, making it one of the first interesting results to be shown outside the scope of Peano Arithmetic.
