I’m not sure exactly what Eliezer intends, but I’ll put in my two cents:
A proof is simply a game of symbol manipulation. You start with some symbols, say ‘(’, ‘)’, ‘¬’, ‘→’, ‘↔’, ‘∀’, ‘∃’, ‘P’, ‘Q’, ‘R’, ‘x’, ‘y’, and ‘z’. Call these symbols the alphabet. Some sequences of symbols are called well-formed formulas, or wffs for short. There are rules to tell what sequences of symbols are wffs, these are called a grammar. Some wffs are called axioms. There is another important symbol that is not one of the symbols you chose—this is the ‘⊢’ symbol. A declaration is the ‘⊢’ symbol followed by a wff. A legal declaration is either the ‘⊢’ symbol followed by an axiom or the result of an inference rule. An inference rule is a rule that declares that a declaration of a certain form is legal, given that certain declarations of other forms are legal. A famous inference rule called modus ponens is part of a formal system called first-order logic. This rule says: “If ‘⊢ P’ and ‘⊢ (P → Q)’ (where P and Q are replaced with some wffs) are valid declarations, then ‘⊢ Q’ is also a valid declaration.” By the way, a formal system is just a specific alphabet, grammar, set of axioms, and set of inference rules. You also might like to note that if ‘⊢ P’ (where P is replaced with some wff) is a valid declaration, then we also call P a theorem. So now we know something: In a formal system, all axioms are theorems.
The second thing to note is that a formal system does not necessarily have anything to do with even propositional logic (let alone first- or second-order logic!). Consider the MIU system (open link in WordPad, on Windows), for example. It has four inference rules for just messing around with the order of the letters, ‘M’, ‘I’, and ‘U’! That doesn’t have to do with the real world or even math, does it?
The third thing to note is that, though a formal system can tell us what wffs are theorems, it cannot (directly) tell us what wffs are not theorems. And hence we have the MU puzzle. This asks whether “MU” is a theorem in the MIU system. If it is, then you only need the MIU system to demonstrate this, but if it is not, you need to use reasoning from outside of that system.
As other commenters have already noted, mathematicians are not thinking about ZFC set theory when they prove things (that’s not a bad thing; they’d never manage to prove any new results if they had to start from foundations for every proof!). However, mathematicians should be fairly confident that the proofs they create could be reduced down to proofs from the low-level axioms. So Eliezer is definitely right to be worried when a mathematician says “A proof is a social construct – it is what we need it to be in order to be convinced something is true. If you write something down and you want it to count as a proof, the only real issue is whether you’re completely convincing.”. A proof is a social construct, but it is one, very, very specific kind of social construct. The axioms and inference rules of first-order Peano arithmetic are symbolic representations of our most fundamental notion of what the natural numbers are. The reason for propositional logic, first-order logic, second-order logic, Peano arithmetic, and the scientific method is that humans have little things called “cognitive biases”. We are convinced by way too many things that should be utterly unconvincing. To say that a proof is a convincing social construct is...technically...correct (oh how it pains me to say that!)...but that very vague part of what it means for something to be a proof seems to imply that a proof is the utter antithesis of what it was meant for! A mathematical proof should be the most convincing social construct we have, because of how it is constructed.
First-order Peano arithmetic has just a few simple axioms, and a couple simple inference rules, and its symbols have a clear intended interpretation (in terms of the natural numbers (which characterize parts of the web of causality as already explained in the OP)). The truth of a few simple axioms and validity of a couple simple inference rules can be evaluated without our cognitive biases getting in the way. On the other hand, it’s probably not a good idea to make “There is a prime number larger than any given natural number.” an axiom of a formal system about the natural numbers, because it is not an immediate part of our intuitive understanding of how causal systems that behave according to the rules of the natural numbers behave. We as humans would have to be very, very, confused if a theorem of first-order Peano arithmetic (because we are so sure that its axioms are true and its inference rules are valid) turned out to be the negation of another theorem of Peano arithmetic, but not so confused if the same happened for ZFC set theory, because we do not so readily observe infinite sets in our day-to-day experience. The axioms and inference rules of first-order Peano arithmetic more directly correspond to our physical reality than those of ZFC set theory do (and the axioms and inference rules of the MIU system have nothing to do with our physical reality at all!). If a contradiction in first-order Peano arithmetic were found, though, life would go on. First-order Peano arithmetic does have a lot to do with our physical reality, but not all of it does. It inducts to numbers like 3^^^3 that we will probably never interact with. The ultrafinitists would be shouting “Told you so!”
Now I have said enough to give my direct response to the comment I am replying to. First of all, the dichotomy between “logic” and “mathematics” can be dissolved by referring to “formal systems” instead. A formal system is exactly as entwined with reality as its axioms and inference rules are. In terms of instrumental rationality, the more exotic theorems of ZFC set theory (and MIU) really don’t help us, unless we intrinsically enjoy considering the question “What if there were (even though we have no evidence that this is the case) a platonic realm of sets? How would it behave?”
When used as means to an end, the point of a formal system is to correct for our cognitive biases. In other words, the definition of a proof should state that a proof is a “convincing demonstration that should be convincing”, to begin with. I suspect Eliezer is so concerned with the Peano axioms because computer programs happen to evidently behave in a very, very mathematical way, and he believes that eventually a computer program will decide the fate of humanity. I share his concerns; I want a mathematical argument that the General Artificial Intelligence that will be created will be Friendly, not anything that might “convince” a few uninformed government officials.
I don’t think we disagree about the social construct thing: see my other comment where I’m talking about that.
It sounds like you pretty much come down in favour of the second position that I articulated above, just with a formalist twist. Mathematical talk is about what follows from the axioms; obviously only certain sets of axioms are worth investigating, as they’re the ones that actually line up with systems in the world. I agree so far, but you think that there is no notion of logic beyond the syntactic?
First of all, the dichotomy between “logic” and “mathematics” can be dissolved by referring to “formal systems” instead.
Aren’t you just dropping the distrinction between syntax and semantics here? One of the big points of the last few posts has been that we’re interested in the semantic implications, and the formal systems are a (sound) syntactic means of reaching true conclusions. From your post it sounds like you’re a pretty serious formalist, though, so that may not be a big deal to you.
I would describe first-order logic as “a formal encapsulation of humanity’s most fundamental notions of how the world works”. If it were shown to be inconsistent, then I could still fall back to something like intuitionistic logic, but from that point on I’d be pretty skeptical about how much I could really know about the world, beyond that which is completely obvious (gravity, etc.).
What did I say that implied that I “think that there is no notion of logic beyond the syntactic”? I think of “logic” and “proof” as completely syntactic processes, but the premises and conclusions of a proof have to have semantic meaning; otherwise, why would we care so much about proving anything? I may have implied something that I didn’t believe, or I may have inconsistent beliefs regarding math and logic, so I’d actually appreciate it if you pointed out where I contradicted what I just said in this comment (if I did).
Looking back, it’s hard to say what gave me that impression. I think I was mostly just confused as to why you were spending quite so much time going over the syntax stuff ;) And
First of all, the dichotomy between “logic” and “mathematics” can be dissolved by referring to “formal systems” instead.
made me think that you though that all logical/mathematical talk was just talk of formal systems. That can’t be true if you’ve got some semantic story going on: then the syntax is important, but mainly as a way to reach semantic truths. And the semantics don’t have to mention formal systems at all. If you think that the semantics of logic/mathematics is really about syntax, then that’s what I’d think of as a “formalist” position.
Oh, I think I may understand your confusion, now. I don’t think of mathematics and logic as equals! I am more confident in first-order logic than I am in, say, ZFC set theory (though I am extremely confident in both). However, formal system-space is much larger than the few formal systems we use today; I wanted to emphasize that. Logic and set theory were selected for because they were useful, not because they are the only possible formal ways of thinking out there. In other words, I was trying to right the wrong question, why do mathematics and logic transcend the rest of reality?
I’m not sure exactly what Eliezer intends, but I’ll put in my two cents:
A proof is simply a game of symbol manipulation. You start with some symbols, say ‘(’, ‘)’, ‘¬’, ‘→’, ‘↔’, ‘∀’, ‘∃’, ‘P’, ‘Q’, ‘R’, ‘x’, ‘y’, and ‘z’. Call these symbols the alphabet. Some sequences of symbols are called well-formed formulas, or wffs for short. There are rules to tell what sequences of symbols are wffs, these are called a grammar. Some wffs are called axioms. There is another important symbol that is not one of the symbols you chose—this is the ‘⊢’ symbol. A declaration is the ‘⊢’ symbol followed by a wff. A legal declaration is either the ‘⊢’ symbol followed by an axiom or the result of an inference rule. An inference rule is a rule that declares that a declaration of a certain form is legal, given that certain declarations of other forms are legal. A famous inference rule called modus ponens is part of a formal system called first-order logic. This rule says: “If ‘⊢ P’ and ‘⊢ (P → Q)’ (where P and Q are replaced with some wffs) are valid declarations, then ‘⊢ Q’ is also a valid declaration.” By the way, a formal system is just a specific alphabet, grammar, set of axioms, and set of inference rules. You also might like to note that if ‘⊢ P’ (where P is replaced with some wff) is a valid declaration, then we also call P a theorem. So now we know something: In a formal system, all axioms are theorems.
The second thing to note is that a formal system does not necessarily have anything to do with even propositional logic (let alone first- or second-order logic!). Consider the MIU system (open link in WordPad, on Windows), for example. It has four inference rules for just messing around with the order of the letters, ‘M’, ‘I’, and ‘U’! That doesn’t have to do with the real world or even math, does it?
The third thing to note is that, though a formal system can tell us what wffs are theorems, it cannot (directly) tell us what wffs are not theorems. And hence we have the MU puzzle. This asks whether “MU” is a theorem in the MIU system. If it is, then you only need the MIU system to demonstrate this, but if it is not, you need to use reasoning from outside of that system.
As other commenters have already noted, mathematicians are not thinking about ZFC set theory when they prove things (that’s not a bad thing; they’d never manage to prove any new results if they had to start from foundations for every proof!). However, mathematicians should be fairly confident that the proofs they create could be reduced down to proofs from the low-level axioms. So Eliezer is definitely right to be worried when a mathematician says “A proof is a social construct – it is what we need it to be in order to be convinced something is true. If you write something down and you want it to count as a proof, the only real issue is whether you’re completely convincing.”. A proof is a social construct, but it is one, very, very specific kind of social construct. The axioms and inference rules of first-order Peano arithmetic are symbolic representations of our most fundamental notion of what the natural numbers are. The reason for propositional logic, first-order logic, second-order logic, Peano arithmetic, and the scientific method is that humans have little things called “cognitive biases”. We are convinced by way too many things that should be utterly unconvincing. To say that a proof is a convincing social construct is...technically...correct (oh how it pains me to say that!)...but that very vague part of what it means for something to be a proof seems to imply that a proof is the utter antithesis of what it was meant for! A mathematical proof should be the most convincing social construct we have, because of how it is constructed.
First-order Peano arithmetic has just a few simple axioms, and a couple simple inference rules, and its symbols have a clear intended interpretation (in terms of the natural numbers (which characterize parts of the web of causality as already explained in the OP)). The truth of a few simple axioms and validity of a couple simple inference rules can be evaluated without our cognitive biases getting in the way. On the other hand, it’s probably not a good idea to make “There is a prime number larger than any given natural number.” an axiom of a formal system about the natural numbers, because it is not an immediate part of our intuitive understanding of how causal systems that behave according to the rules of the natural numbers behave. We as humans would have to be very, very, confused if a theorem of first-order Peano arithmetic (because we are so sure that its axioms are true and its inference rules are valid) turned out to be the negation of another theorem of Peano arithmetic, but not so confused if the same happened for ZFC set theory, because we do not so readily observe infinite sets in our day-to-day experience. The axioms and inference rules of first-order Peano arithmetic more directly correspond to our physical reality than those of ZFC set theory do (and the axioms and inference rules of the MIU system have nothing to do with our physical reality at all!). If a contradiction in first-order Peano arithmetic were found, though, life would go on. First-order Peano arithmetic does have a lot to do with our physical reality, but not all of it does. It inducts to numbers like 3^^^3 that we will probably never interact with. The ultrafinitists would be shouting “Told you so!”
Now I have said enough to give my direct response to the comment I am replying to. First of all, the dichotomy between “logic” and “mathematics” can be dissolved by referring to “formal systems” instead. A formal system is exactly as entwined with reality as its axioms and inference rules are. In terms of instrumental rationality, the more exotic theorems of ZFC set theory (and MIU) really don’t help us, unless we intrinsically enjoy considering the question “What if there were (even though we have no evidence that this is the case) a platonic realm of sets? How would it behave?”
When used as means to an end, the point of a formal system is to correct for our cognitive biases. In other words, the definition of a proof should state that a proof is a “convincing demonstration that should be convincing”, to begin with. I suspect Eliezer is so concerned with the Peano axioms because computer programs happen to evidently behave in a very, very mathematical way, and he believes that eventually a computer program will decide the fate of humanity. I share his concerns; I want a mathematical argument that the General Artificial Intelligence that will be created will be Friendly, not anything that might “convince” a few uninformed government officials.
A few things:
I don’t think we disagree about the social construct thing: see my other comment where I’m talking about that.
It sounds like you pretty much come down in favour of the second position that I articulated above, just with a formalist twist. Mathematical talk is about what follows from the axioms; obviously only certain sets of axioms are worth investigating, as they’re the ones that actually line up with systems in the world. I agree so far, but you think that there is no notion of logic beyond the syntactic?
Aren’t you just dropping the distrinction between syntax and semantics here? One of the big points of the last few posts has been that we’re interested in the semantic implications, and the formal systems are a (sound) syntactic means of reaching true conclusions. From your post it sounds like you’re a pretty serious formalist, though, so that may not be a big deal to you.
Definitely position two.
I would describe first-order logic as “a formal encapsulation of humanity’s most fundamental notions of how the world works”. If it were shown to be inconsistent, then I could still fall back to something like intuitionistic logic, but from that point on I’d be pretty skeptical about how much I could really know about the world, beyond that which is completely obvious (gravity, etc.).
What did I say that implied that I “think that there is no notion of logic beyond the syntactic”? I think of “logic” and “proof” as completely syntactic processes, but the premises and conclusions of a proof have to have semantic meaning; otherwise, why would we care so much about proving anything? I may have implied something that I didn’t believe, or I may have inconsistent beliefs regarding math and logic, so I’d actually appreciate it if you pointed out where I contradicted what I just said in this comment (if I did).
Looking back, it’s hard to say what gave me that impression. I think I was mostly just confused as to why you were spending quite so much time going over the syntax stuff ;) And
made me think that you though that all logical/mathematical talk was just talk of formal systems. That can’t be true if you’ve got some semantic story going on: then the syntax is important, but mainly as a way to reach semantic truths. And the semantics don’t have to mention formal systems at all. If you think that the semantics of logic/mathematics is really about syntax, then that’s what I’d think of as a “formalist” position.
Oh, I think I may understand your confusion, now. I don’t think of mathematics and logic as equals! I am more confident in first-order logic than I am in, say, ZFC set theory (though I am extremely confident in both). However, formal system-space is much larger than the few formal systems we use today; I wanted to emphasize that. Logic and set theory were selected for because they were useful, not because they are the only possible formal ways of thinking out there. In other words, I was trying to right the wrong question, why do mathematics and logic transcend the rest of reality?