I've recently become interested in the way that mathematical theorems can start from a very basic set of axioms and, through clever logic, be proven. I'm interested in knowing more about the reverse process. That is, given a set of axioms and the rules of (first order?) logic, derive theorems that are true, even if they are "uninteresting".
For concreteness, let's assume I have only the following two axioms for defining operations on a set of symbols:
- There is a unique symbol, * in the set
- There is an operation, @, defined so that, for any symbol o in the set $ *@o = o@* = p$ is a new symbol that is also in the set
What additional structure would I need in order to expand this (and similar) axiomatic systems into rich sets of theorems? Is it possible that an internally consistent axiomatic system can be chosen so that no theorems can be derived from it?