Module prop::quality

Path Semantical Quality

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

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

Work-around for symbolic distinction

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

Lifting equality into quality

EqQ<A, B>

This implementation lifts equality directly to quality. Since this is unsound without symbolic distinction, it is not possible to assume this directly.

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

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.

Seshatic Relations

Seshatic<A, B>

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)

Pure Platonism

PurePlatonism<A, B> (feature flag is not needed)

Feature flag: “pure_platonism” (for convenience functions)

Pure Platonism is not strong enough to prove quality, but can prove False from Seshatism (Not<Q<A, A>>). Can be used when reasoning about Seshatism is not needed.

This implementation uses a 2-avatar of equality to model quality within IPL, by exploiting the property (a == b) => ( (a ~~ b) ⋁ ¬¬(a ~~ b) ).

IPL does not have symbolic distinction, so equality a == b can not be lifted properly into a ~~ b. However, since quality is not decidable within IPL, one can not prove a ~~ b from ¬¬(a ~~ b). This means that the 2-avatar can hide reflexivity, by lifting a == b to (a ~~ b) ⋁ ¬¬(a ~~ b).

Notice that this implementation does not support reasoning about Seshatism, because ¬(a ~~ a) (Seshatism) is absurd in this model (it proves anything). Proper Seshatism requires quality to use symbolic distinction instead of the trick above.

Interpreted as an Avatar Graph, the core is a == b and there are two 1-avatars:

• (a ~~ b)
• ¬¬(a ~~ b)

The 2-avatar integrates (a ~~ b) and ¬¬(a ~~ b) using ⋁.

Re-exports

pub use commute as symmetry;

pub use nq_commute as nq_symmetry;

Structs

Q

Quality between A and B (A ~~ B).

Traits

NoOtherQ

Prevents other qualities of A from excluding B.

UniqQ

If something is qual to A, then A is qual to B.

Functions

absurd_plato

¬(a ~~ b) ⋀ (a == b) ⋀ ((a == b) => ( (a ~~ b) ⋁ ¬¬(a ~~ b) )) => c.

commute

Symmetry (a ~~ b) => (b ~~ a).

eq_maybe_lift

Equality maybe lift (a == b) => ( (a ~~ b) ⋁ true ).

excm_plato_refl

Excluded middle with pure Platonism implies reflexivity.

mirror_plato

Mirror with pure Platonism ((a == a) => ( (a ~~ a) ⋁ ¬¬(a ~~ a) )) => ¬¬(a ~~ a).

neq_to_sesh

¬(a == b) => ¬(a ~~ b).

nq_commute

Negated symmetry ¬(a ~~ b) => ¬(b ~~ a).

nq_left

(a ~~ b) ⋀ ¬(a ~~ c) => ¬(b ~~ c).

nq_right

(a ~~ b) ⋀ ¬(b ~~ c) => ¬(a ~~ c).

self_quality_left

(a ~~ b) => (a ~~ a).

self_quality_right

(a ~~ b) => (b ~~ b).

sesh_eq_neq

eqq(a, b) => ¬(a ~~ b) == ¬(a == b).

sesh_left

Introduce a different proposition in right argument (keep left).

sesh_plato_absurd

¬(a ~~ a) ⋀ ((a == a) => ( (a ~~ a) ⋁ ¬¬(a ~~ a) )) => b.

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).

to_eq

Converts to equality (a ~~ b) => (a == b).

transitivity

Transitivity (a ~~ b) ⋀ (b ~~ c) => (a ~~ c).

Type Definitions

EqQ

Lifts equality into quality.

PurePlatonism

Pure Platonism assumption.

Seshatic

A Seshatic relation ¬(a ~~ a) ⋁ ¬(b ~~ b).