# Proofs without variables

% Remco Bloemen % 2010-05-09, last updated 2014-03-04

Suppose we have a formal system for proposition logic with an axiom set containing the modus ponens, the principle of simplification and Frege’s axiom:

```
C →
T 'Modus Ponens'
∧ a
∧ a → b
⊨ b
∎
T 'Principle of simplification'
⊨ a → (b → a)
∎
T 'Frege's axiom'
⊨ (a → (b → c)) → ((a → b) → (a → c))
∎
```

This is similar to the system I have used before but I have removed the well-formedness and Polish notation for clarity.

In this system one can proof truths like "a → a" as follows:

```
T 'From a follows a'
∵ 'Principle of simplification'
a ⊧ a
b ⊧ a
∴ a → (a → a)
∵ 'Principle of simplification'
a ⊧ a
b ⊧ a → a
∴ a → ((a → a) → a)
∵ 'Frege's axiom'
a ⊧ a
b ⊧ a → a
c ⊧ a
∴ (a → ((a → a) → a)) → ((a → (a → a)) → (a → a))
∵ 'Modus Ponens'
a ⊧ a → ((a → a) → a)
b ⊧ (a → (a → a)) → (a → a)
∴ (a → (a → a)) → (a → a)
∵ 'Modus Ponens'
a ⊧ a → (a → a)
b ⊧ a → a
∴ a → a
∎
```

## The problem with variables

*a* → (*b* → *a*)

### Non-unique representations

*a* → (*b* → *a*)

*b* → (*a* → *b*)

In fact, if you give me *n* different variable names, I can give you *n*
² different representations *of the exact same theorem*.

### Bound variables

Consider

∀*x* ∃*y* (*x* ≠ *y*)

For every number *x* there exist a number *y* such that *x* is not equal
to *y*. True.

and now substitute *a* for *x* and *a* for *y*:

∀*a* ∃*a* (*a* ≠ *a*)

For every number *a* there exist a number *a* such that *a* is not equal
to *a*. Rubbish!

It is even funnier to substitute *a* for *x* and 3 for *y*:

∀*a* ∃3 (*a* ≠ 3)

For every number *a* there exist a number 3 such that *a* is not equal
to 3. Ridiculous!