3 ms·

>"what is a true statement" and "what is a derivable statement" should be the same. you mention completeness in the rest of your comment, so I'm not sure how y

>"what is a true statement" and "what is a derivable statement" should be the same. you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1] [1] https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theorems https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...

chowells 2mo ago
That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent. Truth is some sort of value judgment that is outside the scope of formal systems. And looking at how bizarre Gödel statements are, it's unclear if there's any particular justification for declaring them to be true or false.
- j16sdiz 2mo ago
  err... There are always more ---> you can't make it "compete" by adding finite number of axioms
  - cyphar 2mo ago
    You can make it complete, it just won't be consistent. In fact there is a simple way to do it -- add contradictory axioms and then you can use the principle of explosion to prove any statement as true. Is such a system inconsistent and thus useless? Yes, but it is complete.
- logicallee 2mo ago
  The second paragraph of my link talks specifically about truth: >The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e. an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.
- nextaccountic 2mo ago
  The type theory of Lean is certainly rich enough though

chowells 2mo ago

That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent. Truth is some sort of value judgment that is outside the scope of formal systems. And looking at how bizarre Gödel statements are, it's unclear if there's any particular justification for declaring them to be true or false.

j16sdiz 2mo ago
err... There are always more ---> you can't make it "compete" by adding finite number of axioms
- cyphar 2mo ago
  You can make it complete, it just won't be consistent. In fact there is a simple way to do it -- add contradictory axioms and then you can use the principle of explosion to prove any statement as true. Is such a system inconsistent and thus useless? Yes, but it is complete.
logicallee 2mo ago
The second paragraph of my link talks specifically about truth: >The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e. an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.
nextaccountic 2mo ago
The type theory of Lean is certainly rich enough though