= 27d567bc2d48d9f40e9ccc20ea370b15)
Darmani comments on Completeness, incompleteness, and what it all means: first versus second order logic - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (38)
If the human and the computer are using the same formal system, then sure. But how does a human arrive at the belief that some formal system, e.g. PA, is "really" talking about the integers, and some other system, e.g. PA+¬Con(PA), isn't? Can we formalize the reasoning that leads us to such conclusions? Pointing out that PA can be embedded in some larger formal system, e.g. ZFC, doesn't seem to be a good answer because that larger formal system will need to be justified in turn, leading to an infinite regress. And anyway humans don't seem to be born with a belief in ZFC, so something else must be going on.
We form beliefs about mathematics the same way we form beliefs about everything else: heuristic-based learning algorithms. We typically accept things based on intuition and inductive inference until trained to rely on proof instead. There is nothing stopping a computer from forming mathematical beliefs based on statistical inference rather than logical inference.
Have a look at experimental mathematics or probabilistic number theory for some related material.
Saying "heuristic-based learning algorithms" doesn't seem to compress probability mass very much. It feels like skipping over the mysterious part. How exactly do we write a program that would arrive at the axioms of PA by using statistics? I think if we did that, then the program probably wouldn't stop at PA and would come up with many other interesting axioms, so it could be a useful breakthrough.
Yes, but the point is that we are learning features from empirical observations, not using some magic deduction system that our computers don't have access to. That may only be one bit of information, but it's a very important bit. This skips over the mysterious part in the exact same way that "electrical engineering" doesn't answer "How does a CPU work?" -- it tells you where to look to learn more.
I know far less about empirical mathematics than about logic. The only thing along these lines I'm familiar with is Douglas Lenat's Automated Mathematician (which is only semi-automated). A quick search for "automated mathematician" on Google Scholar gives a lot of more recent work, including a 2002 book called "Automated theory formation in pure mathematics."