III Logic - Proof theory and constructive logic

1Proof theory and constructive logic

III Logic

1.1 Natural deduction

The first person to have the notion of “proof” as a mathematical notion was

probably G¨odel, and he needed this to write down the incompleteness theorem.

The notion of proof he had was a very unintuitive notion. It is not very easy to

manipulate, but they are easy to reason about.

In later years, people came up with more “natural” ways of defining proofs,

and they are called natural deduction. In the formalism we learnt in IID Logic

and Set Theory, we had three axioms only, and one rule of inference. In natural

deduction, we have many rules of deduction.

We write or rules in the following form:

A B

∧-int

A ∧ B

This says if we know

and

are true, then we can conclude

A ∧ B

. We call

the things above the line the premises, and those below the line the conclusions.

We can write out the other rules as follows:

A B

∧-int

A ∧ B

∧-elim

A ∧ B

∧-elim

∨-int

A ∨ B

∨-int

A ∨ B

A A → B

→-elim

Here we are separating these rules into two kinds — the first column is the

introduction rules. These tell us how we can introduce a

∧

∨

into our

conclusions. The second column is the elimination rules. These tell us how we

can eliminate the ∧ or → from our premises.

In general, we can think of these rules as “LEGO pieces”, and we can use

them to piece together to get “LEGO assembles”, i.e. proofs.

Example. For example, we might have a proof that looks like

∨-int

A ∨ B A ∨ B → C

→-elim

This corresponds to a proof that we can prove

from

and

A ∨ B → C

. Note

that sometimes we are lazy and don’t specify the rules we are using.

Instead of trying to formally describe how we can put these rules together

to form a proof, we will work through some examples as we go, and it should

become clear.

We see that we are missing some rules from the table, as there are no

introduction rule for → and elimination rule for ∨.

We work with

→

first. How we can prove

A → B

? To do so, we assume

and then try to prove

. If we can do so, then we have proved

A → B

. But we

cannot express this in the form of our previous rules. Instead what we want is

some “function” that takes proof trees to proof trees.

The actual rule is as follows: suppose we have derivation that looks like

This is a proof of C under the assumption A. The

→

-introduction rule says we

can take this and turn it into a proof of A → C.

A → C

This rule is not a LEGO piece. Instead, it is a magic wand that turns a LEGO

assembly into a LEGO assembly.

But we do not want magic wands in our proofs. We want to figure out some

more static way of writing this rule. We decided that it should look like this:

[A]

→-int

A → C

Here the brackets denotes that we have given up on our assumption

to obtain

the conclusion

A → C

. After doing so, we are no longer assuming

. When we

work with complicated proofs, it is easy to get lost where we are eliminating the

assumptions. So we would label them, and write this as, say

[A]

→-int (1)

A → C

Example. We can transform our previous example to say

[A]

∨-int

A ∨ B A ∨ B → C

→-elim

→-int (1)

A → C

Originally, we had a proof that

and

A ∨ B → C

proves

. Now what we have

is a proof that A ∨ B → C implies A → C.

Next, we need an elimination rule of

A ∨ B

. What should this be? Suppose

we proved both that

proves

, and

proves

. Then if we know

A ∨ B

, then

we know C must be true.

In other words, if we have

A ∨ B

then we can deduce C. We write this as

A ∨ B

[A]

[B]

∨-elim

There is an obvious generalization to many disjunctions:

∨ · · · ∨ A

]

∨-elim

How about when we have an empty disjunction? The empty disjunction is just

false. So this gives the rule

⊥

In other words, we can prove anything assume falsehood. This is known as ex

falso sequitur quolibet.

Note that we did not provide any rules for talking about negation. We do

not need to do so, because we just take ¬A to be A → ⊥.

So far, what we have described it constructive propositional logic. What is

missing? We cannot use our system to prove the law of excluded middle,

A ∨ ¬A

or the law of double negation

¬¬A → A

. It is not difficult to convince ourselves

that it is impossible to prove these using the laws we have described above.

To obtain classical propositional logic, we need just one more rule, which is

[A → ⊥]

⊥

If we add this, then we get classical propositional calculus, and it is a theorem

that any truth-table-tautology (i.e. propositions that are always true for all

possible values of

A, B, C

etc) can be proved using natural deduction with the

law of excluded middle.

Example. Suppose we want to prove

A → (B → C) → ((A → B) → (A → C))

How can we possibly prove this? The only way we can obtain this is to get

something of the form

[A → (B → C)]

(A → B) → (A → C)

→-int

A → (B → C) → ((A → B) → (A → C))

Now the only way we can get the second-to-last conclusion is

A → B [A]

A → C

and then further eliminating

A → B

gives us (

A → B

)

→

(

A → C

). At this

point we might see how we can patch them together to get a proof:

[A]

[A → (B → C)]

B → C

[A → B]

[A]

→-int (3)

A → C

→-int (2)

(A → B) → (A → C)

→-int (1)

A → (B → C) → ((A → B) → (A → C))

Note that when we did

→

-int (3), we consumed two copies of

in one go. This

is allowed, as an assumption doesn’t become false after we use it once.

However, some people study logical systems that do not allow it, and demand

that assumptions can only be used once. These are known as resource logics,

one prominent example of which is linear logic.

Example. Suppose we want to prove A → (B → A). We have a proof tree

[A]

[B]

→-int (2)

B → A

→-int (1)

A → (B → A)

How did we manage to do the step from

A B

? One can prove it as follows:

A B

∧-int

A ∧ B

∧-elim

but this is slightly unpleasant. It is redundant, and also breaks some nice

properties of natural deduction we are going to prove later, e.g. the subformula

property. So instead, we just put an additional weakening rule that just says we

can drop any assumptions we like at any time.

Example. Suppose we wanted to prove

A → (B ∨ C) → ((A → B) ∨ (A → C)).

This is indeed a truth-table tautology, as we can write out the truth table and

see this is always true.

If we try very hard, we will find out that we cannot prove it without using the

law of excluded middle. In fact, this is not valid in constructive logic. Intuitively,

the reason is that assuming

is true, which of

is true can depend on

why

is true, and this it is impossible to directly prove that either

A → B

true, or A → C is true.

Of course, this is true in classical logic.

Exercise. Prove the following:

– (P → Q) → ((Q → R) → (P → R))

– (A → C) → ((A ∧ B) → C)

– ((A ∨ B) → C) → (A → C)

– P → (¬P → Q)

– A → (A → A)

– (P ∨ Q) → (((P → R) ∧ (Q → S)) → R ∨ S)

– (P ∧ Q) → (((P → R) ∨ (Q → S)) → R ∨ S)

– A → ((((A → B) → B) → C) → C)

– ((((P → Q) → P ) → P ) → Q) → Q

The last two are hard.

Instead of thinking of natural deduction as an actual logical theory, we often

think of it as a “platform” that allows us to describe different logical theories,

which we can do by introducing other connectives.

Example.

For example, we might want to describe first-order logic. We can

give introduction rules for ∃ as follows:

ϕ(t)

∃-int

∃

ϕ(x)

Similarly, we can have an elimination rule for ∀ easily:

∀

ϕ(x)

∀-elim

ϕ(t)

The introduction rule for

∀

is a bit more complicated. The rule again looks

something like

ϕ(x)

∀-int

∀

ϕ(x)

but for such a proof to be valid, the

must be “arbitrary”. So we need an

additional condition on this rule that there is no free occurrence of x’s.

Finally, suppose we know

∃

(

). How can we use this to deduce some

Suppose we know that

(

) implies

, and also

does not depend on

. Then

just knowing that there exists some x such that ϕ(x), we know p must be true.

∃

ϕ(x)

∃-elim

Again we need x to be arbitrary in p.

Example.

We can also use natural deduction for “naive set theory”, which we

will later find to be inconsistent. We can give an ∈-introduction rule

ϕ(x)

∈-int

x ∈ {y : ϕ(y)}

and a similar elimination rule

x ∈ {y : ϕ(y)}

∈-elim

ϕ(x)

One cannot expect that we can write down whatever introduction and

elimination rule we like, and expect to get a sensible theory. For example, if we

introduce a connective & with the following silly rules:

&-int

A&B

&-elim

then this would immediately give us a theory that proves anything we like.

There are in fact two problems with our introduction and elimination rules.

The first is that once we use our

to deduce

, it is completely gone, and

we cannot recover anything about

from

. The second problem is that,

obviously, proving

doesn’t really involve

at all, but we can use

deduce something about B.

In general, to obtain a sensible natural deduction theory, we need harmony.

Definition

(Harmony)

We say rules for a connective $ are harmonious if

is the strongest assertion you can deduce from the assumptions in the rule of

$-introduction, and

is the weakest thing that implies the conclusion of the

$-elimination rule.

We will not make the notion more precise than this.

Example.

The introduction and elimination rules for

∈

we presented are cer-

tainly harmonious, because the conclusions and assumptions are in fact equiva-

lent.

One can also check that the introduction and elimination rules for

∧

and

∨

are harmonious.

Example (Russel’s paradox). In naive set theory, consider

R = {x : x ∈ x → ⊥}.

Then we can have the deductions

R → R

∈-elim

R ∈ R → ⊥

→-elim

⊥

We can then move on to use this to deduce that R ∈ R:

[R → R]

∈-elim

R ∈ R → ⊥

→-elim

⊥

→-int (1)

R ∈ R → ⊥

∈-int

R ∈ R

Now we have proved

R ∈ R

. But we previously had a proof that

R ∈ R

gives a

contradiction. So what we are going to do is to make two copies of this proof:

[R → R]

∈-elim

R ∈ R → ⊥

→-elim

⊥

→-int (1)

R ∈ R → ⊥

∈-int

R ∈ R

[R → R]

∈-elim

R ∈ R → ⊥

→-elim

⊥

→-int (2)

R ∈ R → ⊥

→-elim

⊥

So we showed that we have an inconsistent theory.

Note that we didn’t use a lot of “logical power” here. We didn’t use the

law of excluded middle, so this contradiction manifests itself even in the case

of constructive logic. Moreover, we didn’t really use many axioms of naive set

theory. We didn’t even need things like extensionality for this to work.

Now we notice that this proof is rather weird. We first had an

→

-introduction

(2), and then subsequently eliminated it immediately. In general, if we have a

derivation of the form

→-int

P → Q

→-elim

We can just move the second column to the top of the first to get

In general,

Definition

(Maximal formula)

We say a formula in a derivation is maximal iff

it is both the conclusion of an occurrence of an introduction rule, and the major

premiss of an occurrence of the elimination rule for the same connective.

Here it is important that we are talking about the major premise. In a

deduction

A → B A

→-elim

we call

A → B

the major premise, and

the minor premise. In the case of

∧

and ∨, the terms are symmetric, and we do not need such a distinction.

This distinction is necessary since a deduction of the form

(A → B) → C

[A]

→-int

A → B

→-elim

One can prove that any derivation in propositional logic can be converted to

one that does not contain maximal formulae. However, if we try to eliminate

the maximal formula in our proof of inconsistency of naive set theory, we will

find that we will end up with the same proof!