Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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.

share|improve this question
2  
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 May 10 at 5:01
2  
Voting to close as an off-topic cross-post: philosophy.stackexchange.com/questions/11448/… –  Niel de Beaudrap May 10 at 9:41

2 Answers 2

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.

share|improve this answer
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). –  Kaveh May 9 at 13:50
    
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 May 9 at 14:10
    
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 May 9 at 14:14
    
"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 May 9 at 15:13
    
Above interpretation is from here: plato.stanford.edu/entries/intuitionistic-logic-development –  Shahab May 9 at 15:16

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.

share|improve this answer
    
Is construction in constructive mathematics like set in set theory? I think that set in set theory is a primary notion. –  Shahab May 11 at 5:13
    
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 May 11 at 5:51

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.