Erik Hoversten

Logic tools

Fitch style proofs

  • This example proof is based on the Language, Proof, and Logic courseware package.
  • Hover over question mark icons to reveal a hint on how to proceed. Click the icon to reveal the next step or subproof.
  • Lines and subproofs can be optionally password protected.
1. (A → (B ∧ C)) ∧ (¬A → (¬B ∧ ¬C))
2. ¬A → ¬D
3. A
4. A → (B ∧ C)∧ Elim : 1

5. B ∧ C→ Elim : 3,4

6. C∧ Elim : 5

7. C ∨ D∨ Intro : 6
8. C ∨ D
9. ¬A
10. C
11. ¬A → (¬B ∧ ¬C)∧ Elim : 1

12. ¬B ∧ ¬C→ Elim : 9,11

13. ¬C∧ Elim : 12

14. ⊥⊥ Intro : 10,13
15. D
16. ¬D→ Elim : 2,9

17. ⊥⊥ Intro : 15,16
18. ⊥∨ Elim : 8,14-15,16-17
19. ¬¬A¬ Intro : 9-18
20. A¬ Elim : 19
21. A ↔ (C ∨ D)↔ Intro : 3-7,8-20
Download the source files

Truth tables

  • These example truth tables can be revealed one column at a time, allowing a student to practice and check their work.
Equivalence
A B A ∨ ¬B  ¬ ( ¬A ∧ B )
T T T F T F F
T F T T T F F
F T F F F T T
F F T T T T F
Consequence
A B (¬A ∨ B) ∧ ¬B ¬A
T T F T F F F
T F F F F T F
F T T T F F T
F F T T T T T
Download the source files

Categorical logic

  • These images are derived from a macro that includes functions for representing the square of opposition as well as categorical propositions and syllogisms using Venn diagrams.

The square of opposition

SVG-Viewer needed.

Categorical propositions

SVG-Viewer needed.

SVG-Viewer needed.

SVG-Viewer needed.

SVG-Viewer needed.

Categorical syllogisms

  1. No P are M
  2. All S are M
  3. ∴, No S are P

SVG-Viewer needed.
  1. Some M are P
  2. All M are S
  3. ∴, Some S are P

SVG-Viewer needed.
  1. All M are P
  2. No S are M
  3. ∴, No S are P

SVG-Viewer needed.
  1. Some M are not P
  2. Some S are M
  3. ∴, Some S are not P

SVG-Viewer needed.
Download the source files

Derivations in Predicate Logic with Anaphora

  • This presentation of derivations in PLA is presented using the reveal.js html slide presentation format.

Download the source file