undefined | Better HN

0 pointsmturmon5y ago0 comments

One of the usual examples given in reaction to this question is the puzzle of Euclid's 5th postulate, the parallel-lines postulate. People tried for centuries to prove that it could be deduced from the other axioms. Turned out, it was independent of the others.

A proof system could identify cases where you need hidden assumptions in order to make proofs. In this case, you would get a null result from the oracle, which would be valuable in itself.

[1] https://en.wikipedia.org/wiki/Parallel_postulate

0 comments

roywiggins5y ago

At best an proof-checker can invalidate a purported proof, it absolutely is not going to prove that no proofs are valid (it would have to affirmatively prove that the result is actually independent of the axioms you picked, which is a lot harder)

mturmonOP5y ago

Many incorrect proofs of this postulate were given over the years. (For instance, in some cases these erroneous proofs have steps that implicitly use the postulate itself.)

The proof checker could detect such errors in a purportedly clean proof.

j / k navigate · click thread line to collapse