/sci/ - Science & Math

Having some fun with Heyting algebras.
Here's the the model of negation in a ring for the 3 element one (with False [math] < [/math] Middle [math] \le [/math] True, although the polynomial just needs False [math]\neq[/math] Middle)

[math] \neg(x) := F + (T-x) \dfrac{M-x}{M-F}[/math]

E.g. for [math]F=0, T=1[/math],

[math] \neg(x) := (1-x)\cdot (1-x\,/\,M)[/math]

Of course this has a natural map into the standard Boolean bits representation, as [math]M=T[/math] makes for [math] \neg(x) := (1-x)[/math].

The curious thing for me is that in general Heyting semantics (including Boolean algebra, but trivially), it's always the case that [math]\neg \circ \neg [/math] is monotone upwards.
So [math] \neg \neg P [/math] is, "truer", or easier to prove than [math] P [/math].
And I think the collapse to the Boolean situation must remain an option and [math] \neg \neg P \lor \neg P [/math] is provably out of the question.