Expand description
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
Quality between A
and B
(A ~~ B
).
Functions
¬(a ~~ b) ⋀ (a == b) => c
.
Symmetry (a ~~ b) => (b ~~ a)
.
Equality lift (a == b) => ( (a ~~ b) ⋁ ¬¬(a ~~ b) )
.
Excluded middle implies reflexivity.
Mirror ¬¬(a ~~ a)
.
(a ~~ b) => (a ~~ a)
.
(a ~~ b) => (b ~~ b)
.
¬(a ~~ a) => b
.
Converts to equality (a ~~ b) => (a == b)
.
Transitivity (a ~~ b) ⋀ (b ~~ c) => (a ~~ c)
.