A slight typo: near the end of my last message (**) (forall a)(forall n)[I(a) and Prov_{S_a}(A_n) --> A(n)] should be (**) (forall a)(forall n)[I(a) and Prov_{S_a}(A(n)) --> A(n)]