Less Wrong is a community blog devoted to refining the art of human rationality. Please visit our About page for more information.

Vladimir_M comments on Learning the foundations of math - Less Wrong

4 Post author: jsalvatier 24 October 2010 07:29PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (31)

You are viewing a single comment's thread. Show more comments above.

Comment author: Vladimir_M 24 October 2010 08:13:43PM *  1 point [-]

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.)

Comment author: jsalvatier 24 October 2010 08:27:30PM *  0 points [-]

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")?

Comment author: Vladimir_M 24 October 2010 09:22:24PM *  2 points [-]

jsalvatier:

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?

Because it's far easier to work that way. You don't need ten different digits to work with natural numbers either, but we still do it for convenience. When you see the formula (p&q)->r, it's much easier to figure out what's going on than if it's in the form ((p|q)|(p|q))|(r|r). (Here "|" is the Sheffer symbol, i.e. NAND, which is by itself functionally complete.)

Is there a formal concept of an alias in math (for example, "a implies b" could be an alias for "(not a) or b")?

Math texts often introduce some notational aliases to make the text more readable, and logic texts do it almost invariably. For example, in the standard syntax of first-order logic, "+" is a binary function symbol, and "=" is a binary predicate, but it's still customary to introduce easier to read notation "x+y" and "x=y" where it should be "+xy" and "=xy". However, these conventions don't have any implications for the actual results being proven and discussed; the theorems still talk about formulas containing "+xy", and you just translate on the fly between that notation and the intuitive one as necessary.

In contrast, introducing additional operators into your definition of logic formulas changes things significantly, since now all your proofs have to account for these additional sorts of well-formed formulas, and also the formal proof system you use must be able to handle them. On the other hand, a good choice of a non-minimal functionally complete set of operators will make the entire work much easier to handle. So in practice, a non-minimal set is normally used. You can also use notation conventions like p->q instead of (~p v q) as long as their relations with the formal syntax are clear and simple enough. (Which definitely wouldn't be the case if you based the entire logic on just NAND and then tried to define AND, OR, etc. as notational aliases.)

Comment author: jsalvatier 25 October 2010 12:39:38AM 0 points [-]

I hope I am not imposing, but Cook's notes have confused me. The first set introduces a syntax which is fine, but then it introduces semantics and starts using several terms that haven't yet been defined (iff, maps and sets) are these part of meta-theory and conceptually different from being part of propositional logic? What am I missing?

Comment author: Vladimir_M 25 October 2010 01:10:48AM *  0 points [-]

Yes, these are concepts from the meta-theory, i.e. the language in which you speak about the formal logic you're defining. When you define, say, sets of formulas, or maps (i.e. functions) from atoms to truth values, these objects exist outside of the formal system (i.e logic) under discussion.

Now of course, you can ask how come we're talking about sets (and functions and other objects which are sets), when we're just defining the formal logic we'll use to axiomatize the set theory. The answer is that you have to start from somewhere; you can't start speaking if you don't already have a language. For this, you use the existing mathematics whose logical foundations are imperfectly formalized and intuitive. This trails off into deep philosophical issues, but you can look at it this way: before embarking on meta-mathematics, imperfectly formalized mathematics is the most rigorous logical tool available, and we're trying to "turn it against itself," to see what it has to say about its own foundations.

Comment author: jsalvatier 25 October 2010 01:19:46AM 0 points [-]

Does one need meta-theory to work from propositional logic to set theory? Can I safely ignore those parts (perhaps coming back later) if my goal is to learn do theory and not to say something about theory?

Comment author: Vladimir_M 25 October 2010 01:35:54AM 0 points [-]

I'm not sure I understand your question. What exactly would you want to skip, and why?

Comment author: jsalvatier 25 October 2010 02:49:00AM 0 points [-]

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?

Comment author: Vladimir_M 25 October 2010 03:28:30AM *  0 points [-]

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?

Comment author: jsalvatier 25 October 2010 04:31:08AM 0 points [-]

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.

Comment author: jsalvatier 25 October 2010 12:23:44AM 0 points [-]

I don't understand why this should be significantly easier, but I'll take your word for it; a formal system is a formal system, I suppose.

Comment author: Vladimir_M 25 October 2010 12:48:27AM 0 points [-]

Take the axioms of ZFC, Peano arithmetic, or some other familiar theory and try writing them down in a logic formalism that features only the NAND connective, and you'll see what I'm talking about. (Better yet, try devising a formal proof system using such formalism!)