David A. Wheeler asked Giovanni Mascellani about the "monster theorem": > > The final expression includes "∧ ⊤" - I would not have expected that. > > Should that be removed?
On Mon, 4 Nov 2019 17:42:39 +0100, Giovanni Mascellani wrote: > It is currently an artifact of the automatic translation from ND. Each > clause converted from ND must have the form "( ph -> ps )", even when > its context is empty, because otherwise I have to branch over the two > possible cases (there is or there is not a context) each time I want to > use or produce a clause. So when the context is empty I need to put > something, which is, of course, "T.". Adding to context is obtained by > replacing "ph" with "( ch /\ ph )", and again I do not want to make a > special rule for when I am adding to an empty context. So, in general, > the context containing ph, ps and ch will be > > ( ph /\ ( ps /\ ( ch /\ T. ) ) ) > > This and many other artifacts, like the explicit substitution > constructors, should eventually be removed (unless they are desired, in > some situation) by the program _consuming_ this proof, which is still to > be written. --- David A. Wheeler -- 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/E1iRg2e-0004cg-VE%40rmmprod07.runbox.
