Part Of: Logic sequence
Content Summary: 500 words, 5 min read

Introduction

Logical systems like IPL have the following ingredients:

• A proposition is an atomic statement that can acquire a truth value.
• A connective takes atomic propositions, and melds them into a composite.

We can label propositions in the language of verification.

• ↑ represents conjecture: propositions that require verification
• ↓ represents knowledge: propositions that can be used for verification.

Introduction and elimination rules can be expressed in this language:

Elimination rules tend to “point down”; introduction rules point up. Roughly, deduction involves applying such rules until the paths meet:

Enough theory! Let’s see how this works in practice.

Exercise One: Implication Exploration

Given A ⊃ (B ⊃ C), show that  (A ⊃ B) ⊃ (B ⊃ C).

We can visualize the challenge as follows. The red line indicates common knowledge.

First, let’s apply elimination on the premises:

Next, let’s apply introduction on the conclusion:

Are we done? No: we have not verified A↑ and B↑. If we had, they would have a red line over them.

To finish the proof, we need to invoke our introduction-rule assumptions.

Proving A↑ is trivial. Proving B↑ requires combining assumptions via elimination.

Done. 🙂 Good work!

Exercise for the Reader

Prove the converse is true. Given (A ⊃ B) ⊃ (B ⊃ C), show that A ⊃ (B ⊃ C).

Example 2: Distributivity

In arithmetic, distributivity refers to how addition and multiplication can interleave with one another. It requires that a + (b * c) = (a*b) + (a*c). For example:

• 2 * (4+5) = 2 * 9 = 18
• (2*4) + (2*5) = 8 + 10 = 18

Are logical conjunction and disjunction distributive? Let’s find out!

First, let’s introduce conjunction on the conclusion.

Here we reach an impasse. We need to introduce disjunction elimination on the premise. But what should we choose for C?

Let’s set C = A or B.

Filling in the gaps is straightforward. On the right, we eliminate conjunction and retain B. Then we introduce disjunction on both sides.

Here is where I originally got stuck. How can we use disjunction elimination?

The way forward becomes easier to grasp, when you remember:

• We can use knowledge as many times as we like.
• The symbols in the rule schematics are arbitrary.

Let’s set the arbitrary elimination symbol “C”  equal to A or C:

From here, the solution is straightforward.

Exercise for the Reader

Prove the converse is true. Given (A ⊃ B) ⊃ (B ⊃ C), show that A ⊃ (B ⊃ C).

Takeaways

In this post, we saw worked examples of deduction. Specifically:

• Given A ⊃ (B ⊃ C),  show that  (A ⊃ B) ⊃ (B ⊃ C).
• Given A ∨ (B ∧ C), show that (A ∨ B) ∧ (A ∨ C).

The best way to learn is practice. For the interested reader, I recommend these exercises:

• Given (A ⊃ B) ⊃ (B ⊃ C), show that A ⊃ (B ⊃ C).
• Given (A ∨ B) ∧ (A ∨ C), show  that A ∨ (B ∧ C).

In the latter exercise, you must also “get creative” on how to use disjunction elimination. Instead of choosing an arbitrary C, you must set A^B to a useful value.

… still stuck? Okay, see solution here. 🙂

Until next time.