Universal Instantiation

Next Related Topic on Ring

(x)ƒx / ƒy UI where the VARIABLE y is free in ƒy in EXACTLY those places that x is bound in ƒx by the quantifier (x)

(x)ƒx / ƒa UI where the CONSTANT a is free in ƒa in EXACTLY those places that x is bound in ƒx by the quantifier (x)

CORRECT

1.  (x)Axy
2.  Axy 1,UI

INcorrect

1. (x)(y)Axy  
2. (y)Ayy 1,UI X since the place controlled in #1 by (x) is in #2 bound by a new quantifier.

CORRECT

1. (x)Axy  
2. Ayy  1,UI

INcorrect

1. (x)(Ax ⊃ Bx)    
2. Ax ⊃ By 1,UI  X since 1 variable in #1 is replaced 2 different ways.

CORRECT

1. (y)[Aax • By]  
2. Aax • Ba 1,UI
3. Aax • Bx 1,UI
4. Aax • By 1,UI
5. Aax • Bb 1,UI