Ernest Schimmerling ; Basic and Intermediate Logic ; Chapter 2

# Online textbook for Basic and Intermediate Logic

## Chapter 2 : Propositional logic

Propositional logic formalizes a small fragment of the logic we use in everyday mathematics. But it is rich enough to illustrate some of the ideas we will apply later in the course to more powerful first-order logic.

### § 2.1   Syntax

We begin by introducing a propositional language with infinitely many parameters. Sentences in this language are built up by recursion from the symbols of the language.

#### List of symbols

 ⊤ ¬ ∧ Pn   for n = 0, 1, 2 etc. ⊥ ∨ → ↔

#### Recursive definition of sentences

• ⊤ and ⊥ are sentences.
• Each Pn is a sentence.
• If φ and ψ are sentences, then so are ( ¬ , φ ) , ( ∧ , φ , ψ ) , ( ∨ , φ , ψ ) , ( → , φ , ψ ) and ( ↔ , φ , ψ ).

The various types of sentences have names:

• The constants are ⊤ and ⊥.
• The parameters are P0 , ... , Pn etc.
• Negations have the form ( ¬ , φ ).
• Conjunctions have the form ( ∧ , φ , ψ ).
• Disjunctions have the form ( ∨ , φ , ψ ).
• Conditionals have the form ( → , φ , ψ ).
• Biconditionals have the form ( ↔ , φ , ψ ).

#### Alternative notations for sentences

Consider the sentence:

( ∨ , ( ∧ , P0 , P1 ) , P2 )

Compare it with the string

∨ ∧ P0 P1 P2

In other words, we have erased the parentheses. (Also the commas.) However, we have not introduced ambiguity because there is only one way to insert parentheses which ends up with a sentence. This is the beauty of what is called Polish notation. On the other hand, Polish notation is painful to read with or without parentheses!

Almost always in this course, we will prefer to use the traditional notation, in which our example is written

( P0 ∧ P1 ) ∨ P2.

We still have parentheses but they are used differently and the sentence is much easier to read. Note that we would never write

P0 ∧ P1 ∨ P2

without parentheses because we would not be able to tell whether we mean

( P0 ∧ P1 ) ∨ P2

or

P0 ∧ ( P1 ∨ P2 ).

In other words, we would not be able to tell whether we mean

( ∨ , ( ∧ , P0 , P1 ) , P2 )

or

( ∧ , P0 , ( ∨ , P1 , P2 ) ).

Yet another way to write sentences is in tree notation. We could picture our example as the following downward growing finite tree.

 ∨ | \ ∧ P2 | \ P0 P1

While we will not emphasize tree notation in this course, sometimes it is a useful image to have in mind.

Another useful way to analyze a sentence is to list its subsentences. In our example:

P0

P1

P2

P0 ∧ P1

( P0 ∧ P1 ) ∨ P2

Notice that proper subsentences are shorter in length. Also observe that proper subsentences of sentences on the list occur earlier on the list. This is always possible and sometimes useful in logic.

#### Recursive definitions and inductive proofs

The recursion and induction principles for natural numbers are considered background for this course. Our definition of "sentence" is supposed to be by recursion but it does not mention natural numbers. Here is an alternative definition of that uses only the version of recursion you are already familiar with from other courses.

First define a function S with dom ( S ) = ω by recursion as follows.

• S ( 0 ) = { ⊤ , ⊥ } ∪ { Pi ∣ i ∈ ω }.
• S ( n + 1 ) = S ( n ) ∪ { ¬ φ ∣ φ ∈ S ( n ) } ∪ { φ ∧ ψ ∣ φ , ψ ∈ S ( n ) } ∪ { φ ∨ ψ ∣ φ , ψ ∈ S ( n ) } ∪ { φ → ψ ∣ φ , ψ ∈ S ( n ) } ∪ { φ ↔ ψ ∣ φ , ψ ∈ S ( n ) }.
Then φ is a sentence iff there exists n ∈ ω such that φ ∈ S ( n ).

What is really going on here is that S ( n ) is the set of sentences of complexity ≤ n where complexity is defined by recursion as follows.

• ⊤, ⊥ and Pi have complexity 0.
• If the complexity of φ is n, then the complexity of ¬ φ is n+1.

• If the complexity of φ is m and the complexity of ψ is n, then each of φ ∧ ψ, φ ∨ ψ, φ → ψ and φ ↔ ψ has complexity max ( m , n ) + 1.
Notice that the complexity of a sentence is a natural number. Also that proper subsentences have strictly smaller complexity. This makes it possible to prove things about sentences by induction on complexity. The following principle captures the essence of this idea.

#### Induction Lemma 2.1

Let Σ ⊆ { φ ∣ φ is a sentence }.

Assume the following.

• ⊤ and ⊥ belong to Σ.
• Each Pn belongs to Σ.
• If φ and ψ belong to Σ, then so do ¬ φ , φ ∧ ψ , φ ∨ ψ , φ → ψ and φ ↔ ψ.

Then Σ = { φ ∣ φ is a sentence }.

#### Lemma 2.2

{ φ ∣ φ is a sentence } is countable.

#### Proof of Lemma 2.2

Let S ( n ) be the set of sentences of complexity ≤ n.

By induction, we prove that S ( n ) is countable.

S ( 0 ) is the union of the countable set { Pi ∣ i ∈ ω } and the pair { ⊤ , ⊥ } , so S ( 0 ) is countable.

Assume S ( n ) is countable.

By definition, S ( n + 1 ) is the union of six sets:

S ( n )

{ ¬ φi ∣ i ∈ ω }

{ φi ∧ φj ∣ i , j ∈ ω }

{ φi ∨ φj ∣ i , j ∈ ω }

{ φi → φj ∣ i , j ∈ ω }

{ φi ↔ φj ∣ i , j ∈ ω }

Using the induction hypothesis, we see that each of these six sets is countable.

Since S ( n + 1 ) is a union of six countable sets, it is also countable.

That completes the induction.

Now { S ( n ) ∣ n ∈ ω } is a countable collection of countable sets.

Therefore, its union { φ ∣ φ is a sentence } is countable by Lemma 1.4.

QED

### § 2.2   Semantics

Functions from { Pn ∣ n = 0, 1, 2 , … } to { 0 , 1 } are called structures.

Each structure A has a corresponding truth function, TruthA, which is a certain function from { φ ∣ φ is a sentence } to { 0 , 1 }.

TruthA is recursively defined as follows.

• TruthA ( Pn ) = 1 iff A ( Pn ) =1.

• TruthA ( ⊤ ) = 1 and TruthA ( ⊥ ) = 0.
• TruthA ( ¬ φ ) = 1 iff TruthA ( φ ) = 0.
• TruthA ( φ ∧ ψ ) = 1 iff ( TruthA ( φ ) = 1 and TruthA ( ψ ) = 1 ).
• TruthA ( φ ∨ ψ ) = 1 iff ( TruthA( φ ) = 1 or TruthA ( ψ ) = 1 ).
• TruthA ( φ → ψ ) = 1 iff ( TruthA ( φ ) = 1 implies TruthA ( ψ ) = 1 ).
• TruthA ( φ ↔ ψ ) = 1 iff ( TruthA ( φ ) = 1 iff TruthA ( ψ ) = 1 ).
The double turnstile symbol ⊨ is used in several different ways which depend on what sort of objects appear to its left and right. Pay attention to this in the following definitions.
• Σ is a theory iff Σ ⊆ { φ ∣ φ is a sentence }.
• (The members of a theory are called its axioms.)

• A is a model of φ and write A ⊨ φ iff TruthA ( φ ) = 1.

(We also say A satisfies φ.)

• A is a model of Σ and write A ⊨ Σ iff A is a model of every member of Σ.
• (We also say A satisfies Σ.)

• ψ is a consequence of φ and write φ ⊨ ψ iff every model of φ is a model of ψ.

• φ is a consequence of Σ and write Σ ⊨ φ iff every model of Σ is a model of φ.
• φ and ψ are logically equivalent and write ψ ╞╡ ψ iff they have exactly the same models.
• (That is, φ ⊨ ψ and ψ ⊨ φ.)

• φ is valid iff every structure is a model of φ.
• (That is, { } ⊨ φ. This may be abbreviated as just ⊨ φ.)

• φ is satisfiable iff φ has at least one model.
• Σ is satisfiable iff Σ has at least one model.

### § 2.3   Truth tables

The truth table for φ is the function A ↦ TruthA ( φ ).

#### Example 2.A

Here is a truth table presented in a familiar way.

 P0 P1 P2 ( P0 → P1 ) ↔ P2 0 0 0 0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 0 1 1 0 1 0 1 1 0 0 1 1 1 1

The first row of this table tells us that if A is any structure with

A ( P0 ) = A ( P1 ) = A ( P2 ) = 0,

then

TruthA ( ( P0 → P1 ) ↔ P2 ) = 0.

The second row of the table tells us that if A is any structure with

A ( P0 ) = A ( P1 ) = 0 and A ( P2 ) = 1,

then

TruthA ( ( P0 → P1 ) ↔ P2 ) = 1.

Notice how the values of A ( Pn ) for n > 2 are irrelevant to this example.

### § 2.4   A deduction system

In everyday mathematics, a theory is a collection of axioms. From the axioms of the theory, we come up with proofs of theorems. The proofs can be broken up into steps where each step is justified by some kind of basic rule about proofs. The axioms of the theory are allowed to be used in the proof.

Our goal is to develop a formal proof system for propositional logic that mirrors what goes on in everyday mathematics. You can imagine that there are many legitimate ways to do this. In fact, we will present two versions. To keep the straight which is which, we will use different names. The words "proof" and "deduction" are synonyms in English but their formal versions will mean different things.

Returning to propositional logic, consider a theory Σ and a sentence ψ. We will explain what is meant that from Σ we may deduce ψ. In this case, we will write Σ ⊢ ψ. Before giving the general definition of Σ ⊢ ψ we list the deduction rules.

 ⊤-in { } ⊢ ⊤ ⊥-out { ⊥ } ⊢ φ ¬-in Σ ∪ { φ } ⊢ ψ and Σ ∪ { φ } ⊢ ¬ ψ implies Σ ⊢ ¬ φ ¬-out { ¬ ¬ φ } ⊢ φ ∧-in { φ , ψ } ⊢ φ ∧ ψ ∧-out { φ ∧ ψ } ⊢ φ and { φ ∧ ψ } ⊢ ψ ∨-in { φ } ⊢ φ ∨ ψ and { ψ } ⊢ φ ∨ ψ ∨-out Σ ∪ { φ } ⊢ χ and Σ ∪ { ψ } ⊢ χ implies Σ ∪ { φ ∨ ψ } ⊢ χ →-in Σ ∪ { φ } ⊢ ψ implies Σ ⊢ φ → ψ →-out { φ, φ → ψ } ⊢ ψ ↔-in { ψ → φ , φ → ψ } ⊢ φ ↔ ψ ↔-out { φ ↔ ψ } ⊢ φ → ψ and { φ ↔ ψ } ⊢ ψ → φ R1 If Δ ⊆ Σ and Δ ⊢ φ, then Σ ⊢ φ. R2 If Σ ⊢ φi for every i < n and { φi ∣ i < n } ⊢ ψ, then Σ ⊢ ψ. R3 If φ belongs to Σ, then Σ ⊢ φ.

Some of the deduction rules have popular alternative names:

• ¬-in is proof by contradiction.
• ¬-out is discharge of double negation.
• ∧-in is proof by parts.
• ∨-out is proof by cases.
• →-out is modes ponens.

Deductions are justified by applying the deduction rules finitely many times. Before stating the definitions of "deduction" and "justification", it is best to give a couple of illustrative examples.

#### Example 2.B

Assume that φ belongs to Σ. Equivalently, that { φ } ⊆ Σ.

1. { φ } ⊢ φ ∧ φ by the ∧-in rule.
2. { φ ∧ φ } ⊢ φ by the ∧-out rule.
3. { φ } ⊢ φ by rule R2 and lines 1 and 2.
4. Σ ⊢ φ by rule R1 and line 3.

Notice that the last line is rule R3. In other words, rule R3 can be justified by the other rules, so we do not really need to include it in our system. Officially, we keep it because it seems so basic and is used so often. But when it suits us, we may assume it was not used in a justification. Rule R3 corresponds to the idea that "every assumption is a theorem".

#### Example 2.C [corrected 9/11/18]

1. { ¬ ( φ ∨ ¬ φ ) , φ } ⊢ φ ∨ ¬ φ by the ∨-in rule.
2. { ¬ ( φ ∨ ¬ φ ) , φ } ⊢ ¬ ( φ ∨ ¬ φ ) by rule R3.
3. { ¬ ( φ ∨ ¬ φ ) } ⊢ ¬ φ by the ¬-in rule and lines 1 and 2.
4. { ¬ ( φ ∨ ¬ φ ) , ¬ φ } ⊢ φ ∨ ¬ φ by the ∨-in rule.
5. { ¬ ( φ ∨ ¬ φ ) , ¬ φ } ⊢ ¬ ( φ ∨ ¬ φ ) by rule R3.
6. { ¬ ( φ ∨ ¬ φ ) } ⊢ ¬ ¬ φ by the ¬-in rule and lines 4 and 5.
7. { ¬ ¬ φ ) } ⊢ φ by the ¬-out rule.
8. { ¬ ( φ ∨ ¬ φ ) } ⊢ φ by rule R2 and lines 6 and 7.
9. { } ⊢ ¬ ¬ ( φ ∨ ¬ φ ) by the ¬-in rule and lines 3 and 8.
10. { ¬ ¬ ( φ ∨ ¬ φ ) } ⊢ φ ∨ ¬ φ by the ¬-out rule.
11. { } ⊢ φ ∨ ¬ φ by by rule R2 and lines 9 and 10.
Line 11 above corresponds to another rule we frequently use in everyday mathematics, namely "every statement is either true or false". This is the law of the excluded middle. But we did not have to formalize it as one of our deduction rules because, as we just saw, it is justified by the rules we chose.

In general, a justification of length n is a finite sequence ( ( Γ0 , ψ0 ) , … , ( Γn , ψn ) ) such that, for every j ≤ n, Γj ⊢ ψi follows from Γi ⊢ ψi for i < j and a deduction rule. We define Σ ⊢ φ iff there is such a justification with Γn equal to Σ and ψn equal to φ. In this case, we say that φ is deducible from Σ and φ is theorem of Σ.

We remark that some of the names of the mathematical objects we are studying are words that we will continue to use in the usual way in English. This leads to slightly odd sentences such as, "Here is a deduction that there is a deduction from the theory Σ of the sentence φ." If we wanted to avoid using the same expressions in different ways, we could add the word "formal" in key places to obtain, "Here is a deduction that there is a formal deduction from the formal theory Σ of the formal sentence φ." Later, when we study other kinds of languages, we could also add the word "propositional" to keep things crystal clear.

### § 2.5   Deduction vs. truth

Intuitively, the next result says that the deduction rules are sound in the sense that whatever you deduce really is a consequence of your theory. The result has a more substantial converse that we will get to later in this section.

#### Soundness Theorem 2.3

Assume Σ ⊢ ψ. Then Σ ⊨ ψ.

#### Sketch of Theorem 2.3

We easily check that each of the deduction rules remains true if we replace ⊢ by ⊨.

QED

(You are asked to complete the proof of Theorem 2.3 in Exercise 2.9.)

#### Finiteness of Deductions Lemma 2.4

Suppose Σ ⊢ φ.

Then there is a finite Δ ⊆ Σ such that Δ ⊢ φ.

#### Sketch of Lemma 2.4

Use induction on the lengths of justifications. Here are the key points.
• Some of the deduction rules do not mention Σ. They only mention specific finite theories.
• For the "in and out" rules that mention Σ, if theories on the left of the word "implies" are finite, then so are the theories on the right.
• With regard to rule R1, note that if Δ' is a finite subset of Δ and Δ ⊆ Σ, then Δ' is a finite subset of Σ.
• For rule R2, suppose we have finite subsets Δi of Σ such that Δi ⊢ φi and { φi ∣ i < n } ⊢ ψ.

Let Δ be the union of Δi for i < n.

Then Δ is a finite subset of Σ and Δ ⊢ φi for all i < n by rule R1.

By rule R2, Δ ⊢ ψ.

• We can ignore rule R3 for reasons explained in Example 2.B.

QED

(You are asked to complete the proof of Lemma 2.4 in Exercise 2.10.)

Here are especially important properties that a theory might have.

• Σ is consistent iff ⊥ is not a theorem of Σ.
• Σ is complete iff for every sentence φ, either Σ ⊢ φ or Σ ⊢ ¬ φ.

#### Lemma 2.5

Let Σ be a theory. The following are equivalent.

1. Σ is inconsistent.
2. For every sentence φ, Σ ⊢ φ.
3. For some sentence φ, Σ ⊢ φ and Σ ⊢ ¬ φ.

#### Proof of Lemma 2.5

That 1 implies 2 follows from the ⊥-out and R2 rules.

Obviously, 2 implies 3.

Assume 3.

Then Σ ∪ { ¬ ⊥ } ⊢ φ and Σ ∪ { ¬ ⊥ } ⊢ ¬ φ by rule R1.

Hence, Σ ⊢ ¬ ¬ ⊥ by the ¬-in rule.

Thus, Σ ⊢ ⊥ by the ¬-out rule.

Therefore, 1 holds.

QED

#### Lemma 2.6

Let Σ be a consistent theory and φ be a sentence.

Then either Σ ∪ { φ } is consistent or Σ ∪ { ¬ φ } is consistent (or both).

#### Proof of Lemma 2.6

Suppose both Σ ∪ { φ } and Σ ∪ { ¬ φ } are inconsistent. By Lemma 2.5, for any sentence ψ,
• Σ ∪ { φ } ⊢ ψ,
• Σ ∪ { φ } ⊢ ¬ ψ,
• Σ ∪ { ¬ φ } ⊢ ψ and
• Σ ∪ { ¬ φ } ⊢ ¬ ψ.
By the ¬-in rule,
• Σ ⊢ ¬ φ and
• Σ ⊢ ¬ ¬ φ.
By Lemma 2.5, Σ is inconsistent.

QED

#### Complete Extensions Lemma 2.7

Let Σ be a consistent theory.

Then there is a consistent theory Γ ⊇ Σ such that for every sentence φ, either φ belongs to Γ or ¬ φ belongs to Γ.

In particular, every consistent theory has a complete consistent extension.

#### Proof of Lemma 2.7

The set of all sentences is countable by Lemma 2.2.

Say { φ ∣ φ is a sentence } = { φn ∣ n = 0 , 1 , 2 , … }.

Using Lemma 2.6, recursively define an infinite sequence of consistent theories

Σ = Γ0 ⊆ Γ1 ⊆ ⋅ ⋅ ⋅ ⊆ Γn ⊆ ⋅ ⋅ ⋅

such that Γn+1 is either Γn ∪ { φn } or Γn ∪ { ¬ φn }.

Let Γ be the union of these theories.

Clearly Γ is complete.

For contradiction, suppose that Γ is inconsistent.

That is, Γ ⊢ ⊥.

By Lemma 2.5, there is a finite Δ ⊆ Γ such that Δ ⊢ ⊥.

Pick a natural number n large enough that Δ ⊆ Γn.

By rule R1, Γn ⊢ ⊥.

Hence Γn is inconsistent, which is a contradiction.

QED

#### Model Existence Theorem 2.8

Assume Σ is a consistent theory. Then Σ has a model.

#### Proof of Theorem 2.8

By Lemma 2.7, there is a complete consistent theory Γ ⊇ Σ such that, for every sentence φ, at least one of φ and ¬ φ belongs to Γ.

To prove Theorem 2.8, it suffices to show that Γ has a model because if A ⊨ Γ, then A ⊨ Σ.

Claim A. For every sentence φ, φ belongs to Γ iff ¬ φ does not belong to Γ.

Should Claim A fail, there would be a sentence φ such that both φ and ¬ φ belong to Γ. But then Γ would be inconsistent by Lemma 2.5.

Claim B. Every theorem of Γ belongs to Γ.

Should Claim B fail, there would be a sentence φ such that Γ ⊢ φ and ¬ φ belongs to Γ, hence Γ ⊢ ¬ φ. But then Γ would be inconsistent by Lemma 2.5.

Define a structure A by setting A ( Pn ) = 1 iff Pn belongs to Γ. The following claim completes the proof of Theorem 2.8.

Claim C. For every sentence φ, TruthA ( φ ) = 1 iff φ belongs to Γ.

The proof of Claim C is by induction on the complexity of φ using Lemma 2.1. Here are the key points.

• TruthA ( ⊤ ) = 1 and, by Claim B, ⊤ belongs to Γ.
• TruthA ( Pn ) = 1 iff A ( Pn ) = 1 iff Pn belongs to Γ.
• As the induction hypothesis, assume that Claim C holds for φ and ψ.

• By the induction hypothesis and Claim A, TruthA ( ¬ φ ) = 1 iff TruthA ( φ ) = 0 iff φ does not belong to Γ iff ¬ φ belongs to Γ.
• By the induction hypothesis and Claim B, TruthA ( φ ∧ ψ ) = 1 iff TruthA ( φ ) = 1 and TruthA ( ψ ) = 1 iff φ and ψ belong to Γ iff φ ∧ ψ belongs to Γ.
• Corresponding statements about φ ∨ ψ, φ → ψ and φ ↔ ψ.

QED

The next result is the converse of Soundness Theorem 2.3. Intuitively, it says that the system of deduction rules is complete in the sense that every logical consequence of a theory can be deduced. (The word "complete" is used many different ways!)

#### Completeness Theorem 2.9

Assume Σ ⊨ φ. Then Σ ⊢ φ.

#### Proof of Theorem 2.9

Assume Σ ⊬ φ .

We claim that Σ ∪ { ¬ φ } is consistent.

Otherwise, by Lemma 2.5, for some sentence ψ, Σ ∪ { ¬ φ } ⊢ ψ and Σ ∪ { ¬ φ } ⊢ ¬ ψ.

By the ¬-in rule, Σ ⊢ ¬ ¬ φ.

By the ¬-out and R1 rules, Σ ⊢ φ.

By Theorem 2.8, there is a model A of Σ ∪ { ¬ φ }.

Then A is a model of Σ but not a model of φ.

Therefore Σ ⊭ φ .

QED

There are useful principles in mathematics that say a certain kind of object has a certain property if all of its small subobjects have the property. Often, these are called "compactness" principles.

#### Compactness Theorem 2.10

Let Σ be a theory. Assume that every finite subtheory of Σ has a model. Then Σ has a model.

#### Proof of Theorem 2.10

By Theorem 2.8, it is enough to show that Σ is consistent. Suppose otherwise. By Lemma 2.4, there is a finite Δ ⊆ Σ such that Δ is inconsistent. So Δ ⊢ ⊥. By Soundness Theorem 2.3, Δ ⊨ ⊥. By assumption, Δ has a model. Say A ⊨ Δ. Then A ⊨ ⊥. This is a contradiction because, by definition, no structure is a model of ⊥.

### § 2.6   A proof system

Some parts of everyday mathematical proofs boil down to nothing more than checking truth tables. After enough practice, we end up considering such parts of proofs to be routine. Even a computer can verify validity using truth tables! So it is reasonable to offer an alternative to our deduction system that takes this idea into account. To keep things straight, we call it a proof system.

A proof from a theory Σ is a finite sequence of sentences ( φ0 , … , φn ) such that for every k ≤ n,

• either φk is valid,
• or φk belongs to Σ,
• or there are i , j < k such that φj is the sentence φi → φk
We will use the notation Σ ⊢p ψ to mean that there is a proof as above with φn equal to ψ.

#### Theorem 2.11

Σ ⊢p φ   iff   Σ ⊢ φ

#### Proof of Theorem 2.11

Left-to-right

We prove by induction on n that if ( φ0 , … , φn ) is a proof from Σ, then Σ ⊢ φn.

If φn is valid, then { } ⊨ φn, so Σ ⊨ φn, hence Σ ⊢ φn by Theorem 2.9.

If φn belongs to Σ, then Σ ⊢ φn by deduction rule R3.

Finally, suppose there are i , j < n such that φj is the sentence φi → φn.

By the induction hypothesis, we know Σ ⊢ φi and Σ ⊢ φi → φn.

By the →-out deduction rule (modes ponens), { φi , φi → φn } ⊢ φn.

By deduction rule R2, Σ ⊢ φn.

Right-to-left

It is enough to show that each of the deduction rules remains true if we replace ⊢ by ⊢p.

We do this for some of the rules and leave the rest as an exercise.

⊤-in

⊤ is valid so ( ⊤ ) is a proof from { } of ⊤.

⊥-out

( ⊥ , ⊥ → φ , φ ) is a proof from { ⊥ } of φ.

¬-out

(¬ ¬ φ , ¬ ¬ φ → φ , φ ) is a proof from { ¬ ¬ φ } of φ.

∧-in

( φ , ψ , φ → ( ψ → ( φ ∧ ψ ) ) , ψ → ( φ ∧ ψ ) , φ ∧ ψ ) is a proof from { φ , ψ } of φ ∧ ψ.

∧-out

Use ( φ ∧ ψ , ( φ ∧ ψ ) → φ , φ ) and ( φ ∧ ψ , ( φ ∧ ψ ) → ψ , ψ ).

∨-in

Use ( φ , φ → ( φ ∨ ψ ) , φ ∨ ψ ) and ( ψ , ψ → ( φ ∧ ψ ) , φ ∨ ψ ).

→-out

Use ( φ , φ → ψ , ψ ).

→-in

Let ( ψ0 , … , ψm ) be a proof from Σ ∪ { φ }.

We must find a proof from Σ of φ → ψm.

If ψm is either φ or valid, then φ → ψm is valid and ( φ → ψm ) is a proof from Σ of φ → ψm.

If ψm belongs to Σ, then ( ψm , ψm → ( φ → ψm ) , φ → ψm ) is a proof from Σ of φ → ψm.

Finally, suppose that there are i,j < m such that ψj is ψi → ψm.

By induction, there are proofs from Σ of φ → ψi and φ → ( ψi → ψm ).

Concatenate these two proofs (in either order) then concatenate by the following additional sentences:

1. ( φ → ψi ) → ( ( φ → ( ψi → ψm) ) → ( φ → ψm ) )
2. ( φ → ( ψi → ψm) ) → ( φ → ψm )
3. φ → ψm
in order to obtain a proof from Σ of φ → ψm.

QED