Why the emphasis on first-order logic?

  • #1
nomadreid
Gold Member
1,481
150
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.
 
  • Like
Likes Aufbauwerk 2045 and Demystifier

Answers and Replies

  • #2
andrewkirk
Science Advisor
Homework Helper
Insights Author
Gold Member
3,885
1,453
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.
 
  • Like
Likes nomadreid
  • #3
nomadreid
Gold Member
1,481
150
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.
 
  • #4
rubi
Science Advisor
847
348
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.
 
  • Like
Likes nomadreid
  • #5
nomadreid
Gold Member
1,481
150
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.
 
  • #6
rubi
Science Advisor
847
348
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
 
  • Like
Likes nomadreid
  • #7
nomadreid
Gold Member
1,481
150
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.
 
  • Like
Likes rubi
  • #8
Demystifier
Science Advisor
Insights Author
Gold Member
11,330
3,952
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
 
  • Like
Likes nomadreid
  • #9
nomadreid
Gold Member
1,481
150
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.
 
  • Like
Likes Demystifier
  • #10
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&tag=pfamazon01-20.
 
  • Like
Likes nomadreid

Related Threads on Why the emphasis on first-order logic?

  • Last Post
2
Replies
35
Views
7K
  • Last Post
Replies
6
Views
4K
  • Last Post
Replies
0
Views
1K
  • Last Post
Replies
3
Views
971
Replies
2
Views
711
  • Last Post
Replies
3
Views
3K
Replies
13
Views
8K
  • Last Post
Replies
1
Views
2K
Replies
1
Views
652
Top