Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

>If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.

Huh? How? Truth is an empirical fact, you can't possibly define it into existence.



You have a point, but to be fair the person you replied to didn't use the word "truth". They said "valid mathematical proof". An in the context of type theory or formal logic "valid proof" is indeed something that has been "defined into existence" (in type theory "valid proof" ≈ "well-typed term"). Whether it represents "truth" is a different matter. Though such systems can (ideally) be proven sound in and with respect to "normal" mathematics. At that point I guess the "truth"ness depends on you overall belief in math :)


All mathematical "truths" are defined into existence as you call it. All mathematical proofs are essentially of the form If A Then B. B is only a "truth" since we defined A a certain way and accept it as True. Due to its very nature, there are no empirical facts in mathematics.

You can argue that the is no Truth is mathematics, which is a perfectly reasonable position to take.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: