4 ms·

I'm really not from the field but wasn't there some Gödel theorem showing every system strong enough cannot show its own consistency?

by xylol 2y ago

peteradio 2y ago
I don't think the system here is trying to prove any of its underlying assumptions, just building on some set of existing ones. I doubt the theorem you are thinking of is applicable.
pulisse 2y ago
The system isn't being used to prove its own consistency. The consistency is proved in a different, stronger system.
hyperpape 2y ago
Gödel's incompleteness theorems are what you're thinking of. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... That said, if you have a system X, it can't prove it's own consistency, but a stronger system Y can prove its consistency (and perhaps some other stronger system can prove Y's consistency. This gives us a chain of systems, each proving the consistency of some weaker system). That doesn't absolutely prove that the system is consistent--if Y was inconsistent, it could prove X is consistent (and also could prove that X is inconsistent). Nonetheless, it is still valuable. After all, part of our use of Y is the fact that we know of no inconsistency in it. And since formal systems often are subtly inconsistent, "consistent assuming some other system is consistent" is a lot better than "we have no proof whatsoever of consistency".
deleted 2y ago
[deleted]
skhunted 2y ago
What’s interesting to note is that even if a strong system could prove its own consistency then it wouldn’t tell you anything. An inconsistent system can prove its own consistency. So if a system has a proof that it is itself consistent then you still wouldn’t know if it is consistent.
- libeclipse 2y ago
  It would tell you that the system is inconsistent
  - skhunted 2y ago
    It would not. If a system can prove (I know sufficiently rich systems can’t do this but suppose it could) its own consistency you still can't conclude it is consistent. EDIT: I'm working under the hypothetical situation in which PA could prove its consistency. I know it can't but assuming that it could prove it's own consistency you still couldn't conclude that it was consistent since an inconsistent system can prove it's consistency.
    - roywiggins 2y ago
      GP is (I think correctly) stating that a system that can "prove" its own consistency is definitely inconsistent. Inconsistent systems can "prove" anything; if a system can appear to prove its own consistency, it isn't.
      - skhunted 2y ago
        Yes. I know this. What I'm saying is that even if a consistent system that was strong enough could prove it's consistency then it still wouldn't tell you anything. There are system that can prove their own consistency for which it is known that they are consistent. https://en.wikipedia.org/wiki/Self-verifying_theories https://en.wikipedia.org/wiki/Self-verifying_theories
        naasking 2y ago
        These are weaker than the systems Godel's theorems are referring to, as discussed in the opening paragraph. Do these systems are not "strong enough" in the sense described in this thread.
        2y ago
francasso 2y ago
You should take this proof as saying: if Lean 4 is consistent then New Foundations is consistent. There is no contradiction of Godel's incompleteness theorem.

I'm really not from the field but wasn't there some Gödel theorem showing every system strong enough cannot show its own consistency?

by xylol 2y ago

I'm really not from the field but wasn't there some Gödel theorem showing every system strong enough cannot show its own consistency?

peteradio 2y ago

I don't think the system here is trying to prove any of its underlying assumptions, just building on some set of existing ones. I doubt the theorem you are thinking of is applicable.

pulisse 2y ago

The system isn't being used to prove its own consistency. The consistency is proved in a different, stronger system.

hyperpape 2y ago

Gödel's incompleteness theorems are what you're thinking of. https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... That said, if you have a system X, it can't prove it's own consistency, but a stronger system Y can prove its consistency (and perhaps some other stronger system can prove Y's consistency. This gives us a chain of systems, each proving the consistency of some weaker system). That doesn't absolutely prove that the system is consistent--if Y was inconsistent, it could prove X is consistent (and also could prove that X is inconsistent). Nonetheless, it is still valuable. After all, part of our use of Y is the fact that we know of no inconsistency in it. And since formal systems often are subtly inconsistent, "consistent assuming some other system is consistent" is a lot better than "we have no proof whatsoever of consistency".

deleted 2y ago

[deleted]

skhunted 2y ago

What’s interesting to note is that even if a strong system could prove its own consistency then it wouldn’t tell you anything. An inconsistent system can prove its own consistency. So if a system has a proof that it is itself consistent then you still wouldn’t know if it is consistent.

libeclipse 2y ago
It would tell you that the system is inconsistent
- skhunted 2y ago
  It would not. If a system can prove (I know sufficiently rich systems can’t do this but suppose it could) its own consistency you still can't conclude it is consistent. EDIT: I'm working under the hypothetical situation in which PA could prove its consistency. I know it can't but assuming that it could prove it's own consistency you still couldn't conclude that it was consistent since an inconsistent system can prove it's consistency.
  - roywiggins 2y ago
    GP is (I think correctly) stating that a system that can "prove" its own consistency is definitely inconsistent. Inconsistent systems can "prove" anything; if a system can appear to prove its own consistency, it isn't.
    - skhunted 2y ago
      Yes. I know this. What I'm saying is that even if a consistent system that was strong enough could prove it's consistency then it still wouldn't tell you anything. There are system that can prove their own consistency for which it is known that they are consistent. https://en.wikipedia.org/wiki/Self-verifying_theories https://en.wikipedia.org/wiki/Self-verifying_theories
      - naasking 2y ago
        These are weaker than the systems Godel's theorems are referring to, as discussed in the opening paragraph. Do these systems are not "strong enough" in the sense described in this thread.
        2y ago

francasso 2y ago

You should take this proof as saying: if Lean 4 is consistent then New Foundations is consistent. There is no contradiction of Godel's incompleteness theorem.