4 ms·

And even that is less of a problem if you take into account that they still accept: ¬¬¬¬ϕ ⇒ ¬¬ϕ

• monochromatic 11y ago
  Do they really? Why?
  • tel 11y ago
    proof : ¬¬¬¬ϕ ⇒ ¬¬ϕ proof (f : ((((a -> False) -> False) -> False) -> False)) = \ (z : a -> False) -> f (\afff -> afff (\aff -> aff z)))
  • iamcurious 11y ago
    It just follows from the axioms. They accept that a proof of ¬ p can be a proof that takes p and arrives to a contradiction. And that a contradiction is a formula and its negation. From that we can prove ¬¬¬¬p => ¬¬p. We can assume ¬p and we have to prove a contradiction. So we have to prove: ¬¬¬¬p, ¬p => _|_ Now, we know* that alpha => ¬¬alpha. So from ¬p, we can get ¬¬¬p. And from ¬(¬¬¬p) and (¬¬¬p) we arrive to _|_. *To prove alpha => ¬¬alpha, we can assume ¬alpha and arrive at a contradiction, so we would have to rpove alpha, ¬alpha => _|_ and we are done. In Natural Deduction: [¬p]1 [¬¬p]2 --------------- _|_ ----------2 ¬¬¬p ¬¬¬¬p ----------------------- _|_ -----------------------1 ¬¬p This has been generalized to translate classical theorems into constructive theorems.[1] Just like this case, though, the resulting theorems are full of double negations. [1] http://en.wikipedia.org/wiki/Double-negation_translation http://en.wikipedia.org/wiki/Double-negation_translation
  • vilhelm_s 11y ago
    It may be slightly easier to work through it for the formula ¬¬¬P ⇒ ¬P. (This also a constructive tautology, and the above formula is an instance of it, taking P = ¬ϕ). So let's prove that. Expanding the definition of ¬, we must prove (((P⇒False)⇒False)⇒False)⇒P⇒False. I.e. we are given two assumptions f : ((P⇒False)⇒False)⇒False x : P and should prove False. So we can use the assumption f, provided we can find an argument of type ((P⇒False)⇒False) to call it with. And in fact that's easy: (λg. g x). The full proof term is λf.λx. f (λg. g x) Indeed, this is a perfectly good function (so it's constructive). If we type that function into (say) a Haskell repl, the typechecker will infer an even more general type for it, but we can check that the type we wanted is an instance: ghci> :type (\f x -> f (\g -> g x)) (\f x -> f (\g -> g x)) :: (((t2->t1)->t1)->t) -> t2 -> t gchi> type Not a = (a -> False) ghci> :type (\f x -> f (\g -> g x)) :: (Not (Not (Not p)))->Not p (\f x -> f (\g -> g x)) :: (Not (Not (Not p))) -> Not p