Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

Unknown Statements

I have said that the assertibility of ¬(¬ K α ∧¬ K ¬α) does not exclude the existence of the fact that neither α nor ¬α are known. Can the intuitionist assert the existence of such a fact? I think not, and in this section I shall try to motivate this opinion.

Let me observe first that “K α”, in all its possible readings, clearly is an empirical statement, not a mathematical one. I have argued elsewhere that the negation of many empirical statements, and in particular of K-statements, cannot be plausibly equated to intuitionistic negation ¬, and I have proposed that it be equated to Nelson's strong negation ∼.26 So, if we add ∼ to the language LIPLK of Intuitionistic Propositional Logic plus the operator K, and we assume for simplicity that all the empirical sentences of LIPL∼,K have proofs,27 we must add, to the Definition 2 of the notion of

proof of K α, a definition of the notion of proof of ∼ K α. Here is my proposal:

Definition 5 Whenever one is presented with something that is not a proof of α, a proof of ∼ K α is the observation that what one is presented with is not a proof of α.

It should be noticed that Dummett's remark—that intuitionistic truth, when it is equated with the actual possession of a proof, does not commute with negation—is certainly correct when it is understood as referring to strong negation. For example, the observation that what one is presented with is not a proof that it is raining is not the same thing as the observation that what one is presented with is a proof that it is not raining. As a consequence, Dummett's objection to the validity of the

(T) schema as a criterion for being a truth operator seems to cause trouble in this case. However, in this case the argument (9) is no longer valid: the second step is an application of contraposition, but contraposition is not valid for strong negation. As a consequence, the fact that strong negation does not commute with truth does not entail the invalidity of the (T) schema. We can therefore conclude that, even when we add to intuitionism strong negation, the knowledge operator K is a truth operator.

25A discussion of this assumption is beyond the limits of this paper.

26Reference [24].

27In general empirical sentences have (non-conclusive) justifications. A definition of the notion of justification for the sentences of LIPL∼,K presupposes a solution of Gettier problems. I have

suggested such a definition in [23].

It seems to me that, if the existence of undecided statements can be expressed at all in an intuitionistic language, it should be expressible in LIPL∼,K . Take for instance g, Goldbach's Conjecture: for the statement

(15) Goldbach's conjecture is undecided (unknown)

the following formula seems to be a plausible formalization in LIPL∼,K :

(16) ∼ K g ∧∼ K ¬g.

Williamson argues against this formalization:

if ∼ is to count intuitionistically as any sort of negation at all, ∼ A should at least be inconsistent with A in the ordinary intuitionistic sense.28

In other words, the schema

(17) ∼α → ¬α;

should be valid; then, from (16) one could derive ¬ K g ∧ ¬ K ¬g, which, by (2) and (13), is equivalent to ¬g ∧ ¬¬g: a contradiction. However, the assumption that

(17) is valid for all α of LIPL∼,K seems to be a sort of petitio principii, since, on the one hand, it almost amounts to assuming what one wants to conclude, i.e. that

(16) is inconsistent, and, on the other hand, the motivation for it seems insufficient. Notice that (17) is valid for all α belonging to LIPL∼ ,29 so, according to Williamson's criterion, ∼ does count intuitionistically as a sort of negation; the possible invalidity of (17) when α contains occurrences of K can therefore be imputed to the interplay between the meanings of K and ∼. On the other hand, (17) is clearly invalid when α contains occurrences of K. Consider the instance

(18) ∼ K α →¬ K α:

it asserts the existence of a function f associating to every proof of the antecedent a proof of the consequent. A proof of the antecedent is the observation that what one is presented with is not a proof of α; this observation is true in two cases: when one is presented with a proof of ∼α, and when one is presented with some x that is neither a proof of ∼α nor a proof of α. In the second case f should associate to x a function f t associating to every proof of K p a contradiction; but f t cannot exist: as x is not a proof of ∼α, the existence of a y that is a proof of α cannot be ruled out, and if one observes that y is a proof of α, that observation is a proof of K α.

However, if we look at the interplay between intuitionistic logical constants, strong negation and K from the standpoint of Kripke semantics, the assertibility of (18) seems to be out of the question. A Kripke model for LIPL∼ is a quadruple

28Reference [26], p. 139.

29Reference [9].

M = (W,, D, V ), where W is a non-empty set (of nodes), ≥ is a reflexive partial order on W , and V is a partial function from atomic formulas and nodes to {0, 1} satisfying the following conditions:

• If V ( p, w) = 0 and w Rwt, then Val( p, wt) = 0;

if V ( p, w) = 1 and w Rwt, then Val( p, wt) = 1 (stability).

• For every wW , V (, w) = 0.

For every wW , V (∼⊥, w) = 1.

The notion Fw α (α is true at w) is defined by induction on α as follows:

Fw p iff V ( p, w) = 1 Fwp iff V ( p, w) = 0 Fw ∼⊥

Fw αβ iff Fw α and Fw β

Fwβ) iff Fwα or Fwβ

Fw αβ iff Fw α or Fw β

Fwβ) iff Fwα and Fwβ

Fw αβ iff, for every wt ≥ w, if Fwt α then Fwt β

Fwβ) iff Fw α and Fwβ.

Now, if we add the operator K to LIPL∼ , the only definition I can see that is faithful to Definition 5 is the following:

(19) Fw K α iff Fw α

Fw ∼ K α iff, for some wt ≥ w, Fwt ∼α.

Call any Kripke model for LIPL∼ in which these clauses hold a model for LIPL∼,K . Consider now the following model M of LIPL∼,K , where V (g, w) is undefined, V (g, w1) = 0 and V (g, w2) = 1:

w1 w2

w ///


M falsifies at w all the following formulas:

∼ K g →¬ K g

∼ K g → ∼g

∼ K g → ¬g

∼ K ¬g → ¬¬g.

On the other hand, Fw ∼ K g ∧∼ K ¬g; but the constraint of monotonicity is not met: not Fw1 ∼ K g and not Fw2 ∼ K ¬g.

Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics