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 → (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!

Expressions as directed graphs

Operators

Theorems

Unique representations

Definitions as directed graphs