Topic Summary

In Section 1 of this topic we introduced our derivation system for quantification theory. In 1.1 we noted that:
 

Use of Sentential Logic

All rules of sentential logic may be used, and both indirect and conditional proof may be used.

In section 1.2 we introduced two rules which appeal to the 'meaning' of the internal structure of our quantificational sentences. The first was a limited version of universal instantiation .
 

Limited Universal Instantiation (ui)

From: ( a ) S a
To: S b

where b is any individual constant, and b replaces all occurrences of a in S a that were bound by ( a ).

Universal instantiation appeals to the fact that what is true of everything is true of any particular thing. We then introduced existential generalization :
 

Existential Generalization (eg)

From: S b
To: ( $ a ) S a

where b is any individual constant and a replaces some or all occurrences of b in S b , provided those occurrences of b are not in the scope of a quantifier ( a ) or ( $ a ) already occurring in S b .

This appeals to the fact that if a particular thing has some feature then there is something with that feature.

In 1.3 we introduced our quantifier exchange rules.
 

Quantifier Exchange (qe)

From: ~( a ) p               From: ( $ a )~ p

To: ( $ a )~ p             To: ~( a ) p

From: ( a )~ p              From: ~( $ a ) p

To: ~( $ a ) p             To: ( a )~ p

In Section 2 we extended our system in order to enable us to be able to show a broader class of arguments to be valid. In 2.1 we extended universal instantiation and introduced universal generalization.
 

Extended Universal Instantiation (ui)

From: ( a ) S a

To: S b

where:

(1) b is any individual constant or variable.
(2) if b is a constant then it replaces all occurrences of a bound by ( a ).
(3) if b is a variable, then it does not occur in   S a and replaces all occurrences of a bound by ( a ).

This version, as opposed to our initial one, allows us to introduce free variables. We then turned to universal generalization :
 

Universal Generalization (ug)

From: S a

where S a is not an assumption and a is a variable that does not occur free in any earlier undischarged assumption.

To: ( b ) S b

where b is an individual variable that does not occur in S a and b replaces all occurrences of a in S a .
 

We then turned, in 2.2 to a new mode of proof, one which we called existential instantiation :
 

Existential Instantiation (ei)

( $ a ) S a

          S b

.

.

.

          q (terminated)

q (discharged)

where b is a constant which does not occur in any accessible line and q does not contain any occurrence of b.

We noted that it was extremely important to observe the restrictions placed on the use of this rule.

In 2.3 we provided some examples of derivations along with some further warnings regarding mistakes to avoid. In 2.4 we turned to identity, introducing the rules necessary to complete derivations which rely upon its special features:
 

Reflexive Introduction (ri)

At any point

( a) I aa

may be introduced as a line.

Identity (=)

From
          S a and I ab           S a and I ba
To:
          S b                     S b

In 2.5 we noted that we could using this system prove theorems in precisely the same way as we could in Topic 7.