Module prop::quality

Path Semantical Quality

Path Semantical Quality is a partial equivalence relation that lifts biconditions with symbolic distinction. See paper.

If this is your first time, then you might want to check out the path_semantics module first.

For a different implementation of quality, see PSI in Avalog.

There is also an implementation in Pocket-Prover.

Path semantical quality is written ~~, e.g. a ~~ b (see Q).

Work-around for symbolic distinction

IPL does not support symbolic distinction, so quality must be assumed explicitly.

There are some ways to cheat though, e.g. using hooo::lift_q or fun::inv::self_inv_to_q.

For more information about symbolic distinction, see the path_semantics module.

Lifting equality into quality

EqQ<A, B> (see EqQ)

Although IPL does not support symbolic distinction, one can use EqQ<A, B> ((a == b) => (a ~~ b)) to model symbolic distinction. This means EqQ<A, B> can be used as an assumption that A and B are symbolic distinct.

Seshatism vs Platonism

In philosophy of mathematics, path semantical quality can be used to talk about the distinction between bias of Seshatic (dual-Platonic) languages and Platonic langauges.

Seshatism is a way to reject two forms of Platonism:

• ¬(a ~~ a): Seshatism
• a ~~ a: Platonism 1 (Loop Witness)
• a ~~ b: Platonism 2 (Product Witness)

Since a ~~ b implies a ~~ a, both Loop and Product Witness are rejected by Seshatism.

For more information, see Seshatism vs Platonism.

Seshatic Relations

Seshatic<A, B> (see Seshatic)

When a relation p(a, b) is Seshatic, it means that it implies Seshatism of either a or b:

p(a, b) => ¬(a ~~ a) ⋁ ¬(b ~~ b)

Aquality

Aquality is a Seshatic relation that is symmetric to quality (Aq). It means, when substituting quality with aquality and vice versa, one can prove the same theorems.

One can think about aquality vs quality as a perspective where Seshatism and Platonism become mirror images of each other.

The core axiom biases mathematics toward Platonism, but this choice is arbitrary since ¬~x == ~¬x (see qubit::eq_sesh_inv). Therefore, “Platonism” is whatever theory/philosophy that is associated with the quality/aquality used in a core axiom. The dual theory/philosophy is Seshatism.

Dualities of this form are common in mathematics, so Seshatism vs Platonism is often used to talk about analogues of other dualities as well.

Functions

• aq_hom_in_left_arg
  (a ~¬~ b) ∧ hom_eq(2, a, c) => (c ~¬~ b).
• aq_hom_in_right_arg
  (a ~¬~ b) ∧ hom_eq(2, b, c) => (a ~¬~ c).
• aq_inv_to_sesh
  (¬a ~¬~ ¬a) => ¬(a ~¬~ a).
• aq_left
  (a ~¬~ b) => (a ~¬~ a).
• aq_right
  (a ~¬~ b) => (b ~¬~ b).
• aq_sesh_eq_neq
  eqaq(a, b) => ¬(a ~¬~ b) == ¬(a == b).
• aq_sesh_hom_in_left_arg
  ¬(a ~¬~ b) ⋀ hom_eq(2, a, c) => ¬(c ~¬~ b).
• aq_sesh_hom_in_right_arg
  ¬(a ~¬~ b) ⋀ (b == c) => ¬(a ~¬~ c).
• aq_sesh_left
  Introduce a different proposition in right argument (keep left).
• aq_sesh_right
  Introduce a different proposition in left argument (keep right).
• aq_sesh_to_neq
  Convert inquality to inequality ¬(a ~¬~ b) ⋀ eqaq(a, b) => ¬(a == b).
• aq_sesh_to_q_inv
  ¬(a ~¬~ a) => (¬a ~¬~ ¬a).
• aq_symmetry
  Symmetry (a ~¬~ b) => (b ~¬~ a).
• aq_to_eq
  Converts to equality (a ~¬~ b) => (a == b).
• aq_transitivity
  Transitivity (a ~¬~ b) ⋀ (b ~¬~ c) => (a ~¬~ c).
• eq_maybe_lift
  Equality maybe lift (a == b) => ( (a ~~ b) ⋁ true ).
• eq_q_symmetry
  (a ~~ b) == (b ~~ a).
• eqq_to_excm_q
  eqq(a, b) => ((a ~~ b) ⋁ ¬(a ~~ b)).
• eqq_to_excm_q_with_excm_eq
  eqq(a, b) ⋀ ((a == b) ⋁ ¬(a == b)) => ((a ~~ b) ⋁ ¬(a ~~ b)).
• hom_in_left_arg
  (a ~~ b) ∧ hom_eq(2, a, c) => (c ~~ b).
• hom_in_right_arg
  (a ~~ b) ∧ hom_eq(2, b, c) => (a ~~ c).
• left
  (a ~~ b) => (a ~~ a).
• naq_left
  (a ~¬~ b) ⋀ ¬(a ~¬~ c) => ¬(b ~¬~ c).
• naq_right
  (a ~¬~ b) ⋀ ¬(b ~¬~ c) => ¬(a ~¬~ c).
• naq_symmetry
  Negated symmetry ¬(a ~¬~ b) => ¬(b ~¬~ a).
• neq_to_aq_sesh
  ¬(a == b) => ¬(a ~~ b).
• neq_to_sesh
  ¬(a == b) => ¬(a ~~ b).
• nq_left
  (a ~~ b) ⋀ ¬(a ~~ c) => ¬(b ~~ c).
• nq_right
  (a ~~ b) ⋀ ¬(b ~~ c) => ¬(a ~~ c).
• nq_symmetry
  Negated symmetry ¬(a ~~ b) => ¬(b ~~ a).
• q_inv_to_sesh
  (¬a ~~ ¬a) => ¬(a ~~ a).
• right
  (a ~~ b) => (b ~~ b).
• sesh_eq_neq
  eqq(a, b) => ¬(a ~~ b) == ¬(a == b).
• sesh_hom_in_left_arg
  ¬(a ~~ b) ⋀ hom_eq(2, a, c) => ¬(c ~~ b).
• sesh_hom_in_right_arg
  ¬(a ~~ b) ⋀ (b == c) => ¬(a ~~ c).
• sesh_left
  Introduce a different proposition in right argument (keep left).
• sesh_right
  Introduce a different proposition in left argument (keep right).
• sesh_to_neq
  Convert inquality to inequality ¬(a ~~ b) ⋀ eqq(a, b) => ¬(a == b).
• sesh_to_q_inv
  ¬(a ~~ a) => (¬a ~~ ¬a).
• symmetry
  Symmetry (a ~~ b) => (b ~~ a).
• theory_eq_to_eqq
  theory(a == b) => eqq(a, b).
• theory_eq_to_excm_q_with_excm_eq
  theory(a == b) ⋀ ((a == b) ⋁ ¬(a == b)) => ((a ~~ b) ⋁ ¬(a ~~ b)).
• to_eq
  Converts to equality (a ~~ b) => (a == b).
• to_eq_aq
  Converts to equality of self-quality (a ~¬~ b) => ((a ~¬~ a) == (b ~¬~ b)).
• to_eq_q
  Converts to equality of self-quality (a ~~ b) => ((a ~~ a) == (b ~~ b)).
• transitivity
  Transitivity (a ~~ b) ⋀ (b ~~ c) => (a ~~ c).

Type Definitions

• Aq
  Aquality definition (a ~¬~ b) == ((a == b) ⋀ ~¬a ⋀ ~¬b).
• EqAq
  Lifts equality into aquality.
• EqQ
  Lifts equality into quality (a == b) => (a ~~ b).
• Q
  Quality definition (a ~~ b) == ((a == b) ⋀ ~a ⋀ ~b).
• Seshatic
  A Seshatic relation ¬(a ~~ a) ⋁ ¬(b ~~ b).