Just putting in my two cents, there are certain systems in which `ph, ps |- ps` is not a valid deduction; linear logic and relevance logic are examples. If you consider an axiom to be a Metamath $a statement with no logical hypotheses, then it would be impossible to prove any statement with no hypotheses without them, since no derivation would decrease the size of the proof stack.
On Tue, Oct 22, 2019, 6:37 AM 'fl' via Metamath <[email protected]> wrote: > >> 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 > <https://groups.google.com/d/msgid/metamath/d7e47217-b0c6-4091-b551-46d827fc4c7b%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAJqce9YfJPicF7CvwUyZobvS60zc0UEtDja_vCo8N9zbsKpO7Q%40mail.gmail.com.
