<p>Intuitionistic negation is perfectly constructive, because $\lnot A$ is simply an abbreviation for $A \to \bot$ (i.e., "A implies false"). You may be thinking of the principle of double-negation elimination (i.e, $\lnot\lnot A \to A$). This principle is indeed nonconstructive.</p>

<p>The reason we call intuitionistic logic constructive is that existentials and disjunctions are "constructive". Concretely, this means that:</p>

<ul>
<li>if you have a proof of $\exists x.\;A[x]$, then you can find a specific value $v$ such that $A[v]$ is provable. </li>
<li>if you have a proof of $A \vee B$, then you can either find a proof of $A$, or a proof of $B$</li>
</ul>

<p>The axiom of the excluded middle is not constructive, because it asserts $A \vee \lnot A$ for any $A$, without giving a procedure for deciding which of $A$ or $\lnot A$ is provable. </p>

<p>Double-negation elimination lets you derive the excluded middle. This is because $\lnot\lnot(P \vee \lnot P)$ is derivable in intuitionistic logic. Here's a proof, given as a lambda-term:</p>

<pre><code>f : ¬¬(P ∨ ¬P)
f : (((P ∨ (P → ⊥)) → ⊥) → ⊥ ) 
f = λk : (P ∨ (P → ⊥)) → ⊥. 
     let g : P → ⊥ = λp:P. k (inl p) in
     let h : (P → ⊥) → ⊥ = λn : P → ⊥. k (inr n) in 
     h g 
</code></pre>

<p>We can combine this with double-negation elimination to conclude that $P ∨ ¬P$ holds generally. Hence it follows that double-negation elimination is not a constructive principle in general. </p>

CC BY-SA 3.0
2014-05-09T13:50:38.997Z
I think the following statement is a bit inaccurate: `we call intuitionistic logic constructive is that existentials and disjunctions are "constructive"`. I think it is more accurate to say that it is called constructive because all logical symbols can be given constructive meanings (e.g. BHK).
Kaveh
CC BY-SA 3.0
2014-05-09T14:10:40.770Z
The idea I had in mind is that if you start with IFOL without existentials or disjunction, then double-negation elimination is an admissible rule. In this way, classical logic can be seen as a subsystem of intuitionistic logic. That is, classical logic satisfies the BHK reading, too -- it's just that we don't have any connectives with the existence property, and so it's not super interesting.
Neel Krishnaswami
CC BY-SA 3.0
2014-05-09T14:14:57.607Z
Another way of putting this is that the Goedel-Gentzen translation of classical logic into intuitionistic logic is the identity for $\forall, \to$ and $\land$.
Neel Krishnaswami
CC BY-SA 3.0
2014-05-09T15:13:04.840Z
"Absurdity ⊥ (contradiction) has no proof; a proof of ¬A is a construction which transforms any hypothetical proof of A into a proof of a contradiction." It seems to me that proof in this interpretation is like a platonic object.
Shahab
CC BY-SA 3.0
2014-05-09T15:16:28.090Z
Above interpretation is from here: http://plato.stanford.edu/entries/intuitionistic-logic-development/
Shahab
CC BY-SA 3.0
2014-05-09T15:19:37.547Z
Above interpretation is from here: http://plato.stanford.edu/entries/intuitionistic-logic-development/
Shahab
CC BY-SA 3.0
2014-05-09T21:42:39.007Z
@Shahab: No, it's not a platonic object. Note that (a) there are no proofs of $\bot$, and (b) a proof of $A \to \bot$ must transform every proof of $A$ into a proof of $\bot$. Hence the only time $A \to \bot$ is derivable is if there are no proofs of $A$, either -- because in this case a null construction will work!
Neel Krishnaswami
CC BY-SA 3.0
2014-05-10T04:56:43.680Z
Neel, my point is that the reason IL is called constructive is not because of EP and DP. There are non-constructive logics that satisfy both of them. Furthermore, these properties were shown to hold for say HA long after the constructive label for it.
Kaveh
CC BY-SA 3.0
2014-05-09T13:07:01.020Z
2014-05-09T13:07:01.020Z
Neel Krishnaswami
<p>Intuitionistic logic is not symmetric regarding truth and falsity.
There primary notion in intuitionistic logic is constructive truth and proofs not constructive falsity and refutation:
a statement is true if there is a proof for it.
And then we discuss various ways of constructions of proofs.
We don't discuss when a statement is false or how to construct a refutation.</p>

<p>We can easily build a dual logic of refutations in place of proofs.
This was noted in the literature by some students of L.E.J. Brouwer 
(it has been years since I have looked at these, 
I will add references if I recall them).</p>

<p>There are also further refinements of intuitionistic logic like linear logic which restore symmetry between truth and falsity.</p>

<p><strong>Intuitionist negation is constructive</strong> but pay attention to the meaning of the intuitionistic negation. 
It is not the same negation as classical one. 
Asserting the statement $\lnot p$ means that </p>

<blockquote>
  <p>we have a <em>construction</em> that transforms any proof of $p$ to a proof of $\not$ (absurdity).</p>
</blockquote>

<p>If $\bot$ has a proof then every statement has a proof by the $\bot$ rule
(there is a restriction of intuitionistic logic that treats $\bot$ 
simply as an arbitrary atomic proposition called minimal logic).</p>

<p>So $\lnot p$ does not meant that $p$ is false, 
it means that it can never be true.
To understand the distinction we should think in the constructive terms not platonic terms.
$p$ not true means we have not constructed a proof of $p$.
$\lnot p$ means no one can ever construct a proof of $p$ and 
we have a construction showing that.</p>

<p>In constructive mathematics 
(in the general sense, not in the sense of constructive theories) 
a proof is not a formal object according 
to some system of fixed rules.
It is a construction.
It is a primary notion that 
need not be further explained in terms of sets or linguistic objects
(though there the meaning of logical symbols are closely related to 
the rules of their manipulation by design of those rules).
The rules of proof construction are not limited to 
what is considered to be acceptable at the moment.
We have to consider the possibility that 
tomorrow someone may come up with a new kind of constructing proofs.</p>

<p>The intuitionist negation is constructive 
because it is shown by constructing a particular kind of proof, 
it is not shown simply by <em>nonexistence</em> of proofs or objects.
To show that $\lnot p$ holds it is not enough that you show there are no proofs for $p$,
you have to give a construction that shows that there cannot a proof for $p$ ever.</p>

CC BY-SA 3.0
2014-05-11T05:13:40.777Z
Is construction in constructive mathematics like set in set theory? I think that set in set theory is a primary notion.
Shahab
CC BY-SA 3.0
2014-05-11T05:51:36.987Z
Yes. If you want to learn more I would suggest reading Troelstra and van Dalen's "constructive mathematics" and Michael Beeson's "Foundations of Constructive Mathematics".
Kaveh
CC BY-SA 3.0
2014-05-10T05:19:24.477Z
2014-05-10T05:36:05.843Z
2014-05-10T05:36:05.843Z
Kaveh
<p>Can someone simply describe why intuitionistic negation is
<br>
not constructive and why intuitionistic proof is constructive?</p>

<blockquote>
  <blockquote>
    <p>in intuitionistic logic the notion of falsity has a 'subordinate' status,
    <br>
    i.e. intuitionistic logic essentially rests upon a certain disparity between verification
    <br>
    and falsification in favor of verification. Unlike intuitionistic truth, intuitionistic
    <br>
    falsity is a non-constructive notion representing simply a non-truth of a sentence"</p>
  </blockquote>
</blockquote>

<p>That is a part of paper entitle "Dual Intuitionistic Logic and a Variety of Negations:
<br>
The Logic of Scientific Research" by Yaroslav Shramko.</p>

CC BY-SA 3.0
2014-05-10T05:01:18.363Z
Please don't edit question fundamentally after it has been answered. Take more time to phrase the question you really want to ask, if you ware revising too extensively it is sign you have not spend enough time to think about and formulate your question.
Kaveh
CC BY-SA 3.0
2014-05-10T09:41:38.793Z
Voting to close as an off-topic cross-post: http://philosophy.stackexchange.com/questions/11448/why-intuitionistic-negation-is-nonconstructive
Niel de Beaudrap
<constructive-mathematics>
Why is intuitionistic negation nonconstructive?
Shahab
# Why is intuitionistic negation nonconstructive?

(Asked by: username_0 on 2014-05-09)

Can someone simply describe why intuitionistic negation is
  
not constructive and why intuitionistic proof is constructive?

> > in intuitionistic logic the notion of falsity has a 'subordinate' status,
> >   
> > i.e. intuitionistic logic essentially rests upon a certain disparity between verification
> >   
> > and falsification in favor of verification. Unlike intuitionistic truth, intuitionistic
> >   
> > falsity is a non-constructive notion representing simply a non-truth of a sentence"

That is a part of paper entitle "Dual Intuitionistic Logic and a Variety of Negations:
  
The Logic of Scientific Research" by Yaroslav Shramko.

**Tags:** constructive-mathematics
> **Comments:**
> **username_1**: Please don't edit question fundamentally after it has been answered. Take more time to phrase the question you really want to ask, if you ware revising too extensively it is sign you have not spend enough time to think about and formulate your question.  
> **username_2**: Voting to close as an off-topic cross-post: http://philosophy.stackexchange.com/questions/11448/why-intuitionistic-negation-is-nonconstructive  

---

## 2 answers

### Answer by username_3 on 2014-05-09. Score: 8

Intuitionistic negation is perfectly constructive, because $\lnot A$ is simply an abbreviation for $A \to \bot$ (i.e., "A implies false"). You may be thinking of the principle of double-negation elimination (i.e, $\lnot\lnot A \to A$). This principle is indeed nonconstructive.
The reason we call intuitionistic logic constructive is that existentials and disjunctions are "constructive". Concretely, this means that:

if you have a proof of $\exists x.\;A[x]$, then you can find a specific value $v$ such that $A[v]$ is provable. 
if you have a proof of $A \vee B$, then you can either find a proof of $A$, or a proof of $B$

The axiom of the excluded middle is not constructive, because it asserts $A \vee \lnot A$ for any $A$, without giving a procedure for deciding which of $A$ or $\lnot A$ is provable. 
Double-negation elimination lets you derive the excluded middle. This is because $\lnot\lnot(P \vee \lnot P)$ is derivable in intuitionistic logic. Here's a proof, given as a lambda-term:
f : ¬¬(P ∨ ¬P)
f : (((P ∨ (P → ⊥)) → ⊥) → ⊥ ) 
f = λk : (P ∨ (P → ⊥)) → ⊥. 
     let g : P → ⊥ = λp:P. k (inl p) in
     let h : (P → ⊥) → ⊥ = λn : P → ⊥. k (inr n) in 
     h g 

We can combine this with double-negation elimination to conclude that $P ∨ ¬P$ holds generally. Hence it follows that double-negation elimination is not a constructive principle in general.

> **Comments:**
> **username_1**: I think the following statement is a bit inaccurate: `we call intuitionistic logic constructive is that existentials and disjunctions are "constructive"`. I think it is more accurate to say that it is called constructive because all logical symbols can be given constructive meanings (e.g. BHK).  
> **username_3**: The idea I had in mind is that if you start with IFOL without existentials or disjunction, then double-negation elimination is an admissible rule. In this way, classical logic can be seen as a subsystem of intuitionistic logic. That is, classical logic satisfies the BHK reading, too -- it's just that we don't have any connectives with the existence property, and so it's not super interesting.  
> **username_3**: Another way of putting this is that the Goedel-Gentzen translation of classical logic into intuitionistic logic is the identity for $\forall, \to$ and $\land$.  
> **username_0**: "Absurdity ⊥ (contradiction) has no proof; a proof of ¬A is a construction which transforms any hypothetical proof of A into a proof of a contradiction." It seems to me that proof in this interpretation is like a platonic object.  
> **username_0**: Above interpretation is from here: http://plato.stanford.edu/entries/intuitionistic-logic-development/  
> **username_0**: Above interpretation is from here: http://plato.stanford.edu/entries/intuitionistic-logic-development/  
> **username_3**: @Shahab: No, it's not a platonic object. Note that (a) there are no proofs of $\bot$, and (b) a proof of $A \to \bot$ must transform every proof of $A$ into a proof of $\bot$. Hence the only time $A \to \bot$ is derivable is if there are no proofs of $A$, either -- because in this case a null construction will work!  
> **username_1**: Neel, my point is that the reason IL is called constructive is not because of EP and DP. There are non-constructive logics that satisfy both of them. Furthermore, these properties were shown to hold for say HA long after the constructive label for it.  

---

### Answer by username_1 on 2014-05-10. Score: 3

Intuitionistic logic is not symmetric regarding truth and falsity.
There primary notion in intuitionistic logic is constructive truth and proofs not constructive falsity and refutation:
a statement is true if there is a proof for it.
And then we discuss various ways of constructions of proofs.
We don't discuss when a statement is false or how to construct a refutation.

We can easily build a dual logic of refutations in place of proofs.
This was noted in the literature by some students of L.E.J. Brouwer
(it has been years since I have looked at these,
I will add references if I recall them).

There are also further refinements of intuitionistic logic like linear logic which restore symmetry between truth and falsity.

**Intuitionist negation is constructive** but pay attention to the meaning of the intuitionistic negation.
It is not the same negation as classical one.
Asserting the statement $\lnot p$ means that

> we have a *construction* that transforms any proof of $p$ to a proof of $\not$ (absurdity).

If $\bot$ has a proof then every statement has a proof by the $\bot$ rule
(there is a restriction of intuitionistic logic that treats $\bot$
simply as an arbitrary atomic proposition called minimal logic).

So $\lnot p$ does not meant that $p$ is false,
it means that it can never be true.
To understand the distinction we should think in the constructive terms not platonic terms.
$p$ not true means we have not constructed a proof of $p$.
$\lnot p$ means no one can ever construct a proof of $p$ and
we have a construction showing that.

In constructive mathematics
(in the general sense, not in the sense of constructive theories)
a proof is not a formal object according
to some system of fixed rules.
It is a construction.
It is a primary notion that
need not be further explained in terms of sets or linguistic objects
(though there the meaning of logical symbols are closely related to
the rules of their manipulation by design of those rules).
The rules of proof construction are not limited to
what is considered to be acceptable at the moment.
We have to consider the possibility that
tomorrow someone may come up with a new kind of constructing proofs.

The intuitionist negation is constructive
because it is shown by constructing a particular kind of proof,
it is not shown simply by *nonexistence* of proofs or objects.
To show that $\lnot p$ holds it is not enough that you show there are no proofs for $p$,
you have to give a construction that shows that there cannot a proof for $p$ ever.

> **Comments:**
> **username_0**: Is construction in constructive mathematics like set in set theory? I think that set in set theory is a primary notion.  
> **username_1**: Yes. If you want to learn more I would suggest reading Troelstra and van Dalen's "constructive mathematics" and Michael Beeson's "Foundations of Constructive Mathematics".  

---

