Double negation vs Intuitionism

To describe and understand the problems with double negation from intuitionistic point of view it is necessary to go outside bivalued contexts and distinguish and sharpen up concepts that are collapsed together in bivalued contexts. However, there is a long way to go, to first sharpen up some traditional concepts before it is possible to right address and show the problem. First we need to distinguish between negation of meaning and truth. When we denies the mening of p we get ~p that is an other meaning, the contrary meaning 'not-p'. Then we denies the meaning 'not-p' we get the contrary meaning to 'not-p', which is p. When we denies the truth of p the meaning p we denies does not change. Lets use the prefix T and F for true and false and assume as in classical logic that truth and falseness is contraries such as T and ~F means the same and F and ~T means the same. When we assumes that p is false, we assumes Fp. This is a new mening that includes the meaning of p but now with the additional meaning 'to be false'. This new statement Fp has quite different properties than the statement of ~p. Then we denies Fp we get the contrary to the meaning Fp which is ~Fp, i.e. 'p is not false', i.e. 'p is true', i.e. Tp which meaning differ from p. Then we denies ~p we get the contrary to the meaning ~p which is p. Next we need to distinguish between "not-1" and 0. This point can not ever be discovered or understood inside a bivalued context as the only two values T and F are represented by 1 and 0 and 'not-1' only can be 0. To understand the difference we need to look at a range of numbers from 0 to 1 including them, i.e. the interval [0,1] or, which is the same, [0%,100%]. Then p is true we also can understand this as 'p has the truthvalue 1', i.e. 'p = 1'. Then we denies this mening itīs the equality we denies and we get 'p < 1 or p > 1' which means the same as 'p < 1' as 1 is the largest number in this context. When we again denies 'p < 1' we get 'p = 1 or p > 1' which means the same as 'p = 1' . So, as 'p = 1' means the same as Tp above '~(p = 1)', i.e. 'p < 1' must mean the same as Fp. In [0,1] the difference between 'p < 1' and 'p = 0' is of great importance. In bivalence these different writings colapses into each others. For easier handling, let's use following definitions and semantics: (1)    Tp    =df    (p = 1)        ; 'p is 100% true' (2)    Fp    =df    (p < 1)        ; 'p is lower than 100% true' (3)    Ep    =df    (p > 0)        ; 'p is higher than 0% true' (4)    Up    =df    (p = 0)        ; 'p is 0% true' As exampel of an applicable context: Think of an urn with 100 marbles and the statement p: 'The marbles in the urn is black'. If all of them are black, the statement is 100% true, if none are black it is 0% true. If there are only 99 black mables the statement is false (but still nearly true). This context has 101 possible values (the number of marbles + 1). If the urn only had one marble, the context should be bivalued. Next we need to right address a third alternative 'unknown' In the above mentioned context the truthvalues of the statements p and ~p together must be 'the hole', i.e. 100%. However, some marbles can remain unknown of some reason, e.g. until all of them are out and visible. Now a third alternative appears to make the sum of p and ~p lower than 100% and the statement 'It is unknown if the marbles in the urn is black or not black' is true to the difference. Let us simplify and use the prefix ? to denote 'it is unknown...' and denote the truthvalues as relative occurences as above with the prefix R. Now the sum of the three alternatives is: (5)    Rp + R~p + R?p 1 'Unknown' is now neither a new truth value between true and false nor a new meaning between p and ~p, but is a new alternative that only concur of the whole avilable truthvalue, 100%, not able to touch the contrarity of p and ~p or true and false. To introduce 'unknown' as a *truth value* beside or between 'true' and 'false' introduces only big philosophical and unsolvable troubles. Next we need to apply this three-alternativs-context to the four definitions above As no marble can satisfy more than one of the statements p, ~p or ?p, the sum (5) also can be expressed as (the proofs are excluded here): (5.1)    R(p v ~p v ?p) 1 (5.2)    R(p v ~p) + R?p 1 (5.3)    Rp + R(~p v ?p) 1 ... etc Using the relation (5.3) the definitions (1)...(4) can be transformed like (with the prefix R used in definitions): Tp    =df    (Rp = 1) (Rp = Rp + R(~p v ?p)) (R(~p v ?p) = 0) U(~p v ?p) ...to: (6)    Tp U(~p v ?p) (7)    Fp E(~p v ?p) (8)    Ep F(~p v ?p) (9)    Up T(~p v ?p) The relation between true and false remains unchanged. The relations between T, F, E and U is: Tp ~Fp ~E(~p v ?p) U(~p v ?p) Fp ~Tp ~U(~p v ?p) E(~p v ?p) Ep ~Up ~T(~p v ?p) F(~p v ?p) Up ~Ep ~F(~p v ?p) T(~p v ?p) Next we need to distinguish between necessary and temporary equality In the relations above both '=' and '' are used to express quantitative equalities, '=' temporary equalities and '' necessary equalities. If two expressions are necessary equal they always has same truth value independent of all circumstances and every arbitrary context or situation. If so, the two expressions has both identical truthvalues and identical meaning. Necessary equality '' is stronger than '=' that only expresses temporary equality of truth values, and stronger than '<=>' that only expresses equivalens, i.e. 'true together' and 'false together'. Outside a bivalued context equivalences are not sufficient to express that two expressions has same meaning - we must prove they are necessary equal. From a necessary equality we of course can conclude both temporary equality and equivalence. Finally we need to enter modal concepts Using the concept of necessary equality we can sharpen up (1)...(4) to define modal concepts. Then 'p = 1' ( i.e. 'Rp = 1') is changed to 'p 1' we tells that 'p is necessary 100% true'. The negation of 'p = 1' is 'p <> 1' (i.e. in [0,1] the same as 'p < 1') will here correspond to 'p 1', 'p is not necessary 100% true'. L and M (like Lewis) are used as prefix for 'necessary true' and 'possible'. (10)    Lp    =df    (Rp 1)        ; 'p is necessary 100% true' (11)    ~Lp    =df    (Rp 1)     ; 'p is not necessary 100% true' (12)    Mp    =df    (Rp 0)     ; 'p is not necessary 0% true' (13)    ~Mp    =df    (Rp 0)     ; 'p is necessary 0% true' In same way as above we can derive (14)    Lp        ~M(~p v ?p) (15)    Mp        ~L(~p v ?p) We are now the whole turn around and back to a pure bivalued context. We have still three alternatives, 'p', 'not-p' and 'unknown', but necessary truth can not be mesured like the marbles in a urn as a portion of 100%. There are no degrees of necessary truth - a statement is necessary true or is not necessary true. There can not be other possibilities. However, by value but not conceptually ' 1' is not the same as ' 0', so ~Lp will never collaps into ~Mp like Fp does into Up in a contingent bivalued context. As modal logic is pure bivalued it has been questioned what more it can contribute to that not allready can be handled by standard logic. Modal logic uses same rules of consequence as all logic but has quite other and important properties than e.g. logic in a contingent context. Intuitionism and constructivism has rejected reduction ad absurbum as an unsure method of proof. Above is shown that from ~M~p we can not conclude Lp. We need to show ~M(~p v ?p), i.e. both ~M~p ("it's not possible that not-p") and ~M?p ("it's not possible that p is unknown") to conclude Lp. Intuitionists are right in their critisism but hits the wrong property of logic. Duoble negation reduction is a most basically foundation of all logic and will still remain untouched. There are still no problems to reduce ~~p to p, to toggle beween a meaning and its contrary meaning for every negation. Also for every negation of truth we still can toggle between the contraries Tp and Fp. As reductio ad absurbum proof takes place in modal contexts we need to handle them by modal logic but for that we need a modal logic strict constructive derived, like the logic refered above.