Proofs without variables

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 → (ba)

Non-unique representations

a → (ba)

b → (ab)

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

xy (xy)

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:

aa (aa)

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!