This is a question about Gentzen calculus. $X$ is a set of formulas with the symbols $\{\lnot, \land\}$, and $a$ is such a formula.
On page 27 of "A Concise Introduction to Mathematical Logic" by Rautenberg, it states:
it easily follows that $X$ is maximally consistent iff either $a \in X$ or $\lnot a \in X$, for each $a$.
Firstly, the text surely means exactly one of $a \in X$ or $\lnot a \in X$, otherwise if both $a, \lnot a \in X$, then $X$ is not consistent.
Now, I tried to formalize this statement in Lean, and was able to formalize the forward $(\to)$ direction. The reverse direction, however, has been difficult, and I'm convinced it's incorrect as stated. I was able to prove half of the reverse direction ($\leftarrow$): $(\forall a$, exactly one of $a \in X$ or $\lnot a \in X) \to \forall X' \supset X, X'$ is inconsistent. (In fact, the "exactly one" bit is not actually required for this half). However, I cannot prove that $(\forall a$, exactly one of $a \in X$ or $\lnot a \in X) \to X$ is consistent. I believe this half of the reverse direction to be false.
If we have $X = \{a : a \text{ has an even number of $\lnot$ as a prefix}\}$, then we have $\forall a$, exactly one of $a \in X$ or $\lnot a \in X$. However, we have that $(a \land \lnot a) \in X$, and therefore $X$ is inconsistent.
Is this a valid counterexample? If not, what am I missing here? If so, what did the text likely mean to say?
Here is the full context of the quote:
The inconsistency of $X$ can be identified by the derivability of a single formula, namely $\bot (=p_1 \land \lnot p_{1})$, because $X \vdash \bot$ implies $X \vdash p_1, \lnot p_1$ by $(\land 2)$, hence $X \vdash a$ for all $a$ by $(\land 1)$. Conversely, when $X$ is inconsistent then in particulyar $X \vdash \bot$. Thus, $X \vdash \bot$ may be read as '$X$ is inconsistent', and $X \not\vdash \bot$ as '$X$ is consistent'. From this it easily follows that $X$ is maximally consistent iff either $a \in X$ or $\lnot a \in X$ for each $a$. The latter is necessary, for if $a$, $\lnot a \notin X$ then both $X$, $a \vdash \bot$ and $X$, $\lnot a \vdash \bot$, hence $X \vdash \bot$ by $(\lnot 2)$. This contradicts the consistency of $X$. Sufficiency is obvious.