The meta-theory parts, so that I am learning just how to make proofs in theory X (e.g. propositional logic), and not learning how to prove things things about theory X proofs. Introduction to Mathematical Logic claims that all theories can be formalized; learning how to work in a theory first and then later possibly coming back to learn how to prove things about proofs in that theory seems like a good way to avoid being confused, and that’s largely my goal. Does that clarify?
That depends on what you want to use formal logic for. If you just want some operational knowledge of propositional logic for working with digital circuits, then yes, any digital systems textbook will teach you that much without any complex math. Similarly, you can learn the informal basics of predicate logic by just figuring out how its formulas map onto English sentences, which will enable you to follow its usual semi-formal usage in regular math prose. But if you want to actually study math foundations, then you need full rigor from the start.
Perhaps there is some confusion about what it is precisely that you want to learn. Could you list some concrete mathematical problems and theories that you’d like to understand, or some applications for which you’d like to learn the necessary math?
This mostly started because I was trying to learn stochastic differential equations and to a lesser extent topology. I became unsatisfied with my understanding of set theory (not sure how to answer questions like “when I construct a set, what am I iterating over?”), and to a lesser extent measure theory. When I went to get the foundations of set theory, I realized I wasn’t even very familiar with first order logic, and I continued down the rabbit hole.
At the moment I am not especially interested in questions like “is this theory consistent”. I am primarily interested in how one does the fundamental theories of math in a way that bottoms out, meaning I can see and enumerate the notions or procedures I am just taking for granted or defining. If propositional logic was just constructing a specific context free grammer and saying statements constructed in this manner are called ‘proofs’ for this grammar I think that would satisfy me (though it doesn’t look like this is all logic involves). I could easily be using the phrase “foundations of math” incorrectly; please tell me if I am.
Then foundations texts are not what you’re looking for. If I understand you correctly, you seem to be confused about the way sets and other basic constructs are used in normal mathematical prose, and you’d like to learn formal logic and formal proof systems, and then use this knowledge to tackle your problem.
Unfortunately, that’s not a feasible way to go, because to learn metamathematics, you first have to be proficient in regular mathematics—and even when you learn it, it won’t help you in understanding standard human-friendly math texts, except insofar as the experience improves your general math skills. Moreover, formal set theory is about esoteric questions that are very rarely relevant for non-foundational areas like differential equations, in which informal naive set theory is nearly always adequate. (In topology you might run into foundational issues, depending on what exactly you’re after.)
So, what you really need is an introductory text about classical mathematical reasoning. I’m not familiar with any such books in English, but the book nhamman recommended (How to Prove It) seems to be exactly what you’re looking for, judging by the Google preview.
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 I understand your question. What exactly would you want to skip, and why?
The meta-theory parts, so that I am learning just how to make proofs in theory X (e.g. propositional logic), and not learning how to prove things things about theory X proofs. Introduction to Mathematical Logic claims that all theories can be formalized; learning how to work in a theory first and then later possibly coming back to learn how to prove things about proofs in that theory seems like a good way to avoid being confused, and that’s largely my goal. Does that clarify?
That depends on what you want to use formal logic for. If you just want some operational knowledge of propositional logic for working with digital circuits, then yes, any digital systems textbook will teach you that much without any complex math. Similarly, you can learn the informal basics of predicate logic by just figuring out how its formulas map onto English sentences, which will enable you to follow its usual semi-formal usage in regular math prose. But if you want to actually study math foundations, then you need full rigor from the start.
Perhaps there is some confusion about what it is precisely that you want to learn. Could you list some concrete mathematical problems and theories that you’d like to understand, or some applications for which you’d like to learn the necessary math?
This mostly started because I was trying to learn stochastic differential equations and to a lesser extent topology. I became unsatisfied with my understanding of set theory (not sure how to answer questions like “when I construct a set, what am I iterating over?”), and to a lesser extent measure theory. When I went to get the foundations of set theory, I realized I wasn’t even very familiar with first order logic, and I continued down the rabbit hole.
At the moment I am not especially interested in questions like “is this theory consistent”. I am primarily interested in how one does the fundamental theories of math in a way that bottoms out, meaning I can see and enumerate the notions or procedures I am just taking for granted or defining. If propositional logic was just constructing a specific context free grammer and saying statements constructed in this manner are called ‘proofs’ for this grammar I think that would satisfy me (though it doesn’t look like this is all logic involves). I could easily be using the phrase “foundations of math” incorrectly; please tell me if I am.
Then foundations texts are not what you’re looking for. If I understand you correctly, you seem to be confused about the way sets and other basic constructs are used in normal mathematical prose, and you’d like to learn formal logic and formal proof systems, and then use this knowledge to tackle your problem.
Unfortunately, that’s not a feasible way to go, because to learn metamathematics, you first have to be proficient in regular mathematics—and even when you learn it, it won’t help you in understanding standard human-friendly math texts, except insofar as the experience improves your general math skills. Moreover, formal set theory is about esoteric questions that are very rarely relevant for non-foundational areas like differential equations, in which informal naive set theory is nearly always adequate. (In topology you might run into foundational issues, depending on what exactly you’re after.)
So, what you really need is an introductory text about classical mathematical reasoning. I’m not familiar with any such books in English, but the book nhamman recommended (How to Prove It) seems to be exactly what you’re looking for, judging by the Google preview.
Thanks for your help, I think you’ve clarified a lot for me.
Would you classify propositional logic/first-order-logic as necessarily metamathematical?
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.