Quoted By:
I just learn about stuff for a hobby and I don't know too much myself, but first you need to understand propositional logic (and, or, conditional, biconditional, truth tables and shit), then learn about first-order logic (quantifiers like for all, there exists). Once you know what all that means, there are a lot of different ways to do foundations. Some different ways of ways of formally express a proof and tell whether it's valid include Hilbert's system, natural deduction, sequent calculus, and truth trees. Then there are different ways of handling predicates / sets and constructing the objects of actual mathematics like natural numbers. On one hand you have ZFC and other set theories which give you axioms about sets, and tricks for encoding things like ordered pairs, numbers, and functions as particular sets of sets. For example, a natural number is usually encoded as the set of prior natural numbers, with zero being the empty set. Enderton's Elements of Set Theory goes over this. Alternatively you have higher-order logic which makes reasoning about predicates part of the logic, and in particular type theory, which teaches you to think of proofs as programs. One variant of this is CIC, used in the proof assistant Coq which can check formal proofs for you. In CIC you get a mechanism to directly create data types with recursive definitions; for example, a natural number is either zero or the successor of a natural number. One of the nice things about learning type theory and using Coq is that it makes it easy to play around with formal proofs and the mathematical objects you're constructing. I should mention Werner's "Sets in types, types in sets" paper which explains ways you can sort of convert back and forth between ZFC and CIC by encoding one system in the other.
There's lots of stuff I didn't even mention here. One thing I'd like to learn more about myself is model theory, so if anyone has any recommended texts or resources on that, I'd appreciate it.
