“Those who find this confusing may find it helpful to study mathematical logic, which trains one to make very sharp distinctions between the proposition P, a proof of P, and a proof that P is provable”
This is a bit of a side question, but wouldn’t a proof that P is provable be a proof of P? In fact, it sounds like a particularly elegant form of proof.
Hrm… if the system is isn’t necessarily trustworthy, then that the system proves that it can prove P doesn’t mean that it’s actually true that it can prove P, I guess.
EDIT: actually, having it as an explicit axiom “If this proves P, then P” runs you into trouble in any system that has something like Lob’s theorem.
(“if some specific subset of the rest of this system, (ie, other than this axiom) proves P, then P” can potentially be okay, though)
Seconded—this is an interesting question. (And I suspect that there are some interesting cases in which a proof that P is provable does not constitute a proof, but this is mainly because I’ve seen mathematicians break similarly intuitive propositions before.)
I suspect that there are some interesting cases in which a proof that P is provable does not constitute a proof, but this is mainly because I’ve seen mathematicians break similarly intuitive propositions before.
It wouldn’t surprise me either. However such cases would have to rely on a precise definition of ‘proof’ differently to what I use. The result would then be filed under ‘fascinating technical example’ but not under ‘startling revelation’ and I would take note of the jargon for use when talking to other mathematicians.
Here’s an example of what Doug Hofstadter writes in I Am A Strange Loop. Kurt Goedel discovered that Principia Mathematica by Bertrand Russell does provide reference to itself. So Russell in his book yields the propositions and their proofs, and then Goedel assigns specific numbers to proofs and therefore proves that there is a proof that they are in fact, provable
Outside of mathematics, a statement that is provable is also disprovable. Then it’s called a hypothesis.
I’m reminded of the joke where an engineer, a physicist, and a mathematician are going to a job interview. The interviewer has rigged a fire to start in the wastepaper basket, to see how they react in a crisis situation. The engineer sees the fire, sees the water cooler, grabs the water cooler and dumps it on the fire. The physicist sees the fire, sees the water cooler, grabs pencil and paper, calculates the exact amount of water needed to extinguish the fire, then pours that amount of water into the basket, exactly extinguishing the fire. The mathematician sees the fire, sees the water cooler, and says, “Ah! A solution exists!”.
“Those who find this confusing may find it helpful to study mathematical logic, which trains one to make very sharp distinctions between the proposition P, a proof of P, and a proof that P is provable”
This is a bit of a side question, but wouldn’t a proof that P is provable be a proof of P? In fact, it sounds like a particularly elegant form of proof.
If you trust base system B, then a proof that P is provable in B is good as gold to you. But it is not a proof in B.
http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/
Hrm… if the system is isn’t necessarily trustworthy, then that the system proves that it can prove P doesn’t mean that it’s actually true that it can prove P, I guess.
EDIT: actually, having it as an explicit axiom “If this proves P, then P” runs you into trouble in any system that has something like Lob’s theorem.
(“if some specific subset of the rest of this system, (ie, other than this axiom) proves P, then P” can potentially be okay, though)
Seconded—this is an interesting question. (And I suspect that there are some interesting cases in which a proof that P is provable does not constitute a proof, but this is mainly because I’ve seen mathematicians break similarly intuitive propositions before.)
It wouldn’t surprise me either. However such cases would have to rely on a precise definition of ‘proof’ differently to what I use. The result would then be filed under ‘fascinating technical example’ but not under ‘startling revelation’ and I would take note of the jargon for use when talking to other mathematicians.
Here’s an example of what Doug Hofstadter writes in I Am A Strange Loop. Kurt Goedel discovered that Principia Mathematica by Bertrand Russell does provide reference to itself. So Russell in his book yields the propositions and their proofs, and then Goedel assigns specific numbers to proofs and therefore proves that there is a proof that they are in fact, provable
Outside of mathematics, a statement that is provable is also disprovable. Then it’s called a hypothesis.
I’m reminded of the joke where an engineer, a physicist, and a mathematician are going to a job interview. The interviewer has rigged a fire to start in the wastepaper basket, to see how they react in a crisis situation. The engineer sees the fire, sees the water cooler, grabs the water cooler and dumps it on the fire. The physicist sees the fire, sees the water cooler, grabs pencil and paper, calculates the exact amount of water needed to extinguish the fire, then pours that amount of water into the basket, exactly extinguishing the fire. The mathematician sees the fire, sees the water cooler, and says, “Ah! A solution exists!”.