Is there really that much difference between Second Order Logic, and First Order Logic quantifying over sets, or over classes?
Put it another way, Eliezer is using SOL to pinpoint the concept of a (natural) “number”. But to do that thoroughly he also needs to pinpoint the concept of a “property” or a “set” of numbers with that property, so he needs some axioms of set theory. And those set theory axioms had better be in FOL, because if they are also in SOL he will further need to pinpoint properties of sets (or proper classes of sets), so he needs some axioms of class theory. Somewhere it all bottoms out in FOL, doesn’t it?
Well, the topic is “logical pinpointing”, and the attempt to logically pinpoint logic itself sounds rather circular...
However, if we really want to, we can describe a computer program which systematically checks any given input string to decide whether it constitutes a valid string of deductions in FOL. Then “first order logic” is anything to which the program gives the answer “Valid”. That’s possible for FOL, but not for SOL. If you want to further pinpoint what a “program” is, the best way to do that is to find a computer and run the d**n thing!
Is there really that much difference between Second Order Logic, and First Order Logic quantifying over sets, or over classes?
Put it another way, Eliezer is using SOL to pinpoint the concept of a (natural) “number”. But to do that thoroughly he also needs to pinpoint the concept of a “property” or a “set” of numbers with that property, so he needs some axioms of set theory. And those set theory axioms had better be in FOL, because if they are also in SOL he will further need to pinpoint properties of sets (or proper classes of sets), so he needs some axioms of class theory. Somewhere it all bottoms out in FOL, doesn’t it?
Why isn’t it necessary to pin point FOL?
Well, the topic is “logical pinpointing”, and the attempt to logically pinpoint logic itself sounds rather circular...
However, if we really want to, we can describe a computer program which systematically checks any given input string to decide whether it constitutes a valid string of deductions in FOL. Then “first order logic” is anything to which the program gives the answer “Valid”. That’s possible for FOL, but not for SOL. If you want to further pinpoint what a “program” is, the best way to do that is to find a computer and run the d**n thing!