Things like the various Type Theories appear to be based on replacement rules of one kind or another.
This got me thinking, what would be the simplest set of replacement rules (maybe even just one rule like one axiom boolean logic) which is complicated enough to be interpreted as mathematics.
(The encoding of mathematics in these strings needn't be obvious).
I wonder if this would in any way be related to a Universal Turing machine, because presumably a such a machine could calculate expressions in mathematics.
Or would it be like Rule 110 cellular automata. Could we not use this and encode Type Theory, for example, into 1's and 0's and use this as a basis of Mathematics? This would make the replacement rules simple, but the axioms of the theory would have to be present in the propositions. Whilst maybe Type Theory, the axioms are apparent in the replacement rules themselves?
In other words, one could say "Type Theory is a basis of mathematics" and then have extra axioms for arithmetic etc. But can't one also just say "Rule 110 is the basis of mathematics" but then have extra axioms which define Type Theory?