つづき

https://mathoverflow.net/questions/332918/what-do-we-gain-with-higher-order-logics
What do we gain with higher order logics?
answered May 31, 2019
Andrej Bauer
If you're a categorical logician, then you are interested in the connections between formal systems and structure, as perceived in category theory.
In this case your view might be that logic is dictated by semantics. For example, the internal language of toposes is fully higher-order, while the internal logic of algebraic varieties is regular logic (just equations, conjunctions, and ∃
). And if you only care about Grothendieck toposes and geometric morphism, geometric logic is for you.

If you're a mathematician, you probably care mostly about using logic as a tool, in which case the primary concern is expressivity. You do not want to be told that some very natural mathematical idea cannot be stated formally, so you would naturally gravitate towards higher-order logics. However, it is known that such needs for expressivity can largely be met by combining first-order logic with set theory. And since logic and set theory are typically taught by logicians, who prefer first-order logic for their own purposes, the prevalent formal system advocated today is first-order logic with set theory. But ultimately, for an ordinary mathematician it does not matter much which one they use.

Computer-scientists have their own ideas about logic and typically take an engineering point of view: use the tool that is appropriate for the situation at hand. For example, when we formalize mathematics with a proof assistant (software that aids and oversees writing of formal proofs), we seek a formalism that allows us to get the job done as directly as possible. For large scale projects the overriding concern becomes proof engineering: how to organize large libraries of definitions and theorems, how to search them, how to write proofs so that they are robust with respect to small changes, etc. Traditional logic has almost nothing to say about these topics, and consequently does not influence much the choice of formalism used in proof assistants. So many proof assistants use type theory, which could be characterized as "predicative higher-order", a reasonable middle ground between first-order and unrestricted higher-order.
(引用終り)
以上