Re: [Haskell-cafe] Derive ET from DN in calculus of constructions

6 Nov
2024
6 Nov
'24
1:18 a.m.
The derivation of the double negation of ET is in line 243 of https://hub.darcs.net/olf/haskell_for_mathematicians/browse/haskell_for_logi... Then use DN on that term, as Tom Smeding suggested. Olaf

6 Nov
6 Nov
7:45 a.m.
New subject: Derive ET from DN in calculus of constructions
Thank you all for the hints and links to many interesting materials! Well, I've understood, that I need to learn more about constructive logic and natural deduction. That book was not too detailed on these topics and authors write only strictly necessary info and from the wording I understand, they assume the readers are familiar with natural deduction at least (but I'm not). So now I'm reading some lectures on these topics and then will try the proof again. Thanks for the help!
195
Age (days ago)
195
Last active (days ago)
1 comments
2 participants
participants (2)
-
Dmitriy Matrosov
-
Olaf Klinke