Reverse polish notation proofs from first principles exclusively

[Guram Mikaberidze]

I am wondering if there is a way to display full RPN proof of an assertion in set.mm without relying on any previously proved theorems. I would like instead to include the proofs of the used theorems in the final RPN, which would only reference the axioms.

--Guga

[Mario Carneiro]

IIRC metamath.exe has a mechanism to show the length of such a proof, but not to calculate the proof itself. Note that these proofs get really ridiculously long (I think you need bignum arithmetic just to determine how many lines of proof there would be), so it's not practical outside toy problems.

On Wed, Apr 5, 2023 at 8:29 PM Guram Mikaberidze <guram.mi...@gmail.com> wrote:

I am wondering if there is a way to display full RPN proof of an assertion in set.mm without relying on any previously proved theorems. I would like instead to include the proofs of the used theorems in the final RPN, which would only reference the axioms.

--Guga

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/701e744f-a297-4ce4-94b5-66bf24b4991an%40googlegroups.com.

[Samiro Discher]

The mmsolitaire project (https://us.metamath.org/mmsolitaire/mms.html) might be relevant to you. (In case you are looking for a minimal proof database and didn't find this yet: https://us.metamath.org/mmsolitaire/pmproofs.txt)
There is a version linked that supports manual input on higher axioms and definitions  (https://catsarefluffy.github.io/mmsjs/unify.html). The axioms used there might not be up to date.

For automated Polish notation parsing, I am only aware of https://github.com/metamath/metamath-exe and https://github.com/xamidi/pmGenerator.

Both only support the propositional axioms ax-1, ..., ax-3 (thus far — I wrote the latter tool and might implement custom axioms in the future).

But I am not aware of any publicly available converter from (all unconditional) proofs of set.mm to PN or RPN.

I'm curious as well, though, so I'd appreciate if you let me know in case you find something.

However, once you have an unfolded proof, the algorithm to generate its condensed detachment proof (in Polish notation) is rather simple, something like this:

string DRuleParser::condensedDetachmentString(const DlProof* proof) {
auto recurse = [&](unsigned pos, stringstream& ss, const auto& me) -> void {
const DlProofReason& reason = proof->reasonAt(pos);
switch (reason.type) {
case DlProofReasonType::ModusPonens:
ss << "D";
me(reason.metadata[1], ss, me);
me(reason.metadata[0], ss, me);
break;
case DlProofReasonType::Axiom: {
unsigned axiomNumber = reason.metadata[0];
if (axiomNumber < 1 || axiomNumber > 3)
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented axiom number " + to_string(axiomNumber) + " for (" + proof->name() + ").");
switch (axiomNumber) {
case 1:
ss << "1";
break;
case 2:
ss << "2";
break;
case 3:
ss << "3";
break;
}
break;
}
case DlProofReasonType::Alias:
me(reason.metadata[0], ss, me);
break;
case DlProofReasonType::Necessitation:
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented reason type 'Necessitation' for (" + proof->name() + ").");
case DlProofReasonType::Premise:
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented reason type 'Premise' for (" + proof->name() + "). You shall not pass a conditional proof.");
case DlProofReasonType::Reference:
throw logic_error("DRuleParser::condensedDetachmentString(): Unimplemented reason type 'Reference' for (" + proof->name() + "). You shall not pass a retracted proof.");
default:
throw logic_error("DRuleParser::condensedDetachmentString(): Unknown reason type for (" + proof->name() + ").");
}
};
stringstream ss;
unsigned startPos = proof->length();
if (startPos == 0)
return "";
recurse(startPos, ss, recurse);
return ss.str();
}

The above C++ example works for propositional proofs (ax-1, ..., ax-3) only.

Note that there are some seriously long proofs in set.mm (which aims not to minimize proofs, but to minimize the overall size of the database).

Here are some that I queried (with an unpublished tool) over only the propositional proofs of set.mm (version 0.198). The fourth column is the unfolded proof length.

411. ax2   7 146802383 >\phi\imply(\psi\imply\chi)\imply(\phi\imply\psi\imply(\phi\imply\chi))
1083. merco1lem14 11 102457811 >\phi\imply\psi\imply\psi\imply\chi\imply(\phi\imply\chi)
1084. merco1lem15 3 136706393 >\phi\imply\psi\imply(\phi\imply(\chi\imply\psi))
1085. merco1lem16 5 144363881 >\phi\imply(\psi\imply\chi)\imply\tau\imply(\phi\imply\chi\imply\tau)
1086. merco1lem17 24 223234495 >\phi\imply\psi\imply\phi\imply\chi\imply\tau\imply(\phi\imply\chi\imply\tau)
1087. merco1lem18 19 476274051 >\phi\imply(\psi\imply\chi)\imply(\psi\imply\phi\imply(\psi\imply\chi))
1285. nic-luk1 23 682656735 >\phi\imply\psi\imply(\psi\imply\chi\imply(\phi\imply\chi))
1286. nic-luk2 11 297742468 >\not\phi\imply\phi\imply\phi
1287. nic-luk3 10 359490068 >\phi\imply(\not\phi\imply\psi)
1647. retbwax1 29 1770374047 >\phi\imply\psi\imply(\psi\imply\chi\imply(\phi\imply\chi))

So, for example, the D-proof of https://us.metamath.org/mpeuni/retbwax1.html alone would be 1770374047 bytes, i.e. approx 1.64 GiB.

— Samiro Discher

[Samiro Discher]

> For automated Polish notation parsing, I am only aware of [...]

Apparently I was mistaken. I meant http://us.metamath.org/downloads/drule.c, which seems is not part of metamath-exe.