Hi all, I noticed an interesting question about Metamath on ProofAssistants StackExchange:
https://proofassistants.stackexchange.com/questions/1273/kunens-inconsistency-axiom-free-proof-on-metamath The question says "Metamath", but what is meant is really "set.mm". I have tried to answer some general Metamath related questions there in the past, but this is beyond my capabilities. Kunen's original paper is not freely accessible, but a proof of his theorem is present as theorem 1.12, page 10 of the PDF: http://math.bu.edu/people/aki/d.pdf I believe the first difficulty will be to express things like "inner model" and "elementary embedding" in set.mm. I'm reposting here in case anyone may be interested. BR, _ Thierry -- 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/e5302793-fc5c-8bc7-6ac3-f7479671d4a6%40gmx.net.
