Tutorial 19 Universal Generalization.

The Tutorial

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

5			Fx
6			(∀x)Fx	5 UG

 

5			Fa
6			(∀x)Fa	5 UG

 

5			Fx
6			(∀z)Fx	5 UG

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)

Proofs

Your browser is not displaying the Deriver applet. Try downloading Deriver itself by clicking on the link elsewhere on the page.

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

Easy Deriver Documentation ©1991-2008 Martin Frické, SoftOption™ Ltd (NZ). Easy Deriver is formed out of Deriver(Generic) Program Units. Deriver(Generic) Program Units ©1987-2008 Martin Frické, SoftOption™ Ltd (NZ). Licenced to SoftOption™ Ltd (NZ).

Should you find any bugs in Easy Deriver, please tell us about them.  (Try to reproduce them, then note their exact symptoms. Send the information to support(at)SoftOption.Us)

NO WARRANTY OR REPRESENTATION IS MADE, EITHER EXPRESSED OR IMPLIED, WITH RESPECT TO THIS SOFTWARE AND DOCUMENTATION, THEIR QUALITY, THEIR PERFORMANCE, THEIR MERCHANTABILITY, OR THEIR FITNESS FOR A PARTICULAR PURPOSE, AS A RESULT, THIS SOFTWARE IS SOLD OR OFFERED 'AS IS' AND YOU THE PURCHASER OR USER ARE ASSUMING THE ENTIRE RISK AS TO THEIR QUALITY AND TO THE SOFTWARE'S PERFORMANCE.