hooo

Propositional logic with exponentials

=== HOOO 0.1 ===
For more information, type `help`
> use silence
> use zero
> use and
> use eq
> use hooo
> ((a = b) ^ True)
(((A □ B) ^ X) = ((A ^ X) □ (B ^ X))) by hooo
((a ^ ⊤) = (b ^ ⊤)) by eq

To run hooo from you Terminal, type:

cargo install --example hooo hooo

Then, to run:

hooo

Motivation

The ongoing research on PSQ suggests that propositional logic can be extended with Category Theory Exponentials.

The problem is that PSQ contains a qubit operator ~ with the special property that it has congruence by tautological identity only. In current theorem provers, it has not been possible to reason about this.

For example, a == b does not imply ~a == ~b, only when a == b is provable from none assumptions.

The (a == b)^true relation is an exponential proposition which proves that a == b from none assumptions. This gives a == b the tautological identity needed for substitution in the qubit operator ~.

It turns out that this is semantically the same as Higher Order Operator Overloading.

Or simply: hooo