Skip to main content
MathOverflow

Return to Question

added 2 characters in body; edited title
Source Link
Daniel Murcia
Daniel Murcia
  • 119
  • 6

Unprovable Undecidable statements in type theory

In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is unprovableundecidable, no element of the type A nor its negation A → ⊥ can be generated. How can be proven that the statement A is unprovableundecidable?

Unprovable statements in type theory

In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is unprovable, no element of the type A nor its negation A → ⊥ can be generated. How can be proven that the statement A is unprovable?

Undecidable statements in type theory

In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is undecidable, no element of the type A nor its negation A → ⊥ can be generated. How can be proven that the statement A is undecidable?

edited tags
Link
YCor
YCor
  • 63.9k
  • 5
  • 187
  • 286
Source Link
Daniel Murcia
Daniel Murcia
  • 119
  • 6

Unprovable statements in type theory

In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is unprovable, no element of the type A nor its negation A → ⊥ can be generated. How can be proven that the statement A is unprovable?