Your original question (about the focus on first-order logic) was a very good one. I asked a logician friend about it, and his answer was the same as the one that you and Samuel settled on here—first-order logic is likely the best that humans brains (or machines) are able to access. So yeah, basically a version of the Church-Turing thesis.
They referred me to Lindström’s theorem as a concrete result in that direction. I don’t know enough to understand the statement of the theorem, but it seems to say something along the lines of “first-order logic is the strongest logic which still has [some properties that computable systems ought to have?].”
Fun fact I learned in the conversation: it is a theorem of first-order ZFC that the models of second-order ZFC are constrained enough to single out a canonical model of the integers.
Your original question (about the focus on first-order logic) was a very good one. I asked a logician friend about it, and his answer was the same as the one that you and Samuel settled on here—first-order logic is likely the best that humans brains (or machines) are able to access. So yeah, basically a version of the Church-Turing thesis.
They referred me to Lindström’s theorem as a concrete result in that direction. I don’t know enough to understand the statement of the theorem, but it seems to say something along the lines of “first-order logic is the strongest logic which still has [some properties that computable systems ought to have?].”
Fun fact I learned in the conversation: it is a theorem of first-order ZFC that the models of second-order ZFC are constrained enough to single out a canonical model of the integers.
Thanks for the links! I will try to explore in this direction.