search

advancedresearch / prop

Propositional logic with types in Rust
MIT License
60 stars 2 forks source link

Add type alias for `!a == !!b` for type theoretic existential philosophy #343

Open bvssvni opened 2 years ago

bvssvni commented 2 years ago

This is useful when two propositions are exclusive:

(!a == !!b) & (!b == !!a)

can be reduced to:

!a == !!b

For existential propositions a, b, !a == !!b implies !a | !b and !!a | !!b

bvssvni commented 2 years ago

I believe !a == !!b also implies a =x= b.

bvssvni commented 1 year ago

!a == !b equals a =x= b, so !a == !!b can't (or should not) imply a =x= b.