[Haskell-cafe] Derive ET from DN in calculus of constructions
Dmitriy Matrosov
sgf.dma at gmail.com
Fri Nov 1 13:44:51 UTC 2024
Hi.
I've reading "Type theory and formal proof, an introduction"
book and in chapter 7.4 authors say, that in constructive
logic plus either excluded third law (ET) or double negation
law (DN) we can derive the other. And then authors derive DN
from ET in calculus of constructions. But they didn't say
anything (yet?) about the vice versa: deriving ET from DN in
calculus of constructions.
I've tried to do this, but the best i can come up with is
just case analysis:
- assume, that 'a' is true, then 'a or not a' is also true
(by 'or-intro' rule).
- or if after assuming that 'a' is true we can derive
bottom, then 'not a' is true (by 'not-intro' rule).
Then using the 'or-intro' rule we again end up with 'a or (not
a)' being true.
- assume 'not a' and if we can derive bottom again, then
'not (not a)' is true. Then by using DN we again end up
with 'a' being true. etc.
I.e. I may reduce any (not.. (n times) .. not a) into either
'a' or 'not a' by using DN and function composition. Thus, i
probable can derive ET from DN using induction, but i can't
code neither induction, nor above case analysis in calculus
of constructions.
So, is it possible to derive ET from DN in calculus of
constructions? If it is, i'd appreciate not a direct answer,
but a hint on how to do this. And if it is not,
well, probably, authors will explain this later in the book
and I should just continue reading.
Thanks.
More information about the Haskell-Cafe
mailing list