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.

  • 1
    $\begingroup$ I believe the text is using the hypothesis that $X$ is consistent to begin with; that is, the point is to characterize the maximal consistent theories amongst all consistent theories. $\endgroup$ Feb 24 at 21:46
  • $\begingroup$ Ah, this could be it. This also clears up the "exactly one" bit. $\endgroup$ Feb 24 at 21:53
  • $\begingroup$ @NoahSchweber I've added the some more context by reproducing the paragraph the quote appears in. It's not obvious to me that the hypotheses of $X$ being consistent is implied here. $\endgroup$ Feb 24 at 22:02
  • $\begingroup$ yes, one needs to assume $X$ is consistent for this to hold. if the author didn't write it explicitly it is an typo/omission $\endgroup$ Feb 26 at 19:25
  • $\begingroup$ Feel free to submit an answer and I'll accept it. $\endgroup$ Feb 27 at 16:28


You must log in to answer this question.