Please disregard this truncated message. Something screwy about Google. I'll repost soon.
On Monday, February 24, 2020 at 2:07:51 PM UTC-5, Norman Megill wrote: > > 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/d7159da3-0a65-4db8-a88d-1ff640b8e8a5%40googlegroups.com.
