Tutorial 19: Universal Generalization

Logical System


The Tutorial

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



The rule is quite simple

The Rule of Universal Generalization UG

If a derivation contains a line of the form

n. <formula> <any justification>

then a line of the form

(∀<variable>)<formula> 'n UG'

may be added to the derivation, provided that <variable> is not free in the <assumptions> of the formula that is generalized (the formula of line n).

You will notice that there is a restriction on the rule-- what this is, and why it is there, will be considered in Tutorial 23.



Exercise to accompany Predicate Tutorial 9


Exercise 1(of 1)

Derive the following

(a) Fa ∴ (∀x)Fa
(b) (∀x) (Fx∧Gx) ∴ (∀x)Fx
(c) (∀x) (Fx∧Gx) ∴ (∀y)Fy
(d) ∴ (∀x)Fx≡(∀y)Fy
(e) (∀x) (Fx∧Gx) ∴ (∀y)Fy∧(∀z)Gz
(f) ∴ (∀x) (Fx∧Gx) ≡ (∀y)Fy∧(∀z)Gz
(g) ∴ (∀x) (Fx∧Gx) ≡ (∀x)Fx∧(∀x)Gx

If you decide to use the web application for the exercises you can launch it from here Deriver [Gentzen] — username 'logic' password 'logic'. Then either copy and paste the above formulas into the Journal or use the Deriver File Menu to Open Web Page with this address https://softoption.us/test/easyDeriver/CombinedExercisesEasyDGentzen.html . 


You may need to set some Preferences for this.

  • you can check that the parser is set to gentzen.