Why is intuitionistic negation nonconstructive?

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"

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

Many thanks to Mauro for highlighting exactly those parts of Shramko's paper that we need to give a more worthy answer to this interesting question. What I said previously was the standard intuitionistic story about falsity. Shramko (in the papers mentioned by Shahab and Mauro) is challenging that story, by introducing a distinction between two ways of defining what it means for a formula to be false. In this revision I want to discuss that distinction (§1) and explain why Shramko says what he says (§4).

§1. Two Definitions of Falsity

On p.10 Shramko introduces two ways of defining falsity ('T(φ)', 'F(φ)' abbreviate "φ is true/false"):

Definition 1. (Purely Semantical)        F1(φ) ≡ ¬T(φ);
Definition 2. (Semantic-Syntactical)   F2(φ) ≡ T(¬φ).

According to definition (1), sentence φ is false just in case it's not true that φ is true. He calls this the purely semantical notion of falsity. He juxtaposes that with definition (2), according to which: sentence φ is false just in case ¬φ is true. He calls this the mixed, semantic-syntactical notion of falsity because it involves the '¬' connective of the object language in the definition.

§2. Classical Falsity

He notes that in classical logic the distinction collapses. To keep things simple, let p be prime. Then:

Fact 3. |= F1(p) ↔ |= F2(p), i.e., classical logic doesn't distinguish between F1 and F2 falsities.

Proof. Here ( |= ) is the classical notion of satisfaction. An arbitrary model M satisfies F1(p) iff by (Definition 1) M doesn't satisfy p, i.e., ¬(M |= p). But that is exactly the truth-condition for M satisfying ¬p, so that means by (Definition 2) that M satisfies F2(p). Hence: |= F1(p) ↔ |= F2(p).                         ■

§3. Intuitionistic Falsity

The same theorem doesn't generally hold for intuitionistic logic. To prove that fact we'll define a version of Kripke semantics for intuitionistic logic that is very similar to the one Shramko uses. Bear with me:

Definition 3. (Intuitionistic Models) An intuitionistic Kripke model is a triple M = (W, ≤, V), where W is a set of possible worlds, V is a function from worlds to ρ(W), and ≤ is an accessibility relation that is a partial order and is hereditary in the sense that: if w ∈ V(p) and w ≤ v, then v ∈ V(p).

Given intuitionistic Kripke models we can define the intuitionistic forcing relation ( ||= ) as follows:

Definition 4. (Intuitionistic Forcing) Given an intuitionistic Kripke model M and a world w ∈ M, we say that M, w ||= φ (read: "M, w forces φ") by induction on the complexity of φ as follows:

1. M, w ¬||= ⊥               (i.e. "no world forces ⊥");
2. M, w ||= A            iff   w ∈ V(A), where A is an propositional letter;
3. M, w ||= (φ ∧ ψ)   iff   M, w ||= φ and M, w ||= ψ;
4. M, w ||= (φ ∨ ψ)   iff   M, w ||= φ or M, w ||= ψ;
5. M, w ||= (φ → ψ)  iff   ∀w ∈ W : if (w ≤ v ∧ M, v ||= φ) then M, v ||= ψ.

Now that we have the proper models and the proper notion of intuitionistic 'satisfiability', we can provide a very simple counterexample to the validity of the of the intuitionistic version of (Fact 3):

Fact 5. The following is invalid: ||= F1(p) ↔ ||= F2(p), i.e., intuitionistic logic distinguishes between F1,F2.

Proof. As a counterexample consider the intuitionistic Kripke model M = (W, ≤, V), where W is a the set {a,b}, ≤ is the set {⟨a,b⟩} (meaning that there is only one arrow, from world a to b), and V(p) = {b} (meaning that p is forced only at world b). Since (M, a) doesn't force p, by (Definition 1) we know that M, a ||= F1(p). But is it also the case that (M, a) forces ¬p? For (M, a) to force ¬p it would be necessary and sufficient for this to hold: M, a ||= (p → ⊥). By (Definition 4.5) that would hold just in case all words v s.t. a ≤ v are such that M, v ¬||= p. But there is a world, namely b, s.t. a ≤ b, but M, b ||= p; so (M, a) doesn't force ¬p, i.e., M, a ¬||= F2(p). This proves that intuitionistically, F1 and F2 falsities are not the same thing.                                                                                                            ■

§4. Shramko's Point

Given (by Fact 5) that from the intuitionistic point of view there is this distinction between purely semantical (Definition 1) and semantical-syntactical (Definition 2) falsities, Shramko asks:

Question 6. Which (among Definitions 1 and 2) is the correct notion of intuitionistic negation?

His own answer to his question is apparent from the last sentence quoted by Shahab:

Shramko's Answer. "[the] non-constructive [one] representing simply a non-truth of a sentence".

He thinks, it seems, that the correct notion of intuitionistic negation is the one given by (Definition 1), which says that a formula is false just in case it's not true. He is right to call this notion of falsity 'non-constructive', because unlike (Definition 2), this one doesn't take advantage of the strong definition of '→' in intuitionistic semantics (see Definition 4.5 above). If you read the paper mentioned by Mauro, you'll see why he chooses the weaker definition of negation. (It is philosophically motivated, and has to do with the two main accounts of intuitionistic truth: actualist and possibilist). This post is long as it is; I don't think my summary of the papers would be appropriate at this point.

I hope the foregoing discussion was intelligible enough to explain his claim that (his own definition) of "intuitionistic falsity is a non-constructive notion".

References

van Benthem, J. (2010) Modal Logic for Open Minds, Stanford, CSLI Lecture Notes #199; Chapter 20.
Holliday, W.H. (2012) Modal Reasoning, Lecture Course (Spring), UC Berkeley; Lecture 11.
Shramko, Y. (2012) "What Is a Genuine Intuitionistic Notion of Falsity?", LLP 21: 3–23.

• transforming a proof of p to a proof of q looks as though where the notion of homotopy could come in, particularly if one thinks of a proof as a 'curve' going from the axioms to p in the space of all propositions. – Mozibur Ullah May 10 '14 at 10:42
• Very nice (+1). I feel like you might appreciate unicode block 22Ax ;) – Lucas May 11 '14 at 18:56
• @Lucas Thanks! I do take advantage of the charset, but that '&models;' looks so small, I can never convince myself that it looks okay enough to use it. – Hunan Rostomyan May 11 '14 at 19:00
• It's certainly no TeX – Lucas May 11 '14 at 19:06
• @Lucas It is not very nice of them to assume that philosophy students couldn't take advantage of the beauty that is LaTeX. Thank god unicode gets processed. – Hunan Rostomyan May 11 '14 at 19:25

You can see Yaroslav Shramko, What is a Genueny Intuitionistic Notion of Falsity (Logic and Logical Philosophy, vol 21, 2012); see Abstract :

One can find two principal (and non-equivalent) versions of such a notion in the literature, namely, falsity as non-truth and falsity as truth of a negative proposition. I argue in favor of the first version as the genuine intuitionistic notion of falsity.

Page 9 :

Generally, there are two basic ways of introducing falsity into a semantic construction. One way is to interpret falsity as a complementary notion to the one of truth: “A is false” means nothing else but “A is not true”. According to another view falsity ought to be interpreted as a direct semantic representation of the syntactic notion of negation, i.e., “A is false” is understood as an abbreviation of the expression “∼A is true”. The main difference between these approaches is that in the first case falsity is defined exclusively in semantic terms (in a metalanguage), and as such is treated as a purely semantic notion; whereas in the second case falsity is introduced by means of some object language terms (namely, the connective of negation), and becomes thus of a mixed semantic-syntactic character.

Page 10 :

As it has already been mentioned, in classical logic both ways are equivalent through the standard definition of truth conditions for classical negation: “∼A is true if and only if A is not true”. But in intuitionistic logic this equivalence fails - one can observe that [according to Kripke semantics] “the state of theory a does not force the constructive truth of sentence A” [i.e., “sentence A is not constructively proved at the state a of theory T”] iff “the state of theory a forces the constructive truth of sentence ∼A”, does not hold in Kripke models in general.

Hence, the question arises,which way should one take to deal with intuitionistic falsehood.

• @HunanRostomyan - it's a pleasure to give you the opportunity to teach us in a so clear a way :) – Mauro ALLEGRANZA May 10 '14 at 14:11