First versus Second Order Logic


So, which logic is superior? It depends to some extent on what we need it for. Anything provable in first order logic can be proved in second order logic, so if we have a choice of proofs, picking the first order one is the better option. First order logic has more pleasing internal properties, such as the completeness theorem, and one can preserve this in second order via Henkin semantics without losing the ability to formally express certain properties. Finally, one needs to make use of set theory and semantics to define full second order logic, while first order logic (and Henkin semantics) get away with pure syntax.

On the other hand, first order logic is completely incapable of controlling its infinite models, as they multiply, uncountable and generally incomprehensible. If rather that looking at the logic internally, we have a particular model in mind, we have to use second order logic for that. If we’d prefer not to use infinitely many axioms to express a simple idea, second-order logic is for us. And if we really want to properly express ideas like “every set has a least element”, “every analytic function is uniquely defined by its power series” – and not just express them, but have them mean what we want them to mean – then full second order logic is essential.

— Completeness, incompleteness, and what it all means: first versus second order logic

— Stuart Armstrong

2014.01.11 Saturday ACHK