generate all possible theories compatible with axioms

Question

I am currently trying to learn about the fundations of mathematical logic, and the incompleteness theorem. I was curious to know if there's a way, given some given axioms, to analyze all the possible theories that are compatible with them.

By "analyze", I mean "say anything that could be interesting", for instance counting how many such theories there are, or automatically generating statements that are true in one of the theories, but false in the other etc...

For instance, given the first 4 axioms of planar geometry, can we automatically deduce that only 3 geometries will be compatible with those axioms (euclidean, spherical and hyperbolic), generate automatically the additional axioms needed to define those geometries, and generate statements that are true in one of the geometries but not the other ?

Even further, given a starting set of axioms, do the allowed theories generated have some sort of structure ? For instance, intuitively I would imagine the possible theories could be organized with a spanning tree, where we branch out by adding different alternative axioms on top of the growing stack of axioms...

By automatically I literally mean using a computer for instance,

I'm just trying to get more intuitions on this area, (at the same time I'm learning more formally to get more into the details of the proofs, formal systems, godel numbering etc)

I'd be really glad to read about any reference about the subject! Particularly with concrete examples using classical axioms systems (like geometry, arithmetic etc)

Thanks a lot,

Answer 1

Your idea that there is a computable tree of possible extensions of a given theory is completely right, in the case of arithmetic.

If we start with any consistent computably axiomatizable theory $T$ of arithmetic (extending a certain sufficient weak theory), then it is a consequence of the Rosser variation of the Gödel incompleteness theorem that there must be a sentence $\rho_T$, the Rosser sentence, that is neither provable nor refutable in the theory. Thus, we may extend the theory in two ways, either by adding the sentence or its negation $$T_0=T+\neg\rho_T\qquad\qquad T_1=T+\rho_T.$$ Each of these theories is a consistent computably axiomatizable theory of arithmetic, a finite extension of the original theory $T$. These new theories $T_s$ therefore have their own Rosser sentences $\rho_s$, and so we may extend to a tree of theories $$T_{s^\frown 0}=T_s+\neg\rho_s\qquad\qquad T_{s^\frown 1}=T_s+\rho_s.$$ In this way, for every binary sequence $s$ we get a theory $T_s$ forming altogether a binary-branching tree of distinct pairwise incompatible consistent theories of arithmetic, each a finite extension of the initial theory $T$. Furthermore, this tree is computable, in the sense that we can compute from any finite sequence $s$ what are the sentences $\rho_{s\upharpoonright n}$ that we had added to form $T_s$.

Every infinite binary sequence $x$ determines a branch through this tree $$T_x=\bigcup_n T_{x\upharpoonright n}$$ and any two such theories will disagree. Thus, there are continuum many distinct consistent theories extending $T$. And the theory $T_x$ is computably axiomatizable from oracle $x$.

You can see an application of this idea on my blog post Every function can be computable!.