-
Notifications
You must be signed in to change notification settings - Fork 41
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Ternary is not Kleene #2958
Ternary is not Kleene #2958
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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. | ||
|
||
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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This paragraph relates to this comment in the main MCP issue:
So, while I agree that implication in Kleene is ¬A ∨ B, I wouldn't call something Kleene logic until this definition has been made. |
||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. (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:
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. |
||
### Unary operators | ||
Unary operators on `Ternary`, where `x` is an expression of type `Ternary`: | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Regarding comment in main MCP issue:
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 ofand
andor
, I would have wanted the connectivesduand
(disregard-unknown-and) andduor
(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 forand
andor
are as obvious as one might first think?