Tag Info

You could address your goals by using a generic proof assistant, one that supports user-definable theories, such as Isabelle and Metamath, and I am sure there are others. These allow you to define ...

Isabelle/Sequents contains a formalisation of intuitionistic linear logic, so conceivably you have a chance of implementing your logic in Isabelle, following the techniques used there. Whether what ...

Free logic is nowhere close to how mathematicians "do things", and neither is ZFC. Proof assistants are our best attempt to provide a rigorous environment that faithfully reflects how ...

Let me try taking a stab at a few provisional definitions. I can make these arbitrarily rigorous, but being fully general makes it hard to see the forest for the trees (at least, for me). Provisional ...