Formalization of an elementary statement in first-order logic First, some motivation for this question. In a finite set $T$ of axioms in a first-order language $L$, we can always join the axioms by conjunction to get a 1-element set of axioms. By this method, we can get a non-redundant set of axioms of the theory generated by $T$. But this method is artificial and unsatisfactory. What we obviously want is for the axiomatization to consist of "elementary" statements. It is this notion of elementary statement that I want to make formal. Obviously, no conjunction can be elementary. But also, something like $((P \land Q) \vee (Q \land P))$ is a "cheating" way to get around this requirement of not being a conjunction. So, what exactly is the proper definition of an elementary statement, a statement that can't be broken down in a non-trivial way?
 A: I think this is a sufficiently vague notion that, while arguably natural, there isn't going to be a single "right way" to set it up. Let me describe, however, a general framework which I think may be fruitful:

The idea is to use a complexity measure on finite sets of formulas. By this I mean a map $\delta: \mathcal{P}_{fin}(Form)\rightarrow W$ for some well-founded partial order $W$, where we interpret $\delta(X)\le \delta(Y)$ as meaning "$X$ is at least as simple as $Y$." I'm being deliberately vague about exactly what I mean here, and certainly there are various basic axioms such a $\delta$ should satisfy (e.g. presumably we should have $X\subseteq Y\implies \delta(X)\le\delta(Y)$), but I don't want to get into that at the moment. I just want to give a high-level impression of what such a thing might do for us here.
For example, we could let $\delta$ be the "sum-of-lengths" function, taking values in $\mathbb{N}$ with the usual ordering. More naturally in my opinion, we could use the measure (also taking values in $\mathbb{N}$) which is implicit in arguments by "induction on formula complexity:" send atomic formulas to $0$, have Booleans and quantifiers increment complexity by $1$, and give a finite set of formulas the same complexity as its conjunction. And there are also approaches which are more context-specific. For example, if we're playing in arithmetic or set theory, the arithmetical or Levy hierarchy (together with some fixed "brute-force" prenexing algorithm) provides such a $\delta$ on individual formulas (which we'd then have to extend to finite sets of formulas) which takes values in a sort of "ladder" partial order: $\Sigma_m$ and $\Pi_m$ are incomparable (excepting that $\Sigma_0=\Pi_0$) but $\Sigma_m>\Pi_n$ and $\Pi_m>\Sigma_n$ whenever $m>n$.
In line with my above-mentioned deliberate vagueness, I don't want to get into the question of which measures are "right" in which contexts. My point in giving the examples above is simply that there are several natural notions of complexity measures floating around already, so it's not like we're introducing a new idea here.
In what follows, fix some $\delta$ which we'll agree measures complexity correctly.
There are two main ways we might measure the complexity of a given finitely axiomatizable theory $T$:

*

*How simple can we make the formulas in an axiomatization of $T$?


*How many sentences do we need to provide an axiomatization of $T$ which can't be "simplified?"
The first of these is easy to formalize - it's just asking for $\min\{\delta(A): A\equiv T\}$, or rather (since $\delta$ takes values in a partial, rather than total, order) for the set of elements of $W$ which equal $\delta(A)$ for some axiomatization $A$ of $T$ and are $W$-minimal with that property. Obviously we'd hope that in "natural" situations we'd get a single element as our answer, and this doesn't seem too unlikely. So let's consider this question more-or-less solved.
The second question is a bit more nuanced, but the following seems satisfactory to me. Say that a finite set $\Gamma$ of first-order formulas is irreducible iff for every $X\subseteq\Gamma$ and every finite set of formulas $Y$ such that $\Gamma\models Y$ and $(\Gamma\setminus X)\cup Y\models X$, we have $\delta(X)\le\delta(Y)$. That is, $\Gamma$ is irreducible if there's no way to take part of $\Gamma$ and reduce its complexity as measured by $\delta$ while keeping the same overall logical strength. Since $\delta$ takes values in a well-founded partial order, "reasonable" hypotheses on $\delta$ will imply that every finite set of formulas is equivalent to an irreducible set. This lets us talk about the essential size of a theory, namely the smallest size of any irreducible finite axiomatization of that theory.
A good test problem for both a particular $\delta$ and this idea as a whole is:

Does essential size $1$ have any particular significance?

Offhand I have no particular thoughts on the matter, but maybe someone else can shed light here.
