In the discussion below, Samiro mentioned ~ retbwax1, which got me looking at ~ meredith and friends: https://groups.google.com/d/msgid/metamath/bc1cdba2626540ad8582917ddcec4d74%40rwth-aachen.de
The comment in ~ meredith mentions that it's "thought to be the shortest possible axiom for propositional calculus", but then ~ merco1 and ~ merco2 go on to show ones that appear shorter. Does the ~ meredith comment still apply, and if so how is length of an axiom defined in this game? -- 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/1Z4BOFDTKFYLH.3JRDYZYNC16FE%40wilsonb.com.
