CHANGE OF QUANTIFIER

Next Related Topic on Ring

Section 8.3 introduces four rules for the situation in which a ~ is either desired or found in front of a quantifier.

CQ (x)ƒx :: ~(∃x)~ƒx
CQ ~(x)ƒx :: (∃x)~ƒx
CQ (∃x)ƒx :: ~(x)~ƒx
CQ ~(∃x)ƒx :: (x)~ƒx

The CQ rules are replacement rules and hence either side can serve as the premise form with the other as the form of the conclusion. While EI, EG, UI, and UG can only be used on a quantifier which is the main operator, CQ can be used on any quantifier.

For example, ~(x)(Fx • Gx) cannot be instantiated since the ~ is the main operator instead of the (x)

First CQ has to be applied.

1. ~(x)(Fx • Gx)  
2. (∃x)~(Fx • Gx) 1 CQ
3. ~(Fa • Ga) 2 EI