On 11/27/19 10:10 PM, 'ookami' via Metamath wrote:
> I'd love to look into all the different aspects of logic.
Unfortunately, I work full-time in a completely different area, and I
have simply no time to follow all the different threads. I do not even
have time to become specialized in the fields I really want to know. So
don't expect too much.
No worries, I'm not assigning homework to you or anyone else.
Just a statement about some of what is out there in case it catches
anyone's fancy.
On 11/27/19 10:10 PM, 'ookami' via Metamath wrote:
Am Donnerstag, 21. November 2019 16:38:57 UTC+1 schrieb Jim Kingdon:
...
I'll also say that if you have any interest in, or curiosity
about, intuitionistic logic, that there is low hanging fruit in
iset.mm <http://iset.mm>. Proofs that can be shortened, cases
where set.mm <http://set.mm> has a better proof which can be
copied over, probably some cases where iset.mm <http://iset.mm>
has a shorter proof which can go over to set.mm <http://set.mm>.
The work is (usually) quite similar to set.mm <http://set.mm> (a
fair number of proofs can be copied over unmodified, for example)
and there is a detailed "how to" guide at
http://us.metamath.org/ileuni/mmil.html#intuitionize
<http://us.metamath.org/ileuni/mmil.html#intuitionize>
(suggestions on making the web pages and comments clearer are also
welcome).
--
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/3f0c716d-e6f2-f949-0fd1-63306f572eca%40panix.com.
