Logic Inference: Natural Deduction

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


Logical systems like IPL have the following ingredients:

  • proposition is an atomic statement that can acquire a truth value.
  • 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:

Logic Metalanguage- Original Rules (1)

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

IPL Inference- Schematic

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.

IPL Inference- Implication Exploration Step0

First, let’s apply elimination on the premises:

IPL Inference- Implication Exploration Step1

Next, let’s apply introduction on the conclusion:

IPL Inference- Implication Exploration Step2.png

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.

IPL Inference- Implication Exploration Step3

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

IPL Inference- Implication Exploration Step4 (2)

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!

IPL Inference- Distributivity Exploration Step0 (1)

First, let’s introduce conjunction on the conclusion.

IPL Inference- Distributivity Exploration Step1

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.

IPL Inference- Distributivity Exploration Step2.png

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

IPL Inference- Distributivity Exploration Step2 (1)

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:

IPL Inference- Distributivity Exploration Step4 (1)

From here, the solution is straightforward.

IPL Inference- Distributivity Exploration Step5 (1)

Exercise for the Reader

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


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.



Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s