Module prop::quality

Path Semantical Quality

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. For a different implementation of quality, see PSI in Avalog.

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;

Structs

Q

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

Functions

absurd

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

commute

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

eq_lift

Equality lift (a == b) => ( (a ~~ b) ⋁ ¬¬(a ~~ b) ).

excm_refl

Excluded middle implies reflexivity.

mirror

Mirror ¬¬(a ~~ a).

self_quality_left

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

self_quality_right

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

sesh_absurd

¬(a ~~ a) => b.

to_eq

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

transitivity

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