There's a general phenomenon in which you can have statements which are
not equivalent in iset.mm but which become equivalent given excluded
middle. Examples include inhabited versus nonempty, the two sides of
http://us2.metamath.org:88/ileuni/xorbin.html , apart versus not equal,
and others. The rpneg vs rpnegap example illustrates two of these -
apartness and exclusive or. There's a whole section
http://us2.metamath.org:88/ileuni/mmil.html#intuitionize about how to
turn a set.mm proof into an iset.mm proof.
I wouldn't say that higher level theorems are necessarily more similar
than lower level theorems - see for example the discussion of the
intermediate value theorem in
http://us2.metamath.org:88/ileuni/mmil.html#Bauer . Or any number of
theorems about series convergence (which I don't know off the top of my
head, but there is a bunch of stuff about modulus of convergence and such).
But I think the "would eventually become ~~ similar?" question wasn't
about "similarity" in a general sense, but specifically about double
negation. I'm not sure I have anything to offer on that. A metamath.exe
run of "search * '-. -.'" in iset.mm shows almost no hits, nor do I
remember much of the literature I've been using talking about double
negation. I've seen things like
https://en.wikipedia.org/wiki/Double-negation_translation but haven't
tried to formalize anything described there. Nor do I know how it
applies to set theory - that page stops at first-order logic and
Heyting/Peano arithmetic.
On 3/31/20 4:12 AM, savask wrote:
Very interesting. Arguably higher level theorems proofs would
eventually become ~~ similar?
I think so. For example, compare rpneg
<http://us2.metamath.org:88/mpeuni/rpneg.html> from set.mm and rpnegap
<http://us2.metamath.org:88/ileuni/rpnegap.html> from iset.mm - they
are certainly similar but not the same (maybe Jim could comment on how
well proofs of high-level theorems translate from set.mm to iset.mm).
--
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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/aed41439-97b7-48c9-aba0-3fbbfa1a942e%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/aed41439-97b7-48c9-aba0-3fbbfa1a942e%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/10940861-6fc1-8224-8e29-5b967d957973%40panix.com.
