> Am 24.02.2020 um 20:48 schrieb Norman Megill <[email protected]>:
>
> 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
> <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.
You argue the same way as Mario does.
My knowledge about Metamath is limited, but I believe that Mario is correct in
that the form of reasoning resembles that of a Hilbert-style system.
However, my perspective is different since my intention is to find the natural
language of mathematics (following Andrews' notion of expressiveness).
This means that (like in Andrews' Q0) metatheorems cannot be expressed directly
using the means of the formal language only.
While implementations based on Q0 (such as Cris Perdues' Prooftoys or my R0
software) use logical implication (located at the object language level) as the
key symbol of the Hilbert-style system, logical frameworks use the turnstile or
another symbols (located at the meta-language level) which denotes derivability
/ provability.
So by definition Metamath (as a logical framework / a metalogic) doesn't fit
into the definition of a Hilbert-style system in the narrow sense, which simply
reflects the fact that the design purposes are different and therefore the
language levels are.
> 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.
Exactly this is done in the R0 software implementation: it does object language
proofs only.
Instead of schemes, templates are used (*.r0t files instead of the regular *.r0
files), so you can re-use the template with different initial values and simply
include the template file.
In his 2002 textbook, Andrews carefully distinguishes meta-language proofs from
object language proofs by introducing boldface "syntactical variables"
[Andrews, 2002, p. 11].
The corresponding theorem in R0 is K8005 (H => H) and uses the logical
implication, so a direct comparison is difficult here.
But substitution may serve as an example here:
> ## Proof A6102: Peano's Postulate No. 5 for Andrews' Definition of Natural
> Numbers
>
> ## Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 262]
>
> ## .1
>
> %K8005
>
> ## use Proof Template A5221 (Sub): B --> B [x/A]
> := $B5221 %0
> := $T5221 o
> := $X5221 x{$T5221}
> := $A5221
> ((&{{{o,o},o}}_(p{{o,$S}}{{o,$S}}_(AZERO{{{o,{o,\3{^}}},^}}_t{^}{^}){$S}){o}){{o,o}}_((A{{{o,{o,\3{^}}},^}}_$S{^}){$To2S}_[\x{$S}{$S}.((=>{{{o,o},o}}_((ANSET{{{o,{o,{o,\4{^}}}},^}}_t{^}{^}){{o,$S}}_x{$S}{$S}){o}){{o,o}}_((=>{{{o,o},o}}_(p{{o,$S}}{{o,$S}}_x{$S}{$S}){o}){{o,o}}_(p{{o,$S}}{{o,$S}}_((ASUCC{{{{o,{o,\4{^}}},{o,{o,\4{^}}}},^}}_t{^}{^}){{$S,$S}}_x{$S}{$S}){$S}){o}){o}){o}]{{o,$S}}){o})
> << A5221.r0t.txt
> := $B5221; := $T5221; := $X5221; := $A5221
The line starting with "<<" includes the template file.
In the preceding lines the initial values are set (pattern: := variable value
).
In the following lines the values are unset (pattern: := variable ).
The semicolon is equivalent to the end of line.
So in fact all proofs are done at the object-language level.
> http://us.metamath.org/mpeuni/mmset.html#2p2e4length
> <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."
It is true that proofs sometimes become slow, but in the approach logical rigor
was more important than practical considerations.
Run
make A6102.r0.dbg.txt && open $_
on a Mac to see the verbose proof of the Principle of Mathematical Induction,
where each proof instance is shown (29M filesize, 624908 lines).
For comparison, the abbreviated proof (not expanding the template proofs)
obtained by
make A6102.r0.out.txt && open $_
has only a filesize of 44K and 973 lines.
In order to fulfil both philosophical and practical needs, my suggestion is a
two-step approach:
The first step focuses on logical rigor and uses the object language only.
(This is my current R0 software implementation.)
In the second step the logic is reformulated in a meta-language where
metatheorems can be expressed directly.
But it is important to separate these two steps.
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
--
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/0E7295FC-CB38-4B16-AD01-878822692E8C%40kenkubota.de.
