Tutorial 19 Simplified Universal Generalization.

12/26/06

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	Fy
6	(x)Fx	5 UG

This rule is a little complex in what is permitted and what not permitted. We will go into the restrictions in depth later. But even to state the rule in a simplified form requires some preliminary explanation.

Let us go back for a moment to the previous rule of Universal Instantiation UI. This lets you make steps like

5	(x)Fx
6	Fy	5 UI

and the line that is licenced by this rule, line 6, is a substitution instance of the scope of the quantifier in line 5 ie it is first Fx then modified by y being substituted for the x. Writing this abstractly, it is <scope>[<term>/<variable>] .

A preliminary, but useful though incorrect, way of thinking about Universal Generalization UG is to imagine it as being UI being done backwards or in reverse. So you start with

<scope>[<term>/<variable>]

and end up with

(<variable) <scope>

Have a look at the examples at the beginning of this tutorial. You can see them as having this form.

Let us immediately add a restriction. The notion of a <term> covers both constants and variables. And Universal Instantiation covers both-- you can infer from Everything is happy both that Bill is happy and that x is happy. But we do not want Universal Generalization to do that-- it will never be correct to infer from Bill is happy that Everything is happy. So we will immediately forbid generalizations on constants in the scope, and we will restrict it to variables in the scope.

We can now state a simplified version of the rule. There will be two further restrictions that will be introduced in a later tutorial.

The Simplified Rule of Universal Generalization UG

If a derivation contains a line of the form

n. <formula>[<variable2>/<variable1>]> <any justification>

then a line of the form

(<variable1>)<formula> 'n UG'

may be added to the derivation, <variable1> may be the same or different to <variable2>.

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) (x) (Fx.Gx) ∴ (x)Fx

(b) (x) (Fx.Gx) ∴ (y)Fy

(c) ∴ (x)Fx≡(y)Fy

(d) (x) (Fx.Gx) ∴ (y)Fy.(z)Gz

(e) ∴ (x) (Fx.Gx) ≡ (y)Fy.(z)Gz

(f) ∴ (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.