Proving sentences to be unprovable with "combinatorial argument"?

Question

In the answer https://math.stackexchange.com/a/2027281/351576 the following is stated.

It is also possible to show that things are unprovable using a direct combinatorial argument on the axioms and deduction rules you are allowed in your logic. I won't go into that here.

I'd like to go into that.

It is clear that for a theory $\Gamma:=\left\{\text{bird}(\text{penguin}), \text{flies}(\text{swallow}),\forall x:x \not = \text{penguin}\implies \text{flies}(x)\right\}$ it is not possible to prove "$\text{flies}(\text{penguin})$" i.e. $\neg \Gamma \vdash \text{flies}(\text{penguin})$.

How to formally prove this?

I'm also looking for books/resources on this.

Answer 1

I think something like the following might be what was meant:

Suppose there is a proof of ${\rm flies}({\rm penguin})$. Now rewrite the proof in the following way:

• Choose variable letters $y$ and $w$ that don't appear anywhere in the proof.
• Replace every ${\rm penguin}$ with $y$ and every term other than ${\rm penguin}$ by $w$.
• Replace every instance of the predicate ${\rm flies}(t)$ with $\neg(t=y)$.
• Replace every remaining atomic formula (including ${\rm bird}(t)$) that isn't an equality by $y=y$.

Argue that this substitution converts every valid inference step (or logical axiom) into another valid inference step. Therefore the substituted proof is actually a valid proof in the pure theory of equality of $$ y=y, w \ne y, \forall x(x\ne y\to x\ne y) \vdash y \ne y $$ However, the first and last of these premises are certainly provable (in standard first-order logic), and if we plug in their proofs we get $$ w \ne y \vdash y \ne y $$ which (by the deduction theorem, contraposition, and the fact that $\vdash y=y$) yields $$ \vdash w = y $$ which we can hopefully agree is not the case.

---

... well, how do we know that $\not\vdash w=y$? Unfortunately, the best argument for that I can come up with is everything that can be proved must be universally true in a structure with two elements (because all of the axioms are and the inference rules preserve that property) -- but that is then basically model theory and therefore presumably doesn't really count as "combinatorial".

I think it might be possible to get through purely syntactically by something in the vein of quantifier elimination, but the details of that elude me for the time being.