On Monday, February 24, 2020 at 11:31:45 AM UTC-5, Ken Kubota wrote: > > My comment on Kevin Buzzard's intervention: > https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ >
(I don't know why Google doesn't let me respond to that post, so I'm responding here.) On Feb. 23 Ken Kubota wrote: ... > (Note that Metamath isn't really Hilbert-style, in my opinion, since it > can express metatheorems. It seems to start directly at a higher level, > like all logical frameworks. > A true Hilbert-style system consists only of the (mathematical) object > language. So I disagree with Mario Carneiro at this point: > https://groups.google.com/d/msg/metamath/DRMh8ZPA6Mo/10_2n9pfDgAJ ) .... I think this is somewhat quibbling. Yes, Metamath proves schemes fromother schemes. However, any of these schemes, as well as any step of any proof, -- 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/ead0f54c-e7ef-47a0-b20e-ef0b4dbeec7e%40googlegroups.com.
