1. Tutorial

We do problems 3.8, 3.10, 3.13, 3.19, 3.23, 3.24, 3.26, 3.27 and 3.32 for extra practice, supplementing the examples worked out in the text (Chapter 3 of GS). Of course, we use our schemata-notation from class, so we prove in each case not just a single theorem (like ¬¬p ≡ p), but a theorem-schema (like ¬¬A ≡ A).

3.8 Prove ¬¬A ≡ A (with no additional assumptions).

We also often say “Prove that ⊢ ¬¬A ≡ A”. Assuming that we know what we are doing, that is probably “OK”. But strictly speaking, we should say “metaprove that ⊢ ¬¬A ≡ A”, because “⊢ ¬¬A ≡ A” says “¬¬A ≡ A is a logical theorem”. Note that the latter statement, although correct, is not in its entirety a formula of our language—only the “¬¬A ≡ A” part of it is—hence it cannot be a “theorem”.

Now that we got the jargon straight, let us proceed:

¬¬A ≡ A
= ⟨⊢ ¬A ≡ B ≡ A ≡ ¬B was proved in class⟩
¬A ≡ ¬A

The last formula is a theorem (class: ⊢ A ≡ A). Done.

Wait a minute! If we proved in class that “⊢ A ≡ A”, how come this is as good as “⊢ ¬A ≡ ¬A”? □

3.10 Prove that ⊢ (A ≢ B) ≡ ¬A ≡ B.

It is important to note that whenever a defined connective such as ≢, ⇐, ⇍, ⇏ is involved, we do not involve it in the formal proof but first translate the informally written formula to correct form, and only then start the proof.

So, translation: We are really being asked to prove that:

⊢ ¬(A ≡ B) ≡ ¬A ≡ B

But this so! This is the axiom on distribution of ¬ over ≡. □

3.13 Prove that ⊢ ((A ≢ B) ≡ C) ≡ (A ≢ (B ≡ C)).

Translation: We are really being asked to prove that:

⊢ (¬(A ≡ B) ≡ C) ≡ ¬(A ≡ (B ≡ C))

Here it goes:

¬(A ≡ B) ≡ C

= ⟨Axiom “distribution of ¬ over ≡⟩

¬((A ≡ B) ≡ C) = ⟨Assoc. of ≡ and Leib. with formula ¬r⟩

¬(A ≡ (B ≡ C))

Done. □

3.19 Prove ⊢ A ∨ B ≡ A ∨ ¬B ≡ A. A common (fatal) error that I often see is the interpretation of the above as

A ∨ B =

A ∨ ¬B =

A

which is “way out”. None of these “=” holds!

Let’s do it then, pretending the rightmost ≡ is the last one. (What do I mean by “the last one”? Can I do that?)

A ∨ B ≡ A ∨ ¬B = ⟨Axiom: distrib. of ∨ over ≡⟩

A ∨ (B ≡ ¬B) = ⟨Leib. on A ∨ r plus ⊢ ¬A ≡ A ≡false from class⟩

A ∨ false = ⟨Class: ⊢ A ∨ false = A⟩

A

Done. □

3.23. Prove that ⊢ A ∧ A ≡ A.

Tutorial for Ch.3\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

A ∧ A ≡ A
= ⟨By “GR”⟩
A ≡ A ∨ A

The second line is an axiom (idempotent for ∨). Done. □

3.24. Prove that ⊢ A ∧ false ≡ false.

A ∧ false ≡ false = ⟨By “GR”⟩

A ≡ A ∨ false

The second line is an (logical) theorem (done in class). Done. □

3.26. Prove that A ∧ ¬A ≡ false.

A ∧ ¬A = ⟨By “GR”⟩

A ≡ ¬A ≡ A ∨ ¬A = ⟨By redundant true plus excluded middle axiom, using Leib. on A ≡ ¬A ≡ r⟩

A ≡ ¬A ≡ true = ⟨By redundant true⟩

A ≡ ¬A = ⟨By ⊢ A ≡ ¬A ≡ false from class⟩

false

Done. □

3.27. Prove that ⊢ A ∧ (A ∨ B) ≡ A.

Tutorial for Ch.3\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

A ∧ (A ∨ B)

= ⟨By “GR”⟩

A ≡ A ∨ B ≡ A ∨ A ∨ B

= ⟨Leib. on A ≡ A ∨ B ≡ r ∨ B and idemp. axiom: A ∨ A ≡ A⟩

A ≡ A ∨ B ≡ A ∨ B

= ⟨Redundant true and ⊢ A ≡ A (class) using Leib. on A ≡ r⟩

A ≡ true

= ⟨Redundant true⟩

A

Done. □

3.32. Prove that ⊢ ¬(A ∧ B) ≡ ¬A ∨ ¬B.

The only “trick” in the proof that follows is not a trick at all. We “factor” formulas (using distribution of ∨ over ≡) just as we do so with numbers. In slow motion, compare

a + a × b

= ⟨⊢ a × 1 = a on numbers, i.e., “1” is the “×-identity”⟩

a × 1 + a × b

= ⟨Distribution of × over +⟩

a × (1 + b)

with

A ≡ A ∨ B

= ⟨⊢ A ∨ false ≡ A on formulas, i.e., “false” is the “∨-identity”⟩

A ∨ false ≡ A ∨ B

= ⟨Distribution of ∨ over ≡⟩

A ∨ (false ≡ B)

Ready for the main event (which uses the immediately above “factoring” twice):

¬(A ∧ B)

= ⟨By “GR” using Leib. on ¬r⟩

¬(A ≡ B ≡ A ∨ B)

= ⟨Distribution of ¬ over ≡⟩

¬A ≡ B ≡ A ∨ B

= ⟨Leib. on ¬A ≡ r ≡ A ∨ B and ⊢ false ∨ B ≡ B (class)⟩

¬A ≡ false ∨ B ≡ A ∨ B

= ⟨Leib. on ¬A ≡ r and distrib. of ∨ over ≡⟩

¬A ≡ (false ≡ A) ∨ B

= ⟨Leib. on ¬A ≡ r ∨ B and ⊢ false ≡ A ≡ ¬A (class)⟩

¬A ≡ ¬A ∨ B

= ⟨Leib. on r ≡ ¬A ∨ B and ⊢ false ∨ B ≡ B (class)⟩

¬A ∨ false ≡ ¬A ∨ B

= ⟨Distrib. of ∨ over ≡⟩

¬A ∨ (false ≡ B)

= ⟨Leib. on ¬A ∨ r and ⊢ false ≡ A ≡ ¬A (class)⟩

¬A ∨ ¬B

Done. □