There is a lot of psuedo-arguing going on here. I’m a mathematician who specializes in logic and foundations, I think I can settle most of the controversy with the following summary:
1) Second-order logic is a perfectly acceptable way to formalize mathematics-in-general, stronger than Peano Arithmetic but somewhat weaker than ZFC (comparable in proof-theoretic strength to “Type Theory” of “Maclane Set Theory” or “Bounded Zermelo Set Theory”, which means sufficient for almost all mainstream mathematical research, though inadequate for results which depend on Frankel’s Replacement Axiom).
2) First-order logic has better syntactic properties than Second-order logic, in particular it satisfies Godel’s Completeness Theorem which guarantees that the syntax is adequate for the semantics. Second-order logic has better semantic properties than first-order logic, in particular avoiding nonstandard models of the integers and of set-theoretical universes V_k for various ordinals k.
3) The critics of second-order logic say that they don’t understand the concept of “finite integer” and “all subsets” and that the people using second-order logic are making meaningless noises, and all we really can be sure about is ZFC and its consequences, and since the ZFC axioms actually allow us to prove more theorems about objects we care about than the usual formalizations of second-order logic (such as, for example, the consistency of full Zermelo set theory), the fans of second-order logic should just quit and use ZFC instead
4) the fans of second-order logic reply that nothing we actually prove and translate into the language of set theory is false and our reasoning is sound by your standards so stop insulting us by claiming that since YOU can’t decide what’s true about sets, OUR notion of “property” or “subset” is vague and incoherent. We say that CH is either true of false but we don’t know which because we don’t have a deductive calculus that settles it which we are confident in, you say that CH is vague and meaningless, but this is a pseudo-problem until either you come up with new set-theoretical axioms which decide CH or we come up with a stonger deductive system which decides it. We can still prove “ZF proves Con(Z)”, we just think that the theorems we can derive in pure second-order logic are epistemologically better supported than theorems you need the full power of ZFC to prove (because they already follow from “logical” rather than “mathematical” axioms) and you shouldn’t mind us making this distinction.
5) The best theories of physics we have need real infinities and finitely many iterations of the Powerset axiom but Second Order Logic or “Type Theory” is completely adequate for them and it is hard to conceive that questions about higher infinites that require infinitely many iterations of the Powerset operation can be relevant to physics.
6) It is also hard to conceive that any form of mathematical finitism is adequate for making actual progress in theoretical physics, even if results that are proved using standard infinitary mathematics can be reformulated as finitary statements about integers and computations, these nominalistic reductions are so cumbersome that the self-imposed avoidance of infinitary ontology cripples physical insight.
(Since the average LW reader may not know whether to trust that this commenter is a mathematician specializing in logic and foundations, I remark that the above summary sounds much like the papers I’ve read on second-order logic. Though ‘pseudo-arguing’ is an odd way to describe the ancient expositional tradition of dialogue.)
it is hard to conceive that questions about higher infinites that require infinitely many iterations of the Powerset operation can be relevant to physics.
If sets with cardinalities equal to these higher infinities exist as mathematical entities, then some of them will be logically dependent on us, on what we do. For example those sets may contain intelligent beings who are simulating our universe and taking different actions based on what they observe. I don’t know if this is actually the case, or if it is, how much we ought to care, but it would be nice if an FAI could consider and try to answer questions like this, and not be arbitrarily limited in its reasoning by the choice of mathematical language we make when building it.
There is a lot of psuedo-arguing going on here. I’m a mathematician who specializes in logic and foundations, I think I can settle most of the controversy with the following summary:
1) Second-order logic is a perfectly acceptable way to formalize mathematics-in-general, stronger than Peano Arithmetic but somewhat weaker than ZFC (comparable in proof-theoretic strength to “Type Theory” of “Maclane Set Theory” or “Bounded Zermelo Set Theory”, which means sufficient for almost all mainstream mathematical research, though inadequate for results which depend on Frankel’s Replacement Axiom).
2) First-order logic has better syntactic properties than Second-order logic, in particular it satisfies Godel’s Completeness Theorem which guarantees that the syntax is adequate for the semantics. Second-order logic has better semantic properties than first-order logic, in particular avoiding nonstandard models of the integers and of set-theoretical universes V_k for various ordinals k.
3) The critics of second-order logic say that they don’t understand the concept of “finite integer” and “all subsets” and that the people using second-order logic are making meaningless noises, and all we really can be sure about is ZFC and its consequences, and since the ZFC axioms actually allow us to prove more theorems about objects we care about than the usual formalizations of second-order logic (such as, for example, the consistency of full Zermelo set theory), the fans of second-order logic should just quit and use ZFC instead
4) the fans of second-order logic reply that nothing we actually prove and translate into the language of set theory is false and our reasoning is sound by your standards so stop insulting us by claiming that since YOU can’t decide what’s true about sets, OUR notion of “property” or “subset” is vague and incoherent. We say that CH is either true of false but we don’t know which because we don’t have a deductive calculus that settles it which we are confident in, you say that CH is vague and meaningless, but this is a pseudo-problem until either you come up with new set-theoretical axioms which decide CH or we come up with a stonger deductive system which decides it. We can still prove “ZF proves Con(Z)”, we just think that the theorems we can derive in pure second-order logic are epistemologically better supported than theorems you need the full power of ZFC to prove (because they already follow from “logical” rather than “mathematical” axioms) and you shouldn’t mind us making this distinction.
5) The best theories of physics we have need real infinities and finitely many iterations of the Powerset axiom but Second Order Logic or “Type Theory” is completely adequate for them and it is hard to conceive that questions about higher infinites that require infinitely many iterations of the Powerset operation can be relevant to physics.
6) It is also hard to conceive that any form of mathematical finitism is adequate for making actual progress in theoretical physics, even if results that are proved using standard infinitary mathematics can be reformulated as finitary statements about integers and computations, these nominalistic reductions are so cumbersome that the self-imposed avoidance of infinitary ontology cripples physical insight.
(Since the average LW reader may not know whether to trust that this commenter is a mathematician specializing in logic and foundations, I remark that the above summary sounds much like the papers I’ve read on second-order logic. Though ‘pseudo-arguing’ is an odd way to describe the ancient expositional tradition of dialogue.)
If sets with cardinalities equal to these higher infinities exist as mathematical entities, then some of them will be logically dependent on us, on what we do. For example those sets may contain intelligent beings who are simulating our universe and taking different actions based on what they observe. I don’t know if this is actually the case, or if it is, how much we ought to care, but it would be nice if an FAI could consider and try to answer questions like this, and not be arbitrarily limited in its reasoning by the choice of mathematical language we make when building it.
Best mathematical comment on LessWrong in four years.
I applaud you, sir or madam.