## Finite axiomatizability of a Theory

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?

 PhysOrg.com science news on PhysOrg.com >> 'Whodunnit' of Irish potato famine solved>> The mammoth's lament: Study shows how cosmic impact sparked devastating climate change>> Curiosity Mars rover drills second rock target
 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.

Recognitions:
Gold Member
Staff Emeritus
 Quote by markiv For example, the theory of infinite sets is not finitely axiomatizable.
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.

## Finite axiomatizability of a Theory

Specifically, I was referring to 34 part b. on the below problem set. $$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}}$$ 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...2/problems.pdf

Recognitions:
Gold Member
Staff Emeritus
 Quote by markiv Specifically, I was referring to 34 part b. on the below problem set.
Ah, I guessed wrongly what you were alluding to. A models of that theory is indeed the same thing as an infinite set.

 Quote by russel 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?
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.

 Quote by Hurkyl 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.
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)?

 Quote by russel 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)?
For proof related computation, you should check out languages like Prolog.

http://en.wikipedia.org/wiki/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.

 Tags axiomatizable