Version 0.2.1 Copyright Ben Selfridge 2017
A customizable proof construction tool for sequent calculi.
logix is a tool for exploring generic sequent calculi. It was inspired by the book "Structural Proof Theory" by Sara Negri & Jan von Plato (Cambridge University Press, 2001), and is really a spiritual successor to PESCA, the proof editor companion to that book developed by Aarne Ranta. logix was intended to be like PESCA, but with more general capabilities and a slightly more intuitive interface.
logix is intended to be very extensible. I tried to take as little for granted as possible about the target theory, so even the primitive connectives are customizable. For instance, & and | come with logix for certain built-in calculi, but you can extend logix by defining your own primitive operators and deduction rules in the source code (src/Calculi.hs). The notion of conjunction and disjunction live solely in that file; the rest of logix is totally agnostic about what symbols you use, and what they mean. I put a lot of effort into making sure that defining new sequent calculi was as straightforward and obvious as possible.
logix is primarily an educational tool for myself. I wanted to learn about structural proof theory, and the best way to learn how to do math is to make a computer do it for you. However, I also would like other people to use the tool, so I have tried to make it as usable as possible by people who actually know something about this stuff.
To install logix, simply type
cabal install
at the root level. Alternatively, if you have Haskell Stack, you can type
stack install
Either of these commands will install logix to wherever your default location is for cabal installations.
After you install logix, assuming the location of the executable on your path, you can start it up as follows:
$ logix
LogiX (Logic Explorer) v0.2.1
a customizable proof construction tool for sequent calculi
(c) Ben Selfridge 2017
Type "help" for a list of commands.
>
For a full list of commands, type help. The only thing you need to know that
isn't in the help listing is the correct format for formulas and sequents. As an
illustrative example, the following command will begin a proof session with the
sequent a | b => ~(~a & ~b) & (b <-> b):
> top a | b => ~(~a & ~b) & (b <-> b)
Changing goal to "a ∨ b ⇒ ¬(¬a & ¬b) & (b ↔ b)".
The important thing is to remember the special symbols; => is the sequent
separator, which divides the left- and right-hand sides of a sequent. The binary
operators &, |, ->, and <-> are self-explanatory. ~ is unary
negation. _|_ is bottom, or false. a <-> b and ~a are both just abbreviations
for (a -> b) & (b -> a) and (a -> _|_), respectively. Quantifiers are input via
forall x. P(x) and exists x. P(x). Below is an illustration of how we would
begin a proof that the classic "Barber's paradox" is unsatisfiable:
> top => ~exists x. (Man(x) & forall y. (Man(y) -> (Shaves(x,y) <-> ~Shaves(y,y))))
Changing goal to " ⇒ ¬∃x.(Man(x) & ∀y.(Man(y) ⊃ (Shaves(x, y) ↔ ¬Shaves(y, y))))".
By default, logix displays sequents using unicode symbols for all these connectives,
but you can turn that off with the unicode command.
If you enter the sequent incorrectly, logix will report a parse error and not give you any helpful information.
We note here that the logical connectives used in the examples above are specific to the particular calculi that come with logix in src/Calculi.hs, and are not built-in. Every calculus in logix is defined completely separately from the core deduction engine.
To extend logix with your own sequent calculi, edit the file src/Calculi.hs encode the calculus using the other calculi as models. It's pretty easy to define your own connectives and abbreviations, and the examples in there should be straightforward to imitate. logix is intended to allow encodings of arbitrary sequent calculi, so if you have something you can't express with the tools provided, please let me know.
I am currently planning to add a mechanism for theory-building via axioms/assumptions
and theorems. This would enable one to build the theory of groups into a logix
session and prove theorems about groups without having to use cumbersome formulas
every time. Axioms would be top-level assumptions that would be automatically
inserted into the left-hand side of every goal sequent initiated by the top
command. Theorems would be similarly inserted. We would abbreviate axioms and
theorems by their names wherever they appear verbatim in a sequent. My goal is to
make working with theories like Group as straightforward and clean as possible; right
now, it's technically possible to do group theory, but I don't want to because I have
to mentally parse the entire set of group axioms every time I want to figure out
which rule to apply. Abbreviations and top-level axioms/theorems are necessary to do
anything useful, so that is definitely coming.
Please contact me if you have any feedback or questions, and especially if you discover a bug.
[1] Negri, Sara, Aarne Ranta, and Jan Von Plato. Structural Proof Theory. Cambridge: Cambridge U, 2000. Print.