Module prop::quality

source · [−]

Expand description

Path Semantical Quality

See paper.

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

Seshatism

Seshatism is a way to reject two forms of Platonism:

¬(a ~~ a): Seshatism (Moment Witness)
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.

Seshatism forces the logical structure around the proposition to be a DAG (Directed Acyclic Graph).

Work-arounds for symbolic distinction

IPL does not support symbolic distinction, so there are two supported work-arounds that are safe to use:

Add argument to explicitly assume lifting equality into quality
Add argument or assume pure Platonism using “pure_platonism” feature flag

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.

If you want to prove stuff about Seshatism, this is the only way.

Pure Platonism

PurePlatonism<A, B>

Feature flag: “pure_platonism”

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: