Finite axiomatizability of a Theory

[russel]

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?

 

[markiv]

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.

 

[Hurkyl]

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.

 

[markiv]

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%20Summer%20School%202012/problems.pdf

 

[Hurkyl]

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.

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.

 

[russel]

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)?

 

[chiro]

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.