Fol support

[McTano]

I realized when I was updating the wiki that I had forgotten to merge this branch.
It makes a small change to the tree->sequent converter which is necessary to make the FOL checker work.

Explanation from slack thread:

Basically, in order to get it to work, I've made use of the 'resolved' field and checkmark, which was just decorative before.
When we instantiate a universal, we need to leave the universally quantified formula unresolved, because we might use it again. That means that the first image is correct, but the second one checks as incorrect.


Here's an example in the propositional logic:

marking row 1 as resolved makes it correct:

As before, if you try to use a formula that has already been discharged, you will get an error, which I've made more specific.

[McTano]

@drgilbert
I'd appreciate your feedback on the error messages.

Currently I've got these:

Formula at row _ is discharged more than once. (Try "unchecking" the formula.)

&

Incorrect use of resolution rule. (Did you forget to check off the resolved formula?)

[McTano]

This was a nice idea but would require rewriting the filter on the Carnap side to generate JSON.

[lf-]

I intend to look at this PR but currently I've deferred all work that can be deferred, possibly for up to a month or two, for very intense personal reasons.