Proving sentences to be unprovable with "combinatorial argument"? 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.
 A: 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.
