Links

̶
Adam I. Gerard
ISU
NIU
CS MS TBD

Read OR Thoughts

Brief discussion on the topic of Disjunction and/or OR.

Logical Disjunction

Logical Disjunction is ancient, going back to Aristotle's Syllogism. It's the most basic notion we'll cover. It's often called "Logical OR", "Disjunction", or "Inclusive OR".

Usually stylized thusly P ∨ Q where ∨ is typically called:

  1. Logical Upside-Down Caret
  2. Unicode U+2228
  3. "wedge"

Evaluated by Boole, Wittgenstien, and predecessors from Antiquity as the following (in Truth-Table format - often credited to Wittgenstien alongside the idea that Truth Evaluations are Truth Functional - to be treated as a Function mapping a Sentence or Proposition to a Truth Value):

P Q P ∨ Q
⊤ ⊤ ⊤
⊤ ⊥ ⊤
⊥ ⊤ ⊤
⊥ ⊥ ⊥

In Natural Language (English) and (mixing our Meta- and Object- Langauges a bit):

  • P ∨ Q is Evaluated ⊤ whenever P or Q is.
  • "P or Q" is True whenever "P" is True or "Q" is True.
  • P ∨ Q is Evaluated ⊥ only when both P and Q is.
  • "P or Q" is False only when "P" is False or "Q" is False.

Technically, the convention since Tarski goes that we discuss a target Language from within another Meta-Language - we're being a bit messy in mixing "or" in one level with a definition at another but it's fine to convey the point here.

To those not familiar with Philosophy, Foundations of Math, Computer Science, or Linguistics this might come as a surprise. If you're familiar with how compilers work or the history of say Java, Ruby on Rails, etc. that's a fairly mundane observation.

XOR

Exclusive OR - akin to Inclusive OR with tighter constraints requiring that the Disjunction be Evaluated ⊤ only when P or Q is but not when both P and Q is.

P Q P ⊻ Q
⊤ ⊤ ⊥
⊤ ⊥ ⊤
⊥ ⊤ ⊤
⊥ ⊥ ⊥

Circuit Breaker OR

From Computer Science and Imperative Programming (with Imperative Operations). Circuit Breaker OR adds to Disjunction certain Temporal or Order Execution concepts:

  • Computer Programs Evaluate Expression in real-time on real physical machines. A bit more mundane than the somewhat Abstract Realm of Cantor and Philosophy of Logic and Maths.
  • Circuit Breakers Evaluate Expressions left to right in chronological and lexiographical order.
P Q P ‖ Q
⊤, Halt Do Not Evaluate, ⊤ ⊤
⊤, Halt Do Not Evaluate, ⊥ ⊤
⊥ ⊤, Halt ⊤
⊥ ⊥ ⊥

This means that a Left-most ⊤ will quickly reduce the Operation to single Evaluation (rather than proceeding to Evaluate all others in the Disjunction).

Exhaustive OR

I was a bit surprised that this apparently isn't Formalized as a notion.

Most people (and especially working Computer Scientists, Software Engineers, Software Developers) have probably encountered this as some point (so no claims to originality here). I am a bit puzzled that there isn't an existing convention for this though (at least to my knowledge).

  • Ex. Disambiguation in Semantics (Polysemanticity)
  • Ex. switch statements and Control Flow Expressions in Programming
  • Ex. An O(1) Key-Value existence check by a Value (Needle belonging to or within a specific Haystack)
  • Ex. Element-wise Set Membership or comparison for many Elements
  • Ex. Subset relationships between Sets

Exhaustive OR restricts an Evaluation to a (definition) Set of Disjuncts. From here we can break this conception into multiple branching (non-mutually-exclusive) pathways for further understanding:

  1. Evaluate ⊥ if any Disjunct isn't part of that Set. E.g. - the "Banhammer Conception".
  2. Evaluate ⊥ if no Disjunct is part of that Set (even though at least one Disjunct might Evaluate to ⊤). E.g. - the "True but Irrelevant Conception".
  3. A Disjunct for which the Inference Rule known as (Disjunctive) Weakening fails (is Invalid): P ⊬ P ∨ Q unless both P, Q are in the Set. E.g. - the "True but Don't Reason About that Rando Conception".
  4. A Disjunct which is Evaluated ⊤ only if every Disjunct in the (definition) Set is present in the Expression. (That all Disjuncts are present in the Expression isn't sufficient to be Evaluated ⊤.) E.g. - the "Exhaustive List Conception".
  5. Through Curry-Howard Correspondence define Exhaustive OR as non-primitive Logical Operator or Symbol. (Or take the alternate approach and define it as a primitive in addition to or outright replacing other kinds of Disjunction.) E.g. - the "Real Academic Research Potential Conception".

With this higher level of specificity we're now entering some interesting and possibly uncharted academic terra incognita. Fun times. To be continued.

Update:C# 15 recently added support for Union Classes which support exhaustive switch statements.

Contents