Dependency tree of elementary arithmetic and algebra

Question

I'm not sure if this violates site policies, but I'd like to ask this question through a small tought experiment.

Imagine we have a blank-slate meta-machine capable of understanding natural language in the same manner humans do as well. Think of it as a small child on steroids.

What would be the necessary topics we would have to model within this machine, and the order in which we would have to model them, so that we would endow it with the capability to perform elementary arithmetic and understand elementary algebra.

Sorry for the inaccurate description. I was refering to a machine with no other prior knowledge or understanding of the outside world, yet the capability to understand natural language. Basically I wanted to disregard the form in which information is fed into the machine, and simply look at the actual concepts that would lay the foundation of the two topics. — Rimio, Sep 27 '19 at 10:11
In my opinion, this question is not really about mathematics, at least as defined by the site guidelines. It might be appropriate on [philosophy.se], though the formulation seems pretty nebulous to me, and I am not sure that it would receive a very warm welcome there, either. — Xander Henderson, Sep 27 '19 at 17:23

score 0 · Accepted Answer · answered Sep 27 '19 at 09:01

Indeed, mathematicians are currently doing this --- they're formalizing large chunks of mathematics in "proof assistants": computer programs which can verify proofs. Examples of such tools include Coq and LEAN

You can take a look at mathematical components, a project which formalised the Fiet-Thompson theorem from group theory (and more results) in Coq. They have an interactive graph of concepts that they have formalized.
There is also a recent formalization of a perfectoid space in LEAN. This concept was used in Peter Schloze's work --- that's all I know about them. There is a nice diagram at the link which shows the vast amount of mathematics they had to formalize to get to this point.

Inside these projects, you can find formalizations of elementary arithmetic, usually starting from the Peano axioms for natural numbers.

Thank you, this is a step in the right direction for me to find an answer! — Rimio, Sep 27 '19 at 10:13
You're welcome! If you can ask a more precise question, I might be able to provide a more precise answer, since I study in this space :) — Siddharth Bhat, Sep 27 '19 at 17:22

Dependency tree of elementary arithmetic and algebra

1 Answers1