> > > Finally, there are the problems of provisos. Tarski showed that in a > formalization with identity one can replace the substitutions normally made > behind the scene by formulas and thus manage the substitutions in a > transparent way in the proof itself > > And we can also design a system with no distinct variables provisos at all. It would simply be totally unmanageable by human beings because the statements would be cluttered by countless hypotheses of the " -. x = y" style.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d7e47217-b0c6-4091-b551-46d827fc4c7b%40googlegroups.com.
