Removing an Antecedent

Question

Suppose $ A \vdash B$

where $A$ is of the form $\forall x\ P(x) \rightarrow \ ... $

and where $B$ does not include the predicate $P$.

My intuition is that this implies that $B$ is a tautology, as in :

$ \vdash B$

But unfortunately I lack the proof-theoretic background to determine exactly why. I can think of an argument involving resolution-proofs, but that requires that the logic we're dealing with is Classical First-Order-Logic, and I was hoping that the result could be shown for a more general case.

Appreciate if anyone has any thoughts... Thanks!

Answer 1

We have a related result, the Craig interpolation theorem.

Assume that $\alpha$ and $\beta$ contain no common predicate symbols and that $\vdash \alpha \to \beta$.

Then:

either $\vdash \lnot \alpha$ or $\vdash \beta$.

Thus, under what condition we have that $\alpha$ is unsatisfiable, when it has the form $\forall x Px \to C$ ?

But we can always find some interpretation where $Px$ does not hold of every objects. Thus, we can always find some interpretation where $\forall x Px \to C$ is a conditional with False antecedent, i.e. such that the formula is True.

Answer 2

For classical logic, one can give a very short semantic proof. If $B$ is not a tautology, then it fails in some model $\mathcal{M}$. Extend that model to $\mathcal{M}_+$ by interpreting $P$ as the empty unary relation, and observe that $\mathcal{M}_+ \models \forall x. P(x) \rightarrow Q$.

The syntactic argument is somewhat more difficult. I will prove the intuitionistic case, but one can show the classical case by a similar argument.

The cut-free sequent calculus proof system LJ has the following convenient property: if $\Gamma, X \vdash \Delta$ has an LJ-proof in which every subformula of $X$ eventually disappears by weakening, then $\Gamma \vdash \Delta$ has a proof. This can be established by a simple induction on the length of the proof.

Now assume that $\forall x. P(x) \rightarrow Q \vdash B$ has an LJ-proof. We claim that in this proof no formula $P(t)$ ever occurs on the left of the turnstile. If one applies the left implication rule to something of the form $P(t) \rightarrow Q$, then $P(t)$ ends up on the right of the turnstile, and since $P(t)$ is atomic, it will not migrate back to the left. The only other way it could appear on the left is if it was a subformula of $B$, but by assumption $B$ does not mention the predicate $P$ at all. Hence, $P(t)$ never occurs on the left of the turnstile in this LJ-proof. It follows that $P(t) \rightarrow Q$ and $\forall x.P(x) \rightarrow Q$ never occur on the right (otherwise, we could use the right universal and right implication rules to make $P(t)$ appear on the left).

Since $P(t)$ cannot occur on the left, it won't appear as the active formula of any axiom $\overline{P(t) \vdash P(t)}$. Therefore, no finished branch of the proof can contain $P(t)$, so every instance of $P(t)$ must eventually (dis)appear as the active formula of weakening. The same holds for $P(t) \rightarrow Q$ and $\forall x. P(x) \rightarrow Q$, which cannot occur on the right. So in the assumed proof of $\forall x. P(x) \rightarrow Q \vdash B$, every subformula of $\forall x. P(x) \rightarrow Q$ eventually disappears by weakening. By the convenient property above, we conclude that $\vdash B$ has a proof. Therefore, $B$ is a tautology.