Version 1.4.0

We have a new milestone! Version 1.4.0 is now available to download. There are a number of big changes in this release, and a lot has happened behind the interface.

The most exciting new feature is support for Modal/Hybrid Logic. There is also a limited implementation of some second-order logic, as well as some refreshed input and output options.

Modal/Hybrid Logic

As I mentioned, 1.4.0 brings support for some modal and hybrid logic operators. Specifically, the following operators are supported:

• [r] (box operator)
• <r> (diamond operator)
• @
• ↓

You're also now able to specify contexts for each line by prepending the line with [context]:. So b:p will create a new line with context b. If you don't specify a context, the line will be given a default context. To create a contextless line, create a line with a blank context, like :p.

To create a box operator, simply type [r] (or [s], [t]...). For a diamond operator, put <r>. @ operators behave in the same way as quantifiers. To get ↓, you'll need to copy/paste or use the new keyboard shortcuts (see below). This works as the quantifiers also.

The new rules are bundled in the rule palette. There is also the option to make contexts visible or invisible. Remember, you can save bundles of rules to custom rulesets.

Second-Order Logic

Very limited, experimental second-order logic has been added for universal elimination and existential introduction. You can activate this in the rule palette, under special rules.

Keyboard Shortcuts

You're now able to input special symbols using keyboard shortcuts. Symbols like + and &, which are already on the keyboard, are not included in this. To get the symbols, use Alt as your key mask (Command on Mac, I hope) and consult the following table:

Character	Shortcut
∨	Alt/Command + v
⊃	Alt/Command + .
≡	Alt/Command + 3
∀	Alt/Command + a
∃	Alt/Command + e
⋅	Alt/Command + 8
↓	Alt/Command + \

While these may not seem immediately obvious shortcuts, I hope they are, given the other symbols on the keys.

Export Changes

Export to text has been revamped in this version. It now supports identity boxes and displays lines for scopes and boxes.

Also added is ANIMATED GIFS. You can now export any proof to an animated gif! The gif will loop through the proof, with one second per frame, and pause on the conclusion. I've uploaded an example into the images folder.

My Axioms

It is now possible to specify axioms for use in a proof. These can be set from the My Axioms window under Options, and will behave like the Q axioms. You must specify line numbers, and the lines must be in TeX code format.