The Russell-Prawitz embedding and the atomization of universal instantiation

José Espírito Santo, Gilda Ferreira

Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system F_at, we study directly in sy…