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!
