Is this sequent calculus complete?

Question

Edit: This question was edited to encoporate the problem Toby Bartels mentioned in their comment.

Note: Throughout this post propositional logic is being considered over the two connectives $\land$ and $\neg$. The connective $\to$ is an abbreviation and expressed in the usual way using the two mentioned connectives.
Consider the propositional sequent calculus with the following rules: $\dfrac{T\vdash\phi\land \psi}{T\vdash \phi,\psi}$, $\dfrac{T\vdash \phi,\psi}{T\vdash \phi \land \psi}$,$\dfrac{T\cup\{\phi\}\vdash \psi}{T\vdash \phi\to \psi}$,$\dfrac{T\vdash \phi \land \neg \phi}{T\vdash \bot},$$\dfrac{T\vdash \neg \phi \to \bot}{T\vdash \phi}$+The usual rule of monotonicity(weakening) and $\phi\vdash\phi$

(Note: The commas ",", inside(not the ones separating the rules!) the rules mean that if one has a proof with the top entailment achieved then on a line below one can conclude either of the formulas separated by the comma)

Question: Is this calculus complete? Or in other words does $T\vdash \phi \iff T\models \phi$? One direction is trivial, since the rules are clearly sound. Does the other direction hold? I am not very sure, for instance I can’t even see how to prove $\{\phi\to\bot\}\vdash\neg \phi$

Answer 1

Your deductive system satisfies completeness with respect to classical propositional logic.

I will prove this by using your calculus to emulate Łukasiewicz's first axiom system, which is known to be complete.

I. Notation

For the sake of readability, I will abbreviate $\Gamma \cup \{X\} \vdash Y$ simply as $\Gamma, X \vdash Y$. This means that commas in the answer mean something different than the (nonstandard) use of commas in the rules given above. Latin capital letters will stand for propositional formulae, while Greek capital letters stand for finite sets of formulae. Greek capitals occur only on the left of the turnstile. From here on, $A \rightarrow B$ abbreviates $\neg (A \wedge \neg B)$.

II. Deduction Theorem

We first show that your calculus satisfies the Deduction Theorem in the following form: $\Gamma, B \vdash C$ is derivable precisely if $\Gamma \vdash \neg (B \wedge \neg C)$ is derivable. The forward direction follows immediately from the rules of your system. For the backward direction we need to produce a derivation of $\Gamma, B \vdash C$ using a derivation of $\Gamma \vdash \neg (B \wedge \neg C)$. We can accomplish this as follows:

• 1 $\Gamma \vdash \neg (B \wedge \neg C)$     (we know how to derive this by assumption)
• 2 $\Gamma, B, \neg C \vdash B$     (by weakening and axiom)
• 3 $\Gamma, B, \neg C \vdash \neg C$     (by weakening and axiom)
• 4 $\Gamma, B, \neg C \vdash B \wedge \neg C$     (by second $\wedge$ rule from 2,3)
• 5 $\Gamma, B, \neg C \vdash \neg (B \wedge \neg C)$     (by weakening from 1)
• 6 $\Gamma, B, \neg C \vdash (B \wedge \neg C) \wedge \neg (B \wedge \neg C)$     (by second $\wedge$ rule from 4,5)
• 7 $\Gamma, B, \neg C \vdash \bot$     (by first $\bot$ rule from 6)
• 8 $\Gamma, B \vdash \neg(\neg C \wedge \neg \bot)$     (by forward deduction rule from 7)
• 9 $\Gamma, B \vdash C$     (by second $\bot$ rule from 8)

III. Cut Rule

Next, we show that the calculus satisfies the Cut Rule in the following form: if we can derive $\Gamma \vdash B$ and $\Gamma, B \vdash C$, then we can also derive $\Gamma \vdash C$.

• 1 $\Gamma \vdash B$     (we know how to derive this by assumption)
• 2 $\Gamma, B \vdash C$     (we know how to derive this by assumption)
• 3 $\Gamma, \neg C \vdash B$     (by weakening from 1)
• 4 $\Gamma, \neg C \vdash \neg C$     (by weakening and axiom)
• 5 $\Gamma, \neg C \vdash B \wedge \neg C$     (by second $\wedge$ rule from 3,4)
• 6 $\Gamma \vdash \neg (B \wedge \neg C)$     (by forward deduction rule from 2)
• 7 $\Gamma, \neg C \vdash \neg (B \wedge \neg C)$     (by weakening from 7)
• 8 $\Gamma, \neg C \vdash (B \wedge \neg C) \wedge \neg (B \wedge \neg C)$     (by second $\wedge$ rule from 6,7)
• 9 $\Gamma, \neg C \vdash \bot$     (by first $\bot$ rule from 8)
• 10 $\Gamma \vdash \neg(C \wedge \neg \bot)$     (by forward deduction rule from 9)
• 11 $\Gamma \vdash C$     (by second $\bot$ rule from 10)

The ordinary Modus Ponens rule follows by choosing $\Gamma = \emptyset$ and applying the Deduction Theorem. Formulating and proving a similar rule involving $\Gamma \vdash B$; $B \vdash C$; $\Gamma \vdash C$ is a good exercise.

IV. Completeness

Łukasiewicz's complete system for propositional logic consists of the Modus Ponens inference rule (from $\vdash_L A$ and $\vdash_L A \rightarrow B$ infer $\vdash_L B$), along with the following three axiom schemas:

1. $\vdash_L A \rightarrow (\neg A \rightarrow B)$,
2. $\vdash_L (\neg A \rightarrow A) \rightarrow A$,
3. $\vdash_L (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$.

Since your deductive system supports a Deduction Theorem and the Modus Ponens rule, all we have to do is produce derivations of these three schemas in your system to show that your calculus can emulate Łukasiewicz's system. Since the latter is complete, the completeness of your proof calculus will immediately follow.

I will now demonstrate that derivations of each of these schemas indeed exist in your system.

For $\vdash A \rightarrow (\neg A \rightarrow B)$, the Deduction Theorem tells us that it's sufficient to find a derivation of $A, \neg A \vdash B$. In turn, the second $\bot$ rule (and another use of the deduction theorem) shows that it's enough to derive $A, \neg A, \neg B \vdash \bot$. But $A, \neg A \vdash \bot$ already, so by weakening we're done.

For $\vdash (\neg A \rightarrow A) \rightarrow A$, we can use the Deduction Theorem and the $\bot$ rules again, to reduce it to $\neg (\neg A \wedge \neg A), \neg A \vdash \bot$. But that's immediate: both $\neg A \wedge \neg A$ and its negation follow from the assumptions.

This leaves $\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$.

We can clearly prove $B \rightarrow C \vdash B \rightarrow C$. By the Deduction Theorem, $B \rightarrow C, B \vdash C$ holds as well. Weakening gives $A \rightarrow B, B \rightarrow C, A, B\vdash C$. Since $A \rightarrow B, B \rightarrow C, A \vdash B$ holds too, we can apply the Cut rule to conclude $A \rightarrow B, B \rightarrow C, A \vdash C$. One last use of the deduction theorem gives us $\vdash (A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$, which was to be shown.

Notes and terminology

On one hand, the term sequent calculus does not have a formal definition. On the other hand, it does have some "connotations": proof theorists usually apply this moniker to deductive systems that enjoy certain structural properties, such as (at least nominal) support for bottom-up proof search, cut-elimination, or the subformula property.

Confusingly, even though the deductive system you presented here indeed constitutes a proof calculus, and every step of the proof is indeed a conditional tautology (a sequent), your system is not something that practicing proof theorists would call a sequent calculus. (Aside: No bottom-up proof search: when going bottom-up, the first $\bot$ rule requires you to conjure up some $\varphi$ out of nowhere, without any guidance. Similarly, the calculus does not enjoy the subformula property.)

While the completeness proof of Łukasiewicz's system is standard (and the result is well-known), I don't have a reference at hand. If you wish to track down a reference, you might want to start from this OCW course. One could, of course, give a direct completeness proof for your calculus (one that does not involve reduction to any intermediary), but due to the ad-hoc nature of your rules, such a proof is unlikely to provide any further insight.

Edit: This leaves only your side question: how does one prove $X \rightarrow \bot \vdash \neg X$? Fortunately, it's not difficult using the tools we've built up in the rest of the answer.

Step 1: Notice that $\neg \neg X \vdash X$ is derivable. Proof. We have $\neg \neg X, \neg X \vdash \bot$, so the Deduction Theorem gives $\neg \neg X \vdash \neg X \rightarrow \bot$, from which $\neg \neg X \vdash X$ follows by a $\bot$ rule.

Step 2: Notice that $X \rightarrow \bot, \neg\neg X, X \vdash \bot$ is also derivable. This follows from $X \rightarrow \bot, \neg \neg X \vdash X \rightarrow \bot$ by the Deduction Theorem.

Step 3: From Step 1 and Weakening, we know that $X \rightarrow \bot, \neg \neg X \vdash X$. From Step 2, we have $X \rightarrow \bot, \neg\neg X, X \vdash \bot$. By the Cut Rule, we get $X \rightarrow \bot, \neg\neg X \vdash \bot$, from which a $\bot$ rule gives $X \rightarrow \bot \vdash \neg X$ as desired.

Answer 2

Note: Everything in this answer is w.r.t to the sequent calculus presented in the question.

I think the completeness of this system can be proven in a directly in the following manner(this is essentially the usual proof of completeness):

First note that every consistent set, $M$, is contained in a maximally consistent set $\mathcal{M}$(a consistent set with no consistent superset).
Maximally consistent sets satisfy these two properties:

• Deductive Closure: Proof: Suppose $\mathcal{M}\vdash \phi$ now if $\phi\not\in\mathcal{M}$ then $\mathcal{M}\cup\{\phi\}\vdash\bot$, but then we have $\mathcal{M}\vdash\neg\phi$(See Z.A.K’s edit) a contradiction.
• Completeness: Exactly one of $\mathcal{M}\vdash\phi$ , $\mathcal{M}\vdash\neg\phi$ holds.Proof: Easy left for the reader.

Now every maximally consistent has a model:
Proof:
Define $t_{\mathcal{M}}$ as a function from the atoms to $\{0,1\}$ on the set of atoms satisfiying $t_{\mathcal{M}}(p)=0$ iff $p\in \mathcal{M}$ and $1$ otherwise. Let $\overline {t_{\mathcal{M}}}$ denote the valuation(or interpretation) that extends ${t_{\mathcal{M}}}$, I claim that $\overline {t_{\mathcal{M}}}(\phi)=1\iff \phi\in \mathcal{M}$(Hence every maximally consistent set has a model), this can be proven by the following induction argument on the set of wffs:
Base case: Atoms: Trivial, for $\bot$ the claim holds vacuously.
Induction step($\land$): Suppose that the claim holds for $\phi$ and $\psi$ then it holds for $(\phi\land \psi)$:
Forward direction: $\overline {t_{\mathcal{M}}}(\phi\land \psi)=1$ implies that both $\overline {t_{\mathcal{M}}}(\phi)=1$ and $\overline {t_{\mathcal{M}}}(\psi)=1$ by the induction hypothesis we have $\mathcal{M}\vdash \phi $ and $\mathcal{M}\vdash\phi$ and so $\mathcal{M}\vdash (\phi \land \psi)$.
Backward direction: Suppose $(\phi\land \psi)\in \mathcal{M}$ then since maximally consistent sets are deductively closed we have $\phi\in \mathcal{M} $ and $\psi \in \mathcal{M}$ and therefore by the induction hypothesis we trivially get the backward direction.
Induction step($\neg)$:Suppose the claim holds for $\phi$ then it holds for $\neg \phi$, this follows easily from completeness.$\square$

Since each consistent set is contained in a maximally consistent set, and every maximally consistent set has a model, every consistent set has a model. So if $T\models\phi$ then we have $T\cup\{\neg \phi\}\models \bot$, and so $T\cup\{\neg \phi\}\vdash \bot$(Because it doesn’t have any model) which implies $T\vdash\phi$ $\square$