Unsure

[Magnogen]

I'm curious - you said that Unsure values are intuitive, but I'm kinda stabbing in the dark as to what they do. Is it like this?

not T `[F]alse?`
not F `[T]rue?`
not U `...?`

That last one would read as "not unsure", or if you cancel the double negative, "sure". This doesn't help because now I know it's sure, but I'm not sure what I'm supposed to be sure it is.

If that makes sense, lol.

How does U interact with the other booleans, and itself, with logical operators?

[hebozhe]

Unsure values allow for intuitionistic evaluations for the operations or, and, and not. All primitive values are stored initially as 8-bit integer arrays [0] (for F), [1] (for U), and [2] for T. Every primitive instance of U, however, also receives an attached Boolean combination unique to it, and its length is determined by the order in which it arises in a program.

For instance, if I have a program involving two variables isUnsure and isAlsoUnsure, they evaluate as follows:

def isUnsure as U;  `Interprets to [1 2 0]`
def isAlsoUnsure as U;  `Interprets to [1 2 2 0 0]`

This is important because, while both values are Unsure, that doesn't mean they're equivalent. We can see that in an equivalence test using the three operators:

def areIdenticalUnsures as (not isUnsure or isAlsoUnsure) and (not isAlsoUnsure or isUnsure);

The value expression evaluates as follows:

1. (not [1 2 0] or [1 2 2 0 0]) and (not [1 2 2 0 0] or [1 2 0])
2. ([1 0 2] or [1 2 2 0 0]) and (not [1 2 2 0 0] or [1 2 0])
3. ([1 0 2] or [1 2 2 0 0]) and ([1 0 0 2 2] or [1 2 0])
4. ([1 0 2 0 2] or [1 2 2 0 0]) and ([1 0 0 2 2] or [1 2 0]) Only equally sized U arrays can be evaluated.
5. ([1 2 2 0 2]) and ([1 0 0 2 2] or [1 2 0])
6. ([1 2 2 0 2]) and ([1 0 0 2 2] or [1 2 0 2 0]) Only equally long U arrays can be evaluated.
7. ([1 2 2 0 2]) and ([1 2 0 2 2])
8. [1 2 0 0 2] This array is ultimately what's stored for areIdenticalUnsures.

What matters for this is whether any articulation of the law of excluded middle or other classically valid, but intuitionistically invalid, tautology holds, while also making sure that all classical contradictions are also intuitionistic contradictions, and thus the classical double negations intuitionistically hold (this is called Gilvenko's theorem).

Consider this example:

def isLEMUnsure as isUnsure or not isUnsure;

1. [1 2 0] or not [1 2 0]
2. [1 2 0] or [1 0 2]
3. [1 2 2] This means that it's a classical tautology, but not an intuitionistic one.
4. [1 2] Because the first half and second half of the Boolean evaluation sub-array is identical, it can be shortened. This is what's stored in isLEMUnsure.

But, what happens if isLEMUnsure is double-negated at some point? Well, that would lead to this evaluation:

1. not not [1 2]
2. not [1 0]
3. not [0] Every classical contradiction is an intuitionistic contradiction. That's what F encodes.
4. [2] Ergo, an intuitionistic tautology. This is what T encodes.

Thanks to this operation in (3), which is called gilvenkoize in both the Python and Go interpreters, the expected intuitionistic evaluations arise.

You can show that this property holds for any Lej-legal and classically valid, but intuitionistically invalid, proposition under the sun. That includes the LEM for trivalent logics ("not A or not not A"), Peirce's theorem, the conversion half of contraposition, the intuitionistically invalid DeMorgan's shift, etc., so long as they are analogs expressed exclusively with and, or, and not.

In short, U values are not one fixed thing. Their values start as different arrays and transform under the logical operations of the language.

[Magnogen]

This interesting, but it is incredibly complicated and I'm still not even sure how this could be useful in a language. How would you use these Array Booleans?

[hebozhe]

This interesting, but it is incredibly complicated and I'm still not even sure how this could be useful in a language. How would you use these Array Booleans?

You can't access the arrays directly in Lej. This merely describes how they're stored.

I've considered a few use cases in asynchronous programming, say, for instance, where a 404 or similar response would return F, a 200 would return T, but the status would remain U until the status resolves one way or another. That would allow users to use the otherwise operator to sleep in Lej's equivalent of a while-loop.

But, I'm making Lej to include intuitionistic semantics so that developers more creative than I am take advantage of it, if they want.

[Magnogen]

Ooo okay that makes sense, and I suppose a simple wave function collapse algorithm could be done with it too. Nice!