implementation of Modus ponens and Modus tollens

Can we have in Prelude - Booleans, Modus ponens and Modus tollens implemented? Or in another module?

reminder:[[BR]]

P is a proposition and v(p) is the logic value of P.[[BR]]

P is true, v(P) = 1[[BR]]

P is false, v(P) = 0[[BR]]

P -> Q is always true in propositional logic.

Modus ponens:[[BR]] v(P) = 1[[BR]]

v(P -> Q) = 1[[BR]]

v(Q) = 1[[BR]]

v(P) and v(P -> q) are premiss, v(q) is the conclusion.[[BR]] or in a more general form[[BR]]

P : X is A[[BR]]

P -> Q : A -> B[[BR]]

Q : X is B[[BR]]

Modus tollens:[[BR]] v(Q) = 0[[BR]]

v(P -> Q) = 1[[BR]]

v(P) = 0[[BR]]

v(Q) and v(P -> Q) are premiss, v(P) is the conclusion.[[BR]] or in a more general form[[BR]]

not Q : X is not B[[BR]]

P -> Q : A -> B[[BR]]

not P : X is not A[[BR]][[BR]]

As well as using the numbers 0 and 1 for the respective values false and true, we'll use the letters F for False and T for True.[[BR]]

We are always:[[BR]] v(F) = 0[[BR]]

v(T) = 1[[BR]]

v(P -> Q) = 1[[BR]]

Trac metadata

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information