It’s weird how in common language use saying something is provable is a stronger statement than merely saying it is true. While in mathematical logic it is a weaker statement. Because truth already implies provability. But provability doesn’t imply truth.
See Godel’s incompleteness theorems. For example, consider the statement “For all A, (ZFC proves A) implies A”, encoded into a form judgeable by ZFC itself. If you believe ZFC to be sound, then you believe that this statement is true, but due to Godel stuff you must also believe that ZFC cannot prove it. The reasons for believing ZFC to be sound are reasons from “outside the system” like “it looks logically sound based on common sense”, “it’s never failed in practice”, and “no-one’s found a valid issue”. Godel’s theorems let us convert this unprovable belief in the system’s soundness into true-but-unprovable mathematical statements.
More mundanely, there are tons of “there doesn’t exist” statements in number theory which are very likely to be true based on unrigorous probabilistic arguments, but are apparently very hard to prove. So there are plenty of things which are “very likely true” but unproven. (I get this example from Paul Christiano, who brings it up in relation to ARC’s “heuristic arguments” work. I think Terence Tao also has a post about this?)
I think we understand each other! Thank you for clarifying.
The way I translate this: some logical statements are true (to you) but not provable (to you), because you are not living in a world of mathematical logic, you are living in a messy, probabilistic world.
It is nevertheless true, by the rule of necessitation in provability logic, that if a logical statement is true within the system, then it is also provable within the system. P → □P. Because the fact that the system is making the statement P is the proof. Within a logical system, there is an underlying assumption that the system only makes true statements. (ok, this is potentially misleading and not strictly correct)
This is fascinating! So my takeaway is something like: our reasoning about logical statements and systems is not necessarily “logical” itself, but is often probabilistic and messy. Which is how it has to be, given… our bounded computational power, perhaps? This very much seems to be a logical uncertainty thing.
It’s weird how in common language use saying something is provable is a stronger statement than merely saying it is true.
While in mathematical logic it is a weaker statement.
Because truth already implies provability.
But provability doesn’t imply truth.
??? For math this is exactly backward, there can be true-but-unprovable statements
Then how do you know they are true?
If you do know then they are true, it is because you have proven it, no?
But I think what you are saying is correct, and I’m curious to zoom in on this disagreement.
See Godel’s incompleteness theorems. For example, consider the statement “For all A, (ZFC proves A) implies A”, encoded into a form judgeable by ZFC itself. If you believe ZFC to be sound, then you believe that this statement is true, but due to Godel stuff you must also believe that ZFC cannot prove it. The reasons for believing ZFC to be sound are reasons from “outside the system” like “it looks logically sound based on common sense”, “it’s never failed in practice”, and “no-one’s found a valid issue”. Godel’s theorems let us convert this unprovable belief in the system’s soundness into true-but-unprovable mathematical statements.
More mundanely, there are tons of “there doesn’t exist” statements in number theory which are very likely to be true based on unrigorous probabilistic arguments, but are apparently very hard to prove. So there are plenty of things which are “very likely true” but unproven. (I get this example from Paul Christiano, who brings it up in relation to ARC’s “heuristic arguments” work. I think Terence Tao also has a post about this?)
I think we understand each other! Thank you for clarifying.
The way I translate this: some logical statements are true (to you) but not provable (to you), because you are not living in a world of mathematical logic, you are living in a messy, probabilistic world.
It is nevertheless true, by the rule of necessitation in provability logic, that if a logical statement is true within the system, then it is also provable within the system. P → □P. Because the fact that the system is making the statement P is the proof.
Withina logical system, there isan underlying assumptionthat the system only makes true statements.(ok, this is potentially misleading and not strictly correct)This is fascinating! So my takeaway is something like: our reasoning about logical statements and systems is not necessarily “logical” itself, but is often probabilistic and messy. Which is how it has to be, given… our bounded computational power, perhaps? This very much seems to be a logical uncertainty thing.