Introduce SProp trait for `!~a == ~!a`

advancedresearch / prop

Propositional logic with types in Rust

MIT License

58 stars 2 forks source link

Open bvssvni opened 1 year ago

bvssvni commented 1 year ago

Is is known that !~a == ~!a does not hold in all models of PSQ, e.g. Dit Calculus.

One could introduce a SProp trait (for Sesh/Seshatism).

bvssvni commented 1 year ago

The problem is that this design does not propagate:

!~~a == ~!~a is not provable from !~a == ~!a