I’m not sure what you mean by “necessarily metamathematical.”
Propositional logic isn’t powerful enough to be of that much use in metamathematics. Its main applications are technical. Most notably, it’s the fundamental basis for digital systems, but it’s also used in various methods for optimization, formal verification, etc. Consequently, it also has huge importance in theoretical computer science.
First-order logic, on the other hand, is principally a tool of metamathematics. Sometimes it’s used in a semi-formal way as a convenient shorthand for long and cumbersome natural-language sentences. But its principal applications are metamathematical, and its significance stems from the fact that it’s powerful enough to formalize “normal” mathematics, which then enables you to reason about that formalism mathematically, and thus examine the foundations of math using mathematical reasoning. (Hence the “meta.”)
I’m not sure what you mean by “necessarily metamathematical.”
Propositional logic isn’t powerful enough to be of that much use in metamathematics. Its main applications are technical. Most notably, it’s the fundamental basis for digital systems, but it’s also used in various methods for optimization, formal verification, etc. Consequently, it also has huge importance in theoretical computer science.
First-order logic, on the other hand, is principally a tool of metamathematics. Sometimes it’s used in a semi-formal way as a convenient shorthand for long and cumbersome natural-language sentences. But its principal applications are metamathematical, and its significance stems from the fact that it’s powerful enough to formalize “normal” mathematics, which then enables you to reason about that formalism mathematically, and thus examine the foundations of math using mathematical reasoning. (Hence the “meta.”)
Thanks, that clears up quite a bit.