gentzen

Reductio ad Absurdum

2/24/06

Absurd Introduction and Simple Reductio

9/12/06

Conditional Proof

This video shows the techniques for Conditional Proof using the downloadable application Deriver. But the techniques are exactly the same for the Proof applet running in a web page. So, the video may look slightly different to what you are looking at, but the underlying principles and approach are the same.

12/22/05

Introduction to Tactics

This video is set in the context of the downloadable program, but it applies equally well in the setting of a proof applet.

Or Introduction

Help for Tutorial 5

2013

Tutorial 5 Example: Doing a derivation

This movie shows the downloadable application being used, but the manipulations are so similar to those of the web page applet that it really covers both.

Example only

Tutorial 16 Symbolization using the quantifiers.

2013

Skill to be acquired in this tutorial:

To learn how to use the Universal and Existential Quantifiers in symbolizing propositions.

The Tutorial

In Predicate Logic there are two new logical connectives, the Universal Quantifier (∀x) and the Existential Quantifier (∃x). These are used for symbolizing certain English constructions (they also have their own rules of inference and their own semantics, which we will learn about later).

2013

Some predicate logic proofs or derivations using Gentzen calculus. Try to prove them. Click on a line to select it. Select one or more lines, apply the appropriate rule off the Rules menu. (Click 'Derive It' off the Wizard Menu, if you want help).

If you can see this, your browser does not understand IFRAME.

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)