It seems like it should be straightforward. But it's mathematically impossible.
Similarly, it seemed to David Hilbert like it should be possible to have a system of formal logic that all could accept, which would prove itself to be consistent. But that also proved to be impossible. And the logic which lead to that being proved impossible is deeply connected to the first line of reasoning that I gave you for why this is also impossible.
And in the end what they all come down to is some kind of self-reference. In this case, to have a finite statement define what it means to be finite, we must already know what finite means. Second order logic sort of assumes that we can simply know what finite means. First order logic doesn't allow you to wave your hands like that. You can't cheat in any way. And so you can't find a way to do it.
> Similarly, it seemed to David Hilbert like it should be possible to have a system of formal logic that all could accept, which would prove itself to be consistent.
Minor nitpick, but I don't think this fully captures the essence of Hilbert's program. If we had a system that could prove itself consistent, that would mean nothing, because the system could be inconsistent, therefore unsound and so its consistency "proof" wouldn't mean anything.
Rather, the goal was to start from an arguably "uncontroversial" base of mathematics (something like primitive recursive arithmetic, which intuitionists might also accept) and use that to bootstrap "infinitary mathematics" of the kind the formalists such as Hilbert were arguing for. The hope was that one could prove the consistency of such more abstract mathematics (PA or ZFC) from the more concrete foundations.
Unfortunately, Gödel's theorems completely demolish that idea. It's not just that a (sufficiently strong) theory can't prove itself consistent, it also can't be proven consistent by a strictly weaker theory such as PRA (because if such a proof existed in the weaker system, it would of course also exist in original system).
> Second order logic sort of assumes that we can simply know what finite means. First order logic doesn't allow you to wave your hands like that.
OK, this I do not understand. How does 2ndOL "sort of assume that we can simply know what finite means"? That seems like an extraordinarily imprecise characterization of 2ndOL. 2ndOL is a formal system just like 1stOL. Neither one lets you "wave your hands" about anything AFAICT.
I view the "for all properties" bit as handwaving. See particularly section 6 of that article, which at one point gives:
The semantics of second-order logic depending on these hard questions of set theory puts second-order logic into the same “basket” with set theory. Criticism of set theory becomes criticism of second-order logic and vice versa.
My Constructivist tendencies are due to my discomfort with accepting the validity of set-theoretic constructions with decisions based on unverifiable truths. Accepting second order logic requires accepting quantifying over similar collections of unverifiable claims. I'm going to be no more sympathetic.
It seems like it should be straightforward. But it's mathematically impossible.
Similarly, it seemed to David Hilbert like it should be possible to have a system of formal logic that all could accept, which would prove itself to be consistent. But that also proved to be impossible. And the logic which lead to that being proved impossible is deeply connected to the first line of reasoning that I gave you for why this is also impossible.
And in the end what they all come down to is some kind of self-reference. In this case, to have a finite statement define what it means to be finite, we must already know what finite means. Second order logic sort of assumes that we can simply know what finite means. First order logic doesn't allow you to wave your hands like that. You can't cheat in any way. And so you can't find a way to do it.