3 ms·

Look up automated proofs. This exists. It's largely useless, due to mathematical properties of logic. Every mathematical system has things which are true but ca

by ggggtez 10y ago

Look up automated proofs. This exists. It's largely useless, due to mathematical properties of logic. Every mathematical system has things which are true but can't be discovered from first principals.

leni536 10y ago
> Every mathematical system has things which are true but can't be discovered from first principals. This is not true, see Gödel's completeness theorem [1], which states "... that a deductive system of first-order predicate calculus is 'complete' in the sense that no additional inference rules are required to prove all the logically valid formulas." It basically means that every "true" statements are provable with a good enough deductive system. What you possibly think about is Gödel's first incompleteness theorem [2] which is quite a different statement. It states that in "most" formal systems (that are complex enough to be able to describe natural numbers) there is always a statement A that both A and "not A" are not provable. It basically means that these statements can't be "logically valid", which means that there exist models of the formal system where A is true and models where "not A" is true. [1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th... [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
eru 10y ago
Nah, P vs NP is a bigger factor here. Basically, checking a proof for correctness takes polynomial time in the size of the proof. (Dependending on how you formalize your proofs, that might even be linear.) Coming up with a reasonable sized proof is much harder. But if we had P=NP, then checking and finding a proof would be about equally hard. See eg http://www.scottaaronson.com/papers/philos.pdf http://www.scottaaronson.com/papers/philos.pdf

by ggggtez 10y ago

leni536 10y ago

> Every mathematical system has things which are true but can't be discovered from first principals. This is not true, see Gödel's completeness theorem [1], which states "... that a deductive system of first-order predicate calculus is 'complete' in the sense that no additional inference rules are required to prove all the logically valid formulas." It basically means that every "true" statements are provable with a good enough deductive system. What you possibly think about is Gödel's first incompleteness theorem [2] which is quite a different statement. It states that in "most" formal systems (that are complex enough to be able to describe natural numbers) there is always a statement A that both A and "not A" are not provable. It basically means that these statements can't be "logically valid", which means that there exist models of the formal system where A is true and models where "not A" is true. [1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th... [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

eru 10y ago

Nah, P vs NP is a bigger factor here. Basically, checking a proof for correctness takes polynomial time in the size of the proof. (Dependending on how you formalize your proofs, that might even be linear.) Coming up with a reasonable sized proof is much harder. But if we had P=NP, then checking and finding a proof would be about equally hard. See eg http://www.scottaaronson.com/papers/philos.pdf http://www.scottaaronson.com/papers/philos.pdf