Module prop::queenity

Seshatic Queenity

Seshatic Queenity is a Seshatic relation that “points directly”. See paper.

A Seshatic relation means it is strictly directional or looping on itself. For more information, see the documentation for the “quality” module.

Intuition

Seshatic Queenity models a particular relationship where a queen has no queens above her, therefore there are no queens below her. Every subordinate of the queen, is subordinated the queen directly.

The queen always queens herself (a ¬> a). This means she has the same relation to herself that every subordinate has to her.

Seshatic Queenity is more “relaxed” than self-inquality ¬(a ~~ a) (Seshatism). Under Seshatism, the Self has same relation to itself as to every other proposition. Seshatism is global, while Seshatic Queenity is local. Furthermore, Seshatic Queenity determines the direction toward the Self. Seshatism can be symmetric, but Seshatic Queenity is asymmetric.

Transitivity

Seshatic Queenity is transitive.

This can seem confusing, because transitivity intuitively models a middle-queen, which is precisely what Seshatic Queenity forbids.

However, without proofs of symbolic distinction, there is no way to explicitly forbid the middle-queen. This means that Seshatic Queenity can be transitive without problems.

Structs

• Sq
  Queenity between A and B (A ¬> B).

Traits

• NoOtherSq
  Prevents other queens of A from excluding queen B.
• UniqSq
  If A’s queen is C, then C is equal to B.

Functions

• in_left_arg
  (a ¬> b) ∧ (a == c) => (c ¬> b).
• in_right_arg
  (a ¬> b) ∧ (b == c) => (a ¬> c).
• nsq_left
  (a ¬> b) ⋀ ((a == b) => (a ~~ b)) => ¬(a ¬> a)
• nsq_left_theory
  (a ¬> b) ⋀ theory(a == b) => ¬(a ¬> a)
• seshatic
  (a ¬> b) => (¬(a ~~ a) ⋁ ¬(b ~~ b)).
• sq_right
  Gets self-queenity of right side (a ¬> b) => (b ¬> b).
• to_imply
  Converts queenity to implication (a ¬> b) => (a => b).
• to_sesh
  Converts queenity to inquality (a ¬> b) => ¬(a ~~ b).
• transitivity
  (a ¬> b) ⋀ (b ¬> c) => (a ¬> c).