# Is there an analysis of the creation of axioms for a mathematical structure as a computational problem?

Historically, what has happened is the following:

1. There is a "mechanical" structure, most importantly, arithmetic, which operates according to a set of well-defined rules that a stupid computer can easily follow. e.g. a computer can easily calculate $5349\cdot 5345=...$

2. There is a "mechanical" proof-system, most importantly, first order logic, which also operates according to well-defined rules that a stupid computer can follow. e.g. a computer can easily apply derivation rules to go from $\forall x \phi(x)$ to $\exists x \phi(x)$, etc.

3. Then there is a non-mechanical "creative" human, who uses his badly-understood "natural insight" to formulate a set of "axioms about arithmetic", which are words in (2)'s language "about" the operations of (1)'s arithmetic computations. He also formulates a set of "logical axioms", the rules by which the mechanical proof system should operate. He chooses these rules because his intuitive insight says that they are "obviously correct".

It seems to me that this third element in the chain (though it happens first chronologically), is always done in an ad-hoc way. But the fact that this has always been done this way so far, doesn't mean that it necessarily has to be this way.

My question is: Has there been an analysis of the creation of axioms as a computational problem? That is, of the problem of choosing axioms about some mathematical structure, for use in a logic-language?

This computational problem is essentially: given e.g. the rules of arithmetic, find a first-order statement that we can use as an axiom to then derive further properties.

ps. I know that this is a vague question. I am simply asking whether someone has analysed this problem in some way.

• What sort of requirements do you have for 'axiom creation'? Do you want to minimize the number of axioms? Select axioms from a big list? I'm not sure how you think such a task should be evaluated, which is required if you want to phrase the task as a computational problem. – Discrete lizard Apr 9 '18 at 15:15
• @discretelizard, I'm sure you know how people evaluate whether their axiomatization is good or not: 1. Are the axioms true in the desired structure. 2 do they imply a large amount of other true statements. 3. Are they compact. – user56834 Apr 9 '18 at 16:40
• Well, I can't read minds, now can I. Aren't axioms true by definition? So why have point 1? Furthermore, a 'large amount' is rather imprecise, as is "compactness" (I think?) in this case. Anyway, I agree with you that it is vague. I think the only answer that would work here would be one providing literature on this, if such literature exists. Perhaps you should specify that further. – Discrete lizard Apr 9 '18 at 16:45
• @discretelizard. Sorry, I shouldn't have suggested you could have read my mind. To answer your question: An axiom is not true by definition. An axiom is true by virtue of the characteristics of the underlying mathematical structure. E.g. arithmetic is basically defined by a set of rules of how to do operations on numbers (addition, multiplication). but yeah the only real answer would be one that points to some literature. I don't know anything about that literature so I'm gonna leave it open to whomever knows more about this. – user56834 Apr 9 '18 at 17:21
• Where did you get your definition of 'axiom'? I've never seen a definition or usage of 'axiom' such that it isn't 'true' by definition. – Discrete lizard Apr 9 '18 at 18:04