On Sunday, February 23, 2020 at 10:24:59 AM UTC-5, 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 from
other schemes. However, any of these schemes, as well as any step of any
proof, can be immediately and trivially instantiated with an
object-language substitution, resulting in a Hilbert-style proof per your
requirements if we do that all the way back to axioms. To be pedantic I
guess one could say that Metamath "directly represents" Hilbert-style
proofs if you disagree that it "is" Hilbert-style.
In real life no one does object-language proofs, not even textbooks that
claim to work with Hilbert-style systems, because you can't reuse the
theorems for other instances, and proofs become astronomically long. Let
us say the object-language variables are v1, v2,... There is a Metamath
(set.mm) scheme called "id" that states "phi -> phi" for any wff phi. If a
proof in the style you are insisting on needed two instances of this, say
"v1 = v2 -> v1 = v2" and "v3 e. v4 -> v3 e. v4" ("e." meaning "element
of"), they would each have to be proved all over again starting from
appropriate instantiations of the starting axiom schemes.
http://us.metamath.org/mpeuni/mmset.html#2p2e4length gives an example of
this. "As an example of the savings we achieve by using only schemes, the
2p2e4 proof described in 2 + 2 = 4 Trivia above requires 26,323 proof steps
[which include the complex number construction] to be proved from the
axioms of logic and set theory. If we were not allowed to use different
instances of intermediate theorem schemes but had to show a direct
object-language proof, where each step is an actual axiom or a rule applied
to previous steps, the complete formal proof would have
73,983,127,856,077,147,925,897,127,298 (about 7.4 x 10^28) proof steps."
Norm
--
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/a102685a-1528-4d1c-822d-746f00a6be2a%40googlegroups.com.
