Skip to main content
MathOverflow

Return to Question

Became Hot Network Question
Proofreading
Source Link
LSpice
LSpice
  • 12.9k
  • 4
  • 45
  • 69

Are there "typical" formal systems that have mutual constencyconsistency proofs? How long a chain of these can we build?

Sufficiently powerful theories (Peano arithmetic, ZFC, and so on -— this question came from thinking about Coq) can't prove their own consistency. However, are there cases of two theories, $A$ and $B$, where $A$ proves $B$ is consistent and $B$ proves $A$ is consistent? (To make up a potential example, "Peano arithmetic proves ZFC is consistent, and ZFC proves Peano arithmetic is consistent".) If so, are there long chains of these sorts of proofs we can build, so that, if any of $k$ theories waswere inconsistent, all of them would be?

(The context here is idle curiosity about whether we can get in-practice reassurances about our theories by noting that many separate systems would need to have "bugs" at once.)

Are there "typical" formal systems that have mutual constency proofs? How long a chain of these can we build?

Sufficiently powerful theories (Peano arithmetic, ZFC, and so on - this question came from thinking about Coq) can't prove their own consistency. However, are there cases of two theories, $A$ and $B$, where $A$ proves $B$ is consistent and $B$ proves $A$ is consistent? (To make up a potential example, "Peano arithmetic proves ZFC is consistent, and ZFC proves Peano arithmetic is consistent".) If so, are there long chains of these sorts of proofs we can build, so that, if any of $k$ theories was inconsistent, all of them would be?

(The context here is idle curiosity about whether we can get in-practice reassurances about our theories by noting that many separate systems would need to have "bugs" at once)

Are there "typical" formal systems that have mutual consistency proofs? How long a chain of these can we build?

Sufficiently powerful theories (Peano arithmetic, ZFC, and so on — this question came from thinking about Coq) can't prove their own consistency. However, are there cases of two theories, $A$ and $B$, where $A$ proves $B$ is consistent and $B$ proves $A$ is consistent? (To make up a potential example, "Peano arithmetic proves ZFC is consistent, and ZFC proves Peano arithmetic is consistent".) If so, are there long chains of these sorts of proofs we can build, so that, if any of $k$ theories were inconsistent, all of them would be?

(The context here is idle curiosity about whether we can get in-practice reassurances about our theories by noting that many separate systems would need to have "bugs" at once.)

Source Link
krzysz00
krzysz00
  • 161
  • 3

Are there "typical" formal systems that have mutual constency proofs? How long a chain of these can we build?

Sufficiently powerful theories (Peano arithmetic, ZFC, and so on - this question came from thinking about Coq) can't prove their own consistency. However, are there cases of two theories, $A$ and $B$, where $A$ proves $B$ is consistent and $B$ proves $A$ is consistent? (To make up a potential example, "Peano arithmetic proves ZFC is consistent, and ZFC proves Peano arithmetic is consistent".) If so, are there long chains of these sorts of proofs we can build, so that, if any of $k$ theories was inconsistent, all of them would be?

(The context here is idle curiosity about whether we can get in-practice reassurances about our theories by noting that many separate systems would need to have "bugs" at once)