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.

  • 1
    $\begingroup$ I'm not sure what you mean, but a possible example would be the use of sequent calculus to prove that pure propositional logic is consistent. The essential idea would be that any natural deduction proof in propositional logic can be "reduced" to a "normal form" which satisfies a certain "subformula condition" - and then the reduced normal form of a proof $\vdash \bot$ would be something which obviously can't exist. (Or similarly, the proof that intuitionistic propositional logic can't prove excluded middle.) $\endgroup$ Sep 15, 2017 at 19:44
  • $\begingroup$ @DanielSchepler: That's a good example. $\endgroup$ Sep 15, 2017 at 19:45

1 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.

  • $\begingroup$ Maybe the quantifier elimination would be something like: every statement is equivalent to a disjunction of (conjunctions which uniquely determine a partition of the free variables into equal vs. nonequal subsets)? e.g. $a=b \wedge c=d \wedge a \ne c \wedge a \ne e \wedge c \ne e$ in case the free variables are $a$ through $e$. $\endgroup$ Sep 15, 2017 at 20:00
  • 1
    $\begingroup$ @DanielSchepler: Yes -- except when it isn't. The truth value can also depend on the size of the universe. $\endgroup$ Sep 15, 2017 at 20:11
  • $\begingroup$ Ah, right, of course... I guess the "free model" on $n$ variables would have to have elements consisting of an equivalence relation on $[n]$, along with a subset of $\mathbb{N}$ such that all sufficiently large numbers are either in or not in the set, with a restriction that some number at least equal to the number of equivalence classes is in the set. And then, of course, reduce that to a purely syntactic expression again. $\endgroup$ Sep 15, 2017 at 20:56
  • $\begingroup$ Or maybe, prove that the theory of infinite setoids (not finitely axiomatizable) doesn't prove $w = y$, and therefore the subtheory of arbitrary setoids can't prove it either. $\endgroup$ Sep 15, 2017 at 21:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .