derivations

Roll your own derivations

2013

You may have derivations of your own that you wish to try. Just type, paste, or drag and drop, them into the panel, select your derivation, and click 'Start from selection'. [Often copy-and-paste won't work directly from a Web Page; however, usually drag-and-drop will work!]

You will need to use the correct logical symbols. Here they are

F ∴ F ∧ G ∼ ∧ ∨ ⊃ ≡ ∀ ∃ ∴ (or use the palette to produce them)

4/24/06

Tutorial 25 Exercises h

4/24/06

Tutorial 25 Exercises g

4/24/06

Tutorial 25 Exercises e

4/24/06

Tutorial 25 Exercises d

4/24/06

9/13/20

Skill to be acquired:

To understand the concepts of scope, free, bound, and free for.

Why this is useful:

The new predicate rules of inference using quantifiers have restrictions on them which are expressed in terms of these concepts.

2013

The Tutorial

Existential Instantiation permits you to remove an existential quantifier from a formula which has an existential quantifier as its main connective. It is one of those rules which involves the adoption and dropping of an extra assumption (like ∼I,⊃I,∨E, and ≡I).

The circumstance that Existential Instantiation gets invoked looks like this.

8/11/2026

The Tutorial

There is a rule for adding a Existential Quantifier. This permits the step illustrated by the following proof fragments.

8/12/26

The Tutorial

There also is a rule for adding a Universal Quantifier. This permits the step illustrated by the following proof fragments.