Contexts

[lionelvaux]

Re,

The instructions suggest the use of Γ, Δ, etc. in formulas but these are usually intended to denote contexts, i.e. lists of rules. For instance, I can prove |-Γ,Γ^ by using the axiom rule in click-and-collect, but if Γ is thought to be a context this is not valid in general.

If one only looks at concrete examples, this is not an issue: we can simply say that all symbols are propositional variables. But if one is also interested in more abstract results, such as the derivability of some rules, then we need to give a special status to contexts to allow writing Γ^ or !Γ or ?Γ, and then forbid the use of the axiom rule on Γ,Γ^, or the promotion rule on ?Δ,!Γ.

As long as this issue is not settled, I would avoid the use of Γ in the example, and also forbid the user to interact with the rules that are given after the tutorial. In any case, while it is essential to keep the tutorial interactive, I think allowing this interaction in the list of rules is a bad idea: if one clicks somewhere by accident or reflex, there is no fool-proof way to recover the "official" list, other than reloading the page. See #14.

À plus, L.

[olaure01]

We followed logitext, and it has mostly to be considered as a hack. The current goal is indeed to focus on concrete examples. If we want to go further with open proofs, derivability, etc, indeed we will probably need to take contexts into account differently. However, in practice, it is not so wrong to consider context as atoms, since anyway click&coLLect is not supposed to be a tool for formal results so far, consider using Yalla for that.

[olaure01]

Trying to think a bit about this idea of first-class contexts, here is a proposal:

• Contexts are generated by a restriction of the grammar of formulas using only unary constructs: ℂ ::= Γ | Γ^ | !ℂ | ?ℂ with Γ^ extended to ℂ^ in the usual way for the user inputs
• The only rules which can be applied are on ?Γ (dereliction, weakening, contraction), possibly represented with double lines to stress the fact that they represent (potentially) multiple applications of basic rules

Are there other uses of contexts to have in mind?

[lionelvaux]

This patch would indeed forbid incorrect application of rules but now that I see it written down, it feels like a hack upon a hack, and I begin to believe that first-class contexts were a bad idea in the first place!

In logitext, a patch along those lines (for instance, simply forbidding the application of connectives other than negation to contexts) might do the trick because, in classical logic, one can choose the version of each rule that leaves contexts unchanged in each premise (except for the trick of renaming bound variables in the right rule of forall/the right rule of exists).

But linear logic imposes a explicit management of contexts. For instance, in exploring the general shape of a cut free proof by focusing on a given formula in the sequent, one might want to split an indeterminate context Γ in two parts, to be routed in separate branches of a tensor rule. But this is only worth the effort if we want to be able to represent generic, open proofs that we can then reason about.

If the goal remains to write down closed proofs of provable sequents, I would rather forget about contexts altogether. And I believe this is the most reasonable route if we want to keep small-step cut elimination as a possible second stage.

[olaure01]

I still believe there is something interesting to do for exporting/playing with open proofs (not for exploring them). Being able to split a context goes too far I think, but if the user anticipates enough context pieces in the goal to be able to apply splitting rules like the tensor one, he could write down the proof he wants and export it.

I see no particular interaction with the questions around cut-elimination.