Yes! I will have to eventually write a Lojban-aware proof explorer, but
I've gotten the stock Proof Explorer to generate some familiar-looking
pages and dumped them into the webroot. For example, ~id [0] looks just
like in the Intuitionistic Proof Explorer.
I have a few pages that have tables of proven statements; the entries in
the table should all have working hyperlinks to the proofs. (A script
checks them at build time.) For example, there's tables for the categories
Loj and Selb [1][2], which show that our logic is justifiable in 1Lab's
homotopy type theory. A typical proof *not* homomorphically borrowed from
iset.mm might look like ~mintu-sym [3] which unwraps definitions and
applies basic lemmas to justify a bit of folklore; in this case, the idea
that {mintu}'s arguments are "interchangeable" [4] according to official
definitions.
Also, unrelated, but to be clear: I just noticed that the copyright
dedications are busted. Please rest assured that I'm working in the public
domain, although I may use some aggressive copyleft to protect the build
scripts if necessary. Lojban was borne from the desire to use Loglan
without the creator's permission, and so Lojban development, just like most
of maths and logic, is done without copyright.
Peace,
~ C.
[0] https://brismu.systems/id.html
[1] https://brismu.systems/loj.html
[2] https://brismu.systems/selb.html
[3] https://brismu.systems/mintu-sym.html
[4] https://jbovlaste.lojban.org/dict/mintu
On Friday, January 3, 2025 at 1:26:03 PM UTC-8 Glauco wrote:
> Hi,
>
> Is there a page where we can see an example of a proof, similar to the
> ones shown in the Metamath Proof Explorer for *set.mm <http://set.mm>*?
>
> Here’s an example of what I mean:
> Identity Theorem <https://us.metamath.org/mpeuni/id.html>
>
> Thanks in advance!
> Glauco
>
>
--
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 visit
https://groups.google.com/d/msgid/metamath/b1abd4ce-5529-42b2-83db-23273f8c0e86n%40googlegroups.com.
