The links I posted in that thread are, to my knowledge, the best free online resources. If you go through Cook's lecture notes, and then continue with the foundations text by Podnieks, it will be pretty much what you're looking for, up to and including the basics of set theory. I'm not familiar with literature in measure theory, though.
Regarding your stated preferences, I'm not sure if you can find math textbooks that use formal context-free grammar to define well-formed formulas. However, it's typically done using recursive definitions that are trivial to formalize as CFGs, so it shouldn't be a problem. In addition, I don't understand what benefit you see in formalizations of propositional logic with only two operators. It will just complicate the exposition and make it less understandable. (And why stop there? You can do it with only one.)
Your road map is helpful. Thanks :)
I didn't mean to say that you couldn't use what you had derived later on, but if you can define a theory with with 1 operator, why do it with more? Is there a formal concept of an alias in math (for example, "a implies b" could be an alias for "(not a) or b")?
I have recently become interested in the foundations of math. I am interested in tracing the fundamentals of math in a path such as: propositional logic -> first order logic -> set theory -> measure theory. Does anyone have any resources (books, webpages, pdfs etc.) they would like to recommend?
This seems like it would be a popular activity among LWers, so I thought this would be a good place to ask for advice.
My criteria (feel free to post resources which you think others who stumble across this might be interested in):