Why the emphasis on first-order logic?

[nomadreid]

It seems to me that, despite several systems developed for higher-order logics, almost all the attention in Logic is devoted to first-order. I understand that higher-order logics have some drawbacks, such as the compactness theorem and the Löwenheim-Skolem theorems and other such not holding in second-order. However, there are some advantages as well, for example doing away with a lot of messy schemata. I would understand if the whole Logic community was composed of Intuitionists or Constructivists, since sets/classes using quantification over sets or relations are harder to construct, or if the Logic community was worried about programming issues, but since neither of these is in fact the case, I am puzzled by the preponderance of attention to first-order results. I know this is a broad question, so any responses will be appreciated.

 

[andrewkirk]

In First-Order Predicate Logic we can axiomatise ZFC set theory, and once we have that we can do almost all interesting mathematics. So there is no need to tiptoe amongst the minefields that arise in higher order logics.

The only well-known bit I'm not sure about is Category Theory, which seems to need something more than just set theory. It's on my to-do list to one day do enough Category Theory to understand what platform it requires to give it sufficient rigour.

Perhaps something about transfinite ordinals as well - another item on my to-do list.

 

[nomadreid]

Thanks, andrewkirk. That makes sense. Actually, almost all the theory on transfinite ordinals that I have seen concentrates on a first-order base as well. But it seems so nice to be able to finitely axiomatise ZFC, possible in second-order but not in first-order. It would also make some theories of truth simpler, perhaps.
I think Category Theory can be done mostly in second-order, but I am not strong on Category Theory, so I won't go into that.

 

[rubi]

The only well-known bit I'm not sure about is Category Theory, which seems to need something more than just set theory. It's on my to-do list to one day do enough Category Theory to understand what platform it requires to give it sufficient rigour.

Much of category theory can be done in ZFC as well. For some constructions however, you need the universe axiom, which is equivalent to the postulate that for every cardinal, there exists a larger inaccessible cardinal.

 

[nomadreid]

Much of category theory can be done in ZFC as well. For some constructions however, you need the universe axiom, which is equivalent to the postulate that for every cardinal, there exists a larger inaccessible cardinal.

Indeed, and at first glance the universe axiom (aka the inaccessible cardinal axiom) cannot be stated within first-order logic -- but I am ready to be corrected on this. Anyone? Nice example, rubi.

 

[rubi]

Indeed, and at first glance the universe axiom (aka the inaccessible cardinal axiom) cannot be stated within first-order logic -- but I am ready to be corrected on this. Anyone? Nice example, rubi.

I wouldn't want to call the universe axiom the inaccessible cardinal axiom, because there are several ways to postulate an inaccessible cardinal and the universe axiom is just one of them. The universe axiom can also be stated in first-order logic, but it is quite complicated. You can find it on Metamath: http://us.metamath.org/mpeuni/ax-groth.html

 

[nomadreid]

The Metamath version is impressive, thanks.
True, the "inaccessible cardinal axiom" is ambiguous, as it could be mixed up with the axiom that says that there exists an inaccessible cardinal, quite a different kettle of fish.

 

[Demystifier]

It seems to me that, despite several systems developed for higher-order logics, almost all the attention in Logic is devoted to first-order. I understand that higher-order logics have some drawbacks, such as the compactness theorem and the Löwenheim-Skolem theorems and other such not holding in second-order. However, there are some advantages as well, for example doing away with a lot of messy schemata. I would understand if the whole Logic community was composed of Intuitionists or Constructivists, since sets/classes using quantification over sets or relations are harder to construct, or if the Logic community was worried about programming issues, but since neither of these is in fact the case, I am puzzled by the preponderance of attention to first-order results. I know this is a broad question, so any responses will be appreciated.

This may be enlightening:
https://www.lesswrong.com/posts/MLq...ss-incompleteness-and-what-it-all-means-first
https://www.lesswrong.com/posts/SWn4rqdycu83ikfBa/second-order-logic-the-controversy

 

[nomadreid]

Demystifier: Thanks, I enjoy the "less wrong" blogs. The essence of the first one (mostly introductory) with respect to my question is the quote
"The lack of completeness means that the truths of second order logic cannot be enumerated - it has no complete proof procedure."
And in the second, he repeats that point before then going into an interesting discussion that I will have to go over again (I've bookmarked it) about the relationships between first order, second order, set theories, and the physical universe. On a first reading I am not actually sure that the author comes to a conclusion in terms of physicists' interest in second-order, but I will be re-reading it. Thanks again.

 

[Aufbauwerk 2045]

I've done some AI programming using FOPL, and also looked into higher-order logic from the viewpoint of developing AI software. AFAIK there is no practical alternative right now to using FOPL for the type of application I was working on. One benefit is the availability of the resolution method of theorem proving. For a reference see https://www.amazon.com/dp/0137117485/?tag=pfamazon01-20.