3 ms·
(((x -> _|_) -> _|_) -> x) would be the type of double negative reduction. I'm not entirely sure what the type should be. Perhaps, (((x -> _|_) -> (y, y -> _|_)
by DanWaterworth 14y ago
(((x -> _|_) -> _|_) -> x) would be the type of double negative reduction. I'm not entirely sure what the type should be. Perhaps, (((x -> _|_) -> (y, y -> _|_)) -> x) is more accurate. In any case, each of the three types are equivalent.
I wanted:
(forall x. ((~x) -> x) -> x) -> (forall y. y \/ (~y))
Rather than:
(forall x. (((~x) -> x) -> x) -> x \/ (~x))
- jules 14y agoProof by contradiction goes like this: You assume ~x, and from this you derive a contradiction _|_. Then you conclude x. So from ~x -> _|_ we derive x. In other words: (~x -> _|_) -> x. That's the same as ((x -> _|_) -> _|_) -> x. But in any case, as you said, this is equivalent to (~x -> x) -> x because ~x -> x is equivalent to ~x -> _|_.
- DanWaterworth 14y agoI think strictly speaking, _|_ isn't a contradiction, it's an absurdity. (x, x -> _|_) is a contradiction.
- jules 14y agoAh I see, that's where the terminological differences came from.