Is there a systematic procedure to construct a model of an axiomatic system from the system itself?

For example given the abstract postulates of a ring we can show that the integers satisfies them and hence this is a model. Of course there are many other types of ring and clearly more general models.

I want to know if there is any systematic algorithm or construction that could derived such models automatically, perhaps given knowledge of simpler mathematical objects like the integers, the reals, complex numbers for example.


  1. I'm definitely not expecting an algorithm that works in all circumstances as that is probably impossible like the Halting Problem.

  2. We should not need to assume the axiomatic system is consistent a model can still exist even if the system is inconsistent.

  3. An algorithm that works for a restricted class of axiomatic systems would be interesting.

  • 1
    $\begingroup$ en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem $\endgroup$ – Matt F. Nov 6 '19 at 12:02
  • 3
    $\begingroup$ A model can still exist even if the system is inconsistent --- you sure about that? Anyway, Google "model existence theorem". $\endgroup$ – Nik Weaver Nov 6 '19 at 12:03
  • 1
    $\begingroup$ A structure with given properties may or may not exist, but there is no such thing as an inconsistent structure. Consistency is a property of axiomatic systems, not of structures. Also, the completeness theorem applies to arbitrary first-order theories, see en.wikipedia.org/wiki/… . $\endgroup$ – Emil Jeřábek 3.0 Nov 6 '19 at 13:50
  • 2
    $\begingroup$ I have no idea what that question even means. Algorithms deal with finite strings (and other finite objects that can be encoded as finite strings). Models of interesting theories are usually infinite. $\endgroup$ – Emil Jeřábek 3.0 Nov 6 '19 at 14:06
  • 2
    $\begingroup$ @IvanMeir. Models can't be inconsistent, that expression has no meaning. Also I think your understanding of "first order logic" is faulty --- e.g., ZFC is a first order theory. So yes, it is applicable to all of mathematics. $\endgroup$ – Nik Weaver Nov 6 '19 at 14:40

A simple example for a restricted class is free algebras. Given a set of equations in a functional type (no relation symbols other than standard equality), one can construct the term algebra using the function symbols and variable symbols, and then construct congruence relations induced by identifying the left hand side with the right hand side of an equation. (Iterate this over the computable set of equations.) You always get a model, which may be the trivial one element model, from the quotient of the term algebra by the (equivalence relation determined from the) set of induced equivalence relations.

Gerhard "Is This A Good Example?" Paseman, 2019.11.06.

  • $\begingroup$ Thank you Gerhard for this example. This is what I was interested in seeing - examples of axiomatic systems where there was a procedure for generating a model. I like this as it seems analogous to solving a polynomial equation by quotienting out the polynomial ring by the polynomial and in my mind I think of models as "solutions" of the axiomatic system. $\endgroup$ – Ivan Meir Nov 6 '19 at 18:53
  • $\begingroup$ The process is a little more complicated than what I describe, but the idea is there, and should serve as motivation for studying the completeness theorems and other systems. Note that in order for it to be properly algorithmic, you need to restrict to finite or recursive presentations and to expand your notion of constructing from finite to infinite objects. You might check out subjects in algorithmic algebra, e.g. computational group theory. Gerhard "Can Groups Have Undo Buttons?" Paseman, 2019.11.06. $\endgroup$ – Gerhard Paseman Nov 6 '19 at 20:40
  • $\begingroup$ Thanks again Gerhard your advice is welcome and appreciated, Ivan $\endgroup$ – Ivan Meir Nov 7 '19 at 12:54

Not the answer you're looking for? Browse other questions tagged or ask your own question.