Ternary is not Kleene #2958
Ternary is not Kleene #2958
Conversation
This puts emphasis on Ternary not being designed to be a complete model of Kleene logic -- the truth tables for 'not', 'and' and 'or' are just defined in accordance with Kleene.
henrikt-ma
added
MCP0034
|
|
||
| For example, to evaluate `false or unknown`, one has to consider both possible outcomes for the uncertain operand, meaning that the result might be ither `false or false` or `false or true`. Since the different outcomes don't agree, the result of the operation is uncertain, represented by `unknown`. | ||
|
|
||
| Although the truth tables of `not`, `and` and `or` agree with Kleene logic, the set of logical connectives on `Ternary` is deliberately not meant to model any particular ternary logic. In particular, by not defining an operator for material implication, `Ternary` cannot be considered a complete model of Kleene logic. Applications requiring a complete model of one of the many possible ways to define ternary logic may use `Ternary` to represent the three truth values, but should define all the logical connectives of the logic in question as a package (library) of functions. |
There was a problem hiding this comment.
This paragraph relates to this comment in the main MCP issue:
To reassure you that the MCP is not about a 3-valued logic as you think of it, note that the MCP does not introduce an implies operator
The Kleene truth tables of the MCP already define implication (since implication in Kleene is just ¬A ∨ B). The issues of this logic are there, regardless if we support a dedicated implication operator or not. The point of these issues I described above is not that Kleene is wrong or something. The issue is that complex expressions in that logic often yield very surprising results (for which reason other, more advanced logics are proposed). More complex 3-valued logic relations may be hard to develop and likely boil down to try and error for users or need for step-by-step debugging of logic expressions.
So, while I agree that implication in Kleene is ¬A ∨ B, I wouldn't call something Kleene logic until this definition has been made.
|
|
||
| For example, to evaluate `false or unknown`, one has to consider both possible outcomes for the uncertain operand, meaning that the result might be ither `false or false` or `false or true`. Since the different outcomes don't agree, the result of the operation is uncertain, represented by `unknown`. | ||
|
|
||
| Although the truth tables of `not`, `and` and `or` agree with Kleene logic, the set of logical connectives on `Ternary` is deliberately not meant to model any particular ternary logic. In particular, by not defining an operator for material implication, `Ternary` cannot be considered a complete model of Kleene logic. Applications requiring a complete model of one of the many possible ways to define ternary logic may use `Ternary` to represent the three truth values, but should define all the logical connectives of the logic in question as a package (library) of functions. | ||
|
|
There was a problem hiding this comment.
(Attaching comment to empty line just to get a separate discussion thread.) The paragraph, meant to turn into non-normative text in the specification also tries to address this concern from the main MCP issue:
the MCP does not intend to enter the muddy waters of all 3-valued logics
And I don't want it to be the opener for future proposals in that direction.
If we say: That's it, Kleene truth tables and nothing more -- even if hell freezes -- I am very much Ok with it. The Kleene 3-valued logic is the most simple straight forward many-valued logic. I consider it very limited in its application area however -- that is why it is not used for anything but most simple applications. If somebody comes in the future with "but that case of the three-valued logic also needs some consideration" we should pull the plug.
I believe it will be hard to specify things in a way that will for sure prevent more or less arbitrary future specialization to some popular ternary logic, but I think that a well formulated non-normative paragraph or two should be able to capture the essence of the concerns felt today, and thereby drastically reduce risk of these concerns being forgotten or ignored in the future.
| @@ -32,10 +32,12 @@ There is a total order of the possible `Ternary` values given by `Ternary(false) | |||
|
|
|||
| ## Expressions with Ternary | |||
|
|
|||
| Logical operations on `Ternary` are defined according to Kleene, where `unknown` can be thought of as representinc uncertainty about being `true` or `false`. With this interpretation the Kleene logic tables then follow from the Boolean logic. | |||
| The logical connectives `not`, `and` and `or` on `Ternary` are defined in accordance with Kleene, where `unknown` can be thought of as representinc uncertainty about being `true` or `false`. With this interpretation the truth tables then follow from the Boolean logic. | |||
There was a problem hiding this comment.
Regarding comment in main MCP issue:
Right. We should not use Ternary to build theorem proofers.
But our users will see the 3-valued logic, and start trying it on more complex domains than just dialog visibility. I have this requirements engineering library of EDF in my mind that had been proposed some time ago, also as a motivation to add 3-valued logic (at the end it turned out it was kind of a 4-valued logic because of the need to model time ... voilà, there it goes). With the proposed 3-valued logic, this requirements engineering example will first become sort-of more easy to develop, but then turns out to fall short and then all the craziness comes in step by step as additional requirements and corner-cases.
Your comment makes me think of the connectives I would have liked to handle things like "Boolean annotations with clever automatic default". Instead of interpreting unknown as unknown, I would have liked it to be interpreted as disregard, allowing it to be cancelled from both conjunction and disjunction. That is, instead of and and or, I would have wanted the connectives duand (disregard-unknown-and) and duor (disregard-unknown-and). Do you happen to know if this has a name in the literature? If so, maybe this could also be mentioned non-normatively, as it illustrates that not even the truth tables for and and or are as obvious as one might first think?
|
@christoff-buerger I think that the contents of this PR have been assumed already part of the current proposal when discussed at the previous web meeting. Would you agree, meaning that we should merge this to again have everything in one place? |
I am sorry for the late reply. |
This PR is meant to be the continuation of the discussion in the main MCP issue, with last comment #2477 (comment).
The goal is to remove traces of
Ternarybeing designed as a model of Kleene logic, and make it clear thatTernarydoesn't want to be any other particular ternary logic either.Note that this PR is only targeting the design documents, and is meant to be merged before work on actual specification changes is initiated. This allows us to have this discussion now, instead of delaying it until proposed specification changes are available.