Proof of consistency of proof system syntactically.

Question

I am trying to prove the "only one" part of the problem.

Let $A$ be a set of propositional symbols, $\alpha$ ba a WFF over $A$ and $M\subseteq A$. And let $M^+: = M \cup \{(\neg a): a\in (A-M)\}$. Then, only one of $M^+ \vdash \alpha$ or $M^+ \vdash \neg \alpha$ are true.

• $M^+\vdash \alpha$ means that there are exists a sequence $\Sigma$ of elements of $M^+$ such that $\Sigma \vdash \alpha$ is provable.

It seems to be almost the same as proving the consistency of the proof system. I want to prove this purely syntactically. I will copy here the proof system in my logic textbook. For convenience, assume $\neg$ and $\wedge$ are the only connectives. From now, Let $\Sigma $ be a sequence of WFF, $\alpha, \alpha_1,\alpha_2$ be a WFF and $\cdot$ is sequence concatenation.

axioms: $\Sigma \vdash \alpha$ iff $\alpha$ occurs in $\Sigma$

FI: $\dfrac{\Sigma \vdash \alpha, \ \Sigma \vdash (\neg\alpha) }{\Sigma \vdash ⊥}$

NI: $\dfrac{\Sigma\cdot \alpha\vdash ⊥ }{\Sigma \vdash (\neg \alpha)},\quad $ NE: $\dfrac{\Sigma\cdot (\neg \alpha) \vdash ⊥ }{\Sigma \vdash\alpha}$

CI:$\dfrac{\Sigma \vdash \alpha_1, \ \Sigma \vdash \alpha_2 }{\Sigma \vdash (\alpha_1\wedge \alpha_2)},\quad $ CE: $\dfrac{\Sigma \vdash (\alpha_1\wedge \alpha_2)} {\Sigma \vdash \alpha_1, \ \Sigma \vdash \alpha_2 }$

and assumption transformation rules:

EX : $\dfrac{\Sigma\vdash \alpha}{\Sigma\cdot \beta \vdash \alpha},\ $ DL : $\dfrac{\Sigma\cdot \beta\cdot \beta \vdash \alpha}{\Sigma\cdot \beta \vdash \alpha},\ $ RO : $\dfrac{\Sigma_1\cdot \beta_1\cdot \beta_2 \cdot \Sigma_2 \vdash \alpha}{\Sigma_1\cdot \beta_2\cdot \beta_1 \cdot \Sigma_2 \vdash \alpha}$

I tried to use induction. So I tried to prove the following proposition by induction on $n$.

There is no derivation that satisfies both of the following two properties.

(a): $\Sigma$ is a sequence of elements of $M^+$, $\pi_1$ and $\pi_2$ are derivations of $\Sigma\vdash \alpha$ and $\Sigma\vdash (\neg\alpha)$ respectively.

(b): $\max(|\pi_1|, |\pi_2|)=n$

The base case is easy. But I failed in the proof of induction step. For example, if the last step of $\pi_2$ is obtained by NI, the previous step will be $\Sigma\cdot \alpha \vdash ⊥$, and before that it will be $\Sigma\cdot\alpha \vdash \beta $ and $\Sigma\cdot\alpha \vdash \neg\beta$. But in my opinion, this is not a contradiction with the induction hypothesis. Because in general, $\Sigma\cdot\alpha$ is "NOT" a sequence of elements of $M^+$(Because $\alpha$ is not an element of $M^+$.).

Please help me with this problem.

Answer 1

Since you have the $\bot$ connective, we can define consistency to mean $\nvdash\bot$. You can also easily derive $\dfrac{\Sigma\vdash\bot}{\Sigma\vdash\beta}$ for any formula $\beta$. (How?)

FI immediately implies that deriving $\Sigma\vdash\alpha$ and $\Sigma\vdash\neg\alpha$ means $\Sigma\vdash\bot$ is derivable, and as stated above $\Sigma\vdash\bot$ implies both of $\Sigma\vdash\alpha$ and $\Sigma\vdash\neg\alpha$. You can therefore simplify to just showing that $\Sigma\vdash\bot$ is not derivable. Of course, given EX, this immediately means that $\vdash\bot$ can't be derivable, i.e. that the logic needs to be consistent.

Unfortunately this doesn't help that much because of the FI rule (and to a lesser extent the NE rule). The problem is that the proof system you've presented lacks the subformula property. That is, some rules have formulas above the line which need not occur below the line. In particular, the only rules with this issue are FI and NE. The problem the lack of the subformula property causes becomes evident when we attempt a structural induction on derivations. We'd like to prove that there is no derivation ending in $\vdash\bot$ (e.g. for the $M=\varnothing$ case). The only possible rule that could end such a derivation is FI. Unfortunately, FI instantiated with any formula $\alpha$ would work, and we then need to generalize our induction hypothesis greatly because we now have to show that we can't derive both of $\vdash\alpha$ and $\vdash\neg\alpha$ for all formulas. The issue with NE isn't quite as bad, but it's still inconvenient that $\neg\alpha$ is not in any way "simpler" than $\alpha$.

When we look at LK, the equivalent for $\vdash\bot$ is $\cdot\vdash\cdot$ where $\cdot$ indicates an empty sequence of formulas. We can look and see that there is simply no rule that will produce an empty sequence of conclusions except for Cut which is the only rule that violates the subformula property. Gentzen's Hauptsatz is that Cut isn't necessary.¹ In general, the subformula property helps us to avoid needing to "guess" an arbitrary formula during an induction on derivations. The proof of the Hauptsatz is pretty gnarly, though it's clear enough what it is doing: we just show that every use of Cut in a derivation can be moved closer to the leaves. Eventually the Cut will encounter Id where it can be trivially eliminated. The devil is definitely in the details here. You need a rather complicated pattern of inductions (corresponding to a transfinite induction), and Gentzen actually introduces a "multi-cut" rule and eliminates that instead due to difficulties with the contraction rule. The procedure implicitly being described is very non-deterministic because the cases are not all mutually exclusive.

Using much more modern techniques coming from linear logic, particularly polarization and focusing, we can formulate proof systems that have a lot less non-determinism both in proof search and in the cut-elimination procedure as described in the technical report On focusing and polarities in linear logic and intuitionistic logic by Liang and Miller. We can also simplify the proof of cut-elimination a bit, e.g. by eliminating the need for a "multi-cut". The technical report referenced includes most of a proof for cut-elimination for the system LJF which is a focused form of Gentzen's intuitionistic LJ. It also briefly touches on the adaptations that would be needed for a (direct) cut-elimination proof for LKF, a focused form of LK which is embeddable into LJF. A direct proof for LKF would be shorter than one for LJF since LKF requires fewer connectives.

Both Gentzen's original proof and the more modern one for LJF span several pages. The multiple inductions over derivations leads to a large number of cases. I'd have to recheck Gentzen's proof, but I believe both hand-wave many cases as being similar, and don't spell them out. For intuitionistic propositional logic (IPL), this appears to be a a formulation of a syntactic cut-elimination proof in Coq. A proof of cut-elimination LJ and LK in the proof assistant Elf is presented A Structural Proof of Cut Elimination and Its Representation in a Logical Framework by Pfenning. Pfenning's proof has the nice properties of being 1) mechanized, 2) relatively short for a completely mechanized proof², 3) formulated with just three nested structural inductions, 4) not requiring finite (multi-)sets, and 5) executable, i.e. it can actually produce cut-free derivations from derivations using Cut. One potential downside is that it uses a higher-order representation of derivations which is almost certainly crucial to the proofs relative simplicity.

There's a common theme in all of these of moving to a more tractable proof system. The sequent calculus itself (LK and LJ) was introduced to understand natural deduction (NK and NJ) also introduced by Gentzen. Natural deduction, as the name suggests, is indeed more natural to use than the sequent calculus.

All of the proofs mentioned are fairly complicated. As mentioned, the conceptual idea isn't too complicated but there are a large amount of details. This is pretty common in (structural) proof theory.³ (To be fair, a full spelling out of a completeness proof is not usually very short either.) That said, there is a significant savings in the meta-logical assumptions as compared to a typical semantic proof for first-order logic. For classical propositional logic, this is not so much the case since we can think of truth-table semantics syntactically.

¹ If you wanted to just leverage the work Gentzen has already done, you could (syntactically) show that each derivation in this system has a corresponding derivation in LK and vice versa. "Corresponding" would mean that if you go from one side and back, you get a derivation for a provably equivalent formula. To be precise, we only need to be able to go to LK and back and produce an provable equivalent formula. This can be viewed as half of an equivalence of categories where we view $\vdash$ as a preorder. (It would be a bit more natural to decategorify a notion of an equivalence of multicategories.)

² Most of the work is in a proof of the admissibility of Cut ca' that is spread over several pages, but that is with each rule having a (mechanically generated) informalization also presented. In general, the informal presentation is less concise than the formal presentation so this more than doubles the size.

³ In fact, LF, the logic behind Elf, was specifically motivated to deal with the high amount of tedious complexity these kinds of proofs present.

Answer 2

The argument is by induction/recursion on the proofs of $\Sigma\vdash\alpha$ ($\Sigma\vdash\lnot\alpha$).

Suppose $M^+\vdash\alpha$. I show that $M^+\not\vdash\lnot\alpha$ (the other direction is analogous).

Let's assume, for a contradiction, that $M^+\vdash\lnot\alpha$. Then, there is a sequence $\Sigma$ of elements from $M^+$ such that $\Sigma\vdash\lnot\alpha$ is provable. Consider any such proof. Disregarding the assumption transformation rules, the conclusion $\Sigma\vdash\lnot\alpha$ could have been obtained by applications of either CE, NI or NE. The cases where it was obtained by CE lead (through CI) inevitably to the two other cases, NI or NE. Furthermore, both NI and NE lead, through the second premiss of FI to $\Sigma\cdot\alpha\vdash\lnot\beta_{i}$ ($\Sigma\cdot\lnot\alpha\vdash\lnot\beta_{i}$) for some $\beta_{i}$, whereby the assumption $\alpha$ ($\lnot\alpha$) is appended to $\Sigma$. The same combinatorial analysis holds as we climb up the proof until, after collecting assumptions into a subsequence $\Delta$, we reach an axiom such that $\Sigma\cdot\Delta\vdash\lnot\beta_{0}$, where $\lnot\beta_{0}$ then occurs in $\Sigma\cdot\Delta$. The analysis for the first premiss of FI is similar, only with $\lnot\beta_{i}$s replaced by $\beta_{i}$s.

Examining the discharging rules NE and NI for negation, it is easy to see that, at the axioms, the subsequences $\Delta$ are complementary to $\Sigma$ in the sense that, if a formula $\gamma$ ($\lnot\gamma$) occurs in $\Delta$, then $\lnot\gamma$ ($\gamma$) occurs in $\Sigma$ and, therefore, is an element of $M^+$. Now, we can construct a proof of $\Sigma^\prime\vdash\alpha$ by exchanging some axioms $\Sigma\cdot\Delta\vdash\lnot\beta_{0}$ for $\Sigma^\prime\cdot\Delta^\prime\vdash\beta_{0}$ (or vice versa) and then, mutatis mutandis, exchanging applications of NI for NE (or vice versa). In some axioms of this new proof, a formula that occured in $\Sigma$ is replaced by its negation (or, alternatively, a negation is replaced by the negated formula). By hypothesis, there is such a proof (modulo assumption transformation rules and detours through CI and CE) where all the formulas occurring in $\Sigma^\prime$ are also elements of $M^+$. However, this would mean that both some formula and its negation (or, alternatively, a negation and the negated formula) are elements of $M^+$ which is in contradiction to the definition of $M^+$.