= 27d567bc2d48d9f40e9ccc20ea370b15)
cousin_it 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)
Not much, admittedly :-) The interesting question to me is how to make a computer understand "integers" the way we seem to understand them. It must be possible because humans are not magical, but second-order logic doesn't seem to help much.
Computers can prove everything about integers that we can. I don't see a problem here.
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."
Well, human beings are abductive and computational reasoners anyway. I think our mental representation of the natural numbers is much closer to being the domain-theoretic definition of the natural numbers as the least fixed point of a finite set of constructors.
Note how least fixed-points and abductive, computational reasoning fit together: a sensible complexity prior over computational models is going to assign the most probability mass to the simplest model, which is going to be the least-fixed-point model, which is the standard model (because nonstandard naturals will require additional bits of information to specify their constructors).
A similar procedure, but with a coinductive (greatest-fixed-point) definition that involves naturals as parameters to the data constructors, will give you the real numbers.