Contradictory vacuous truths in consistent formal system

Question

Can 2 contradictory vacuously true statements be proved in a consistent formal system?

Answer 1

Vacuity doesn't enter into this at all. Consistency means that no pair of contradictory sentences can be proved. You're asking "Can a consistent theory be inconsistent?," and the answer to this is clearly no by definition.

---

That said, we can (and generally do) simultaneously prove statements of the form $$\forall x(P(x)\implies Q(x))\quad\mbox{and}\quad\forall x(P(x)\implies \neg Q(x)),$$ but this doesn't constitute a pair of contradictory statements; these two sentences can indeed be both true at the same time. Indeed, their conjunction is equivalent to $\forall x(\neg P(x))$, so we only get a contradiction if in addition our theory proves $\exists x(P(x))$. Indeed, this is exactly what characterizes vacuity: $\forall x(P(x)\implies Q(x))$ is a vacuous truth (with respect to our theory) iff $\forall x(P(x)\implies \neg Q(x))$ is.