zlacker

I'm not convinced by Cyc either, but this argument is a bit off. A system like this would need to define axioms and inference rules. But it wouldn't need to collect upfront a database of every possible inference which might be made from them.

(In mathematics you don't technically need very many axioms or inference rules, although you do need a large body of heuristics and hints if you want a proof system which confines itself to proving inferences that are actually useful in some sense of the word, rather than proving a combinatorial explosion of trivial theorems. Dealing with the body of elementary arithmetic problems, however, wouldn't necessarily be particularly intractable -- last time I checked software proof systems can already deal with proving theorems in areas of mathematics like this and a fair bit further.)

>>mjw+(OP)
Maths is a self-consistent and closed system. From that point of view, the nature of axioms is irrelevant. You can have an unlimited kinds of axiomatic systems, each consistent and each explanatory in its own way. What is a theorem in one system can be treated as an axiom in the next as long as the system itself leads to no contradictions.

Given that human knowledge encompasses more than one axiomatic system, it would be foolish to endow a system designed to replicate human knowledge with an immutable set of axioms.

Please watch this presentation of Richard Feynman on the nature of maths and physics: http://www.feynmanphysicslectures.com/relation-of-mathematic...