Metamath in Metamath?

[Steven]

From metamath.pdf: "With suitable axioms and definitions, Metamath can
even describe and prove things about itself."

Does anybody know if these axioms and definitions been written in a
Metamath database yet? If not, I'd like to take a crack at it.

If it hasn't been done, are there any definitions/theorems in set.mm
or elsewhere that could potentially be adapted to represent something
like the "list" of symbols that form an expression or the "list" of
labels that form a proof?

[igblan]

Steven,

Good for you, you've decided to prove Godel's Incompleteness Theorem
(*pace*
Dark Star)!

It shouldn't take more than a few months.

The first thing you need is a proof of the Fundamantal Theorem of
Arithmetic, ie
every positive integer has a unique prime-power decomposition.

Then you can start representing wffs, axioms and theorems as Godel
numbers.

Good luck!

Cheers, Paul

[Steven]

Thanks Paul. Formulating and proving these theorems should be a fun
and educational project (not to mention that it sounds very
challenging). I think it will also help me become familiar with
Metamath and give me some useful experience with proofs.

Ultimately though, I'm not sure the Godel numbers are what I had in
mind (I could be wrong). Once I had a database of assertions that
defined Metamath (say, metamath.mm), I envisioned being able to
programmatically convert other databases into a kind of "metalevel"
representation that metamath.mm could understand.

Then I could create another database and do something like

$[ metamath.mm $]
$[ metalevel.mm $]

and go on to prove statements like

* Definition df-MyDefinition is a true definition in the sense
described on page 125 in metamath.pdf

* thm-MyTheorem is not provable from {ax-1, ax-2, ax-3}

* S is a valid "next step" in a construction C (part of a proof)

I'm going to give the Godel numbers and incompleteness theorem a try
either way, but I'm wondering, could they lead into something like
this?

Oh, one more question: what does (*pace* Dark Star) mean?


Thanks,

Steven

[Jeff Hoffman]

I played around with Hofstadter's MUI system in Metamath, not like the
examples that use def statements, but actually *in* Metamath's set
theory. I think such an approach is necessary for Godel's proof. I
bet if you can prove MU is not a theorem, you'll have many useful
constructs. Personally, I feel the mapping done by Godel-numbering is
not crucial. Any mapping will do. For me, the difficult part was
using the rec() function to define a recursively enumerated set.
Also, handling variable substitutions in the iterated function that
generates new theorems was quite nasty.

I'm a CompSci guy, so my mapping used nested pairs, a la lisp. For
example, a 4 symbol theorem would look like the set
<A, <B, <C, D>>>. Using 1st() and 2nd() [ aka cons and cddr ], a
string function that implements modus ponens might be defined. It
seemed a more natural representation than powers of primes. One does
need some extra closure/uniqueness proofs for strings, but it seemed
worth the effort. I gave up when variable substitution in MUI stopped
being fun.

The string approach might come in handy for trying to handle non-
Metamath strings. On the other hand, if what you really want is a
isomerism between Metamath and something else, traditional code/proofs
might be a better way to go. Defining an isomorphism *and* proving
it's consistent *in* Metamath looks quite huge to this bear of very
little brains*.

// * thm-MyTheorem is not provable from {ax-1, ax-2, ax-3}
If the domain is only prop calc, this feels like the satisfiability
problem (NP-hard, SAT). For prep calc and above, it seems like another
version of the impossible Turing halting problem.

// * S is a valid "next step" in a construction C (part of a proof)
This is what the program metamath.c does. Because of Curry-Howard, a
proof that S applies to C0 to yield C1 is doable. Automatically
generating such a proof seems non-trivial. It involves most of the
nasty topics mentioned.

I'd like to hear how things proceed.
Peace,
Jeff

[*] Winnie-the-Pooh and I have much in common. Usual disclaimers
apply. Sorry, I also missed the 'dark star' reference.