Yes. Mummert is far more qualified than I am on these matters. Here is a line from his reply that is important:
"So, even though Z2 with full second-order semantics is categorical, for any sound effective deductive system there are still true formulas of Z2 that are neither provable nor disprovable in that system."
The key is sound and effective deductive system. Think computable or mechanistic process for deduction. The second order Peano axioms with second order semantics are not and effective deduction system.
In all proofs you have to start with (or end up with depending on the direction your proofs go) axioms. In the second order Peano axioms with second order semantics you can end up in a situation where you don't know if a given statement is an axiom! Making that determination can be quite hard.
Fascinating! How does the situation arise where you don't know if something is an axiom? Aren't axioms either members of a small agreed-on set, or based on an axiom schema?
Well let's say I take as my axioms all true statements about the Natural numbers. Let's take the Goldbach conjecture. Is it an axiom? No one knows because no one knows if it is true or not.
When you say "small agreed upon set" you are in essence talking about a recursively enumerable set of axioms. A collection of axioms that is "small" enough so that one could easily determine if a statement is an axiom.
If you have time for another question, I'm still confused about how it applies to second-order arithmetic, though, since the Peano axioms are well-known and easily listed on a single piece of paper. What difficulty is there be in determining whether a statement is a second-order Peano axiom?
It seems particularly strange since there are apparently fewer axioms than in first-order Peano arithmetic (by replacing an axiom schema with a single induction axiom).
"So, even though Z2 with full second-order semantics is categorical, for any sound effective deductive system there are still true formulas of Z2 that are neither provable nor disprovable in that system."
The key is sound and effective deductive system. Think computable or mechanistic process for deduction. The second order Peano axioms with second order semantics are not and effective deduction system.
In all proofs you have to start with (or end up with depending on the direction your proofs go) axioms. In the second order Peano axioms with second order semantics you can end up in a situation where you don't know if a given statement is an axiom! Making that determination can be quite hard.