Review of the Quantificational Rules.

12/26/06

The Rule of Universal Instantiation UI

If a derivation contains a line of the form

n (<variable>)<scope> <any justification>

then a line of the form

<<scope>[<term>/<variable>]> 'n UI'

may be added to the derivation, provided that <variable> is free for <term> in the <scope> ie that the substitution [<term>/<variable>] is legitimate .

The Rules 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>, provided that

a) <variable2> does not appear free in any previous line obtained by EI,
b) <variable2> does not appear free in any undischarged 'Assumed Premise' (of an open conditional proof).

The Rule of Existential Generalization EG

If a derivation contains a line of the form

n. <formula>[<term>/<variable>]> <any justification>

where <variable> is free for <term> in <formula> ie the substitution is legitimate

then a line of the form

(∃<variable>)<formula> 'n EG'

may be added to the derivation, provided that <variable> is new to <formula>.

Existential Instantiation EI

If a derivation contains a line of the form

n. (∃<variable>)<formula> <any justification>

then a line of the form

<formula>[<term>/<variable>]> n EI

may be added to the derivation, provided that <term> is new to the proof.

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.