Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Finite axiomatizability of a Theory

  1. Jul 5, 2012 #1
    Hello to everyone,

    I would like to ask what does it mean that a theory is NOT finitely axiomatizable? What are the pleasant and unpleasant consequences of that?
  2. jcsd
  3. Jul 6, 2012 #2
    It means that there is no finite axiomatization of that theory. In general, if T is an L-theory, then T' is an axiomatization of T if T and T' prove the same L-sentences. T is finitely axiomatizable if there's a T' that is finite.

    For example, the theory of infinite sets is not finitely axiomatizable.
  4. Jul 6, 2012 #3


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    You mean, presumably, that ZFC is not finitely axiomatizable.

    NBG, however, is finitely axiomatizable.. So is ETCS (elementary theory of the category of sets), I believe.
  5. Jul 7, 2012 #4
    Specifically, I was referring to 34 part b. on the below problem set. [tex]T_\infty = \{ \exists x_1 \ldots \exists x_n \bigwedge _{1 \le i < j \le n} (x_i \ne x_j) \} _{n \in \mathbb{N}}[/tex] seemed to be axiomatizing infinite sets (it defines infinitely many distinct elements), but I might be wrong. In any case, it is any example of a theory that is not finitely axiomatizable.

    http://www.math.ucla.edu/~anush/UCLA%20Summer%20School%202012/problems.pdf [Broken]
    Last edited by a moderator: May 6, 2017
  6. Jul 7, 2012 #5


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    Ah, I guessed wrongly what you were alluding to. A models of that theory is indeed the same thing as an infinite set.

    TMK, finite axiomatizability is not actually an interesting condition -- instead the thing you want to consider is if there is an axiomatization for which there is an algorithm for enumerating the axioms.

    The existence of such an algorithm would, for example, imply the existence of an algorithm that enumerates all proofs that can be done in the theory, which in turn implies the existence of an algorithm which enumerates all theorems of the theory.

    Proof theory and formal syntax are very closely tied to topics in the theory of computation, by way of the existence of such algorithms.
  7. Jul 7, 2012 #6
    What I had in mind was about computation related subjects, like the one you mention about enumerating all proofs. So, it has to do with the "power" of the theory too? Has it to do with noncompleteness too? For example, if you give a theorem to a not finitely axiomatizable theory it may be not able to give a proof (or a proof of the negation of the theorem)?
  8. Jul 7, 2012 #7


    User Avatar
    Science Advisor

    For proof related computation, you should check out languages like Prolog.


    There are implementations out there to download and if you are interested in computational proof mechanisms in an applied sense, you'll get a lot of benefit out of it.
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook