Substructural logics Rules

Recall that X and Y on the left of sequents are not sets of formulae, but bunches of formulae. See the examples of non-classical proofs for details. The logical rules for introducing and eliminating connectives and quantifiers are the same for both the relevant logic R and the fuzzy logic F*:

Here Γ(X) is a bunch in which X occurs somewhere as a sub-bunch, so Γ(Y) is the result of replacing that specific occurrence of X by Y.

The basic structural rules governing the comma and the semicolon are also common to both logics, and are normally applied without comment, as in the classical case. Both operations are associative and commutative—that is, X,Y and X;Y are the same as Y,X and Y;X respectively, and (X,Y),Z and (X;Y);Z are the same as X,(Y,Z) and X;(Y;Z) respectively. The special object TEE satisfies the condition that TEE;X may replace or be replaced by X in any position in a bunch.

The comma additionally satisfies the two rules:

Note well that there is no vacuous discharge in the present formulation of these logics. We also do not allow the bunch of assumptions (the left side of a sequent) to be empty. Theorems are formulae derivable with just TEE on the left. Discharge is also strict in that only one instance of the assumption is discharged, even if that assumption occurs several times in the bunch.

The relevant logic R results from the basic system by adding the rule of importation:

Γ(X;Y)  ⊢  A	import
Γ(X,Y)  ⊢  A

The fuzzy logic F* results from the basic system by adding instead the converse rule of exportation:

Γ(X,Y)  ⊢  A	export
Γ(X;Y)  ⊢  A

An equivalent of importation is the rule of contraction for the semicolon:

Γ(X;X)  ⊢  A	W
Γ(X)  ⊢  A

Exportation is equivalent to weakening in the form:

Γ(X)  ⊢  A	K
Γ(X;Y)  ⊢  A

In proofs in R, we allow rule W to be used in place of importation wherever it is convenient to do so. Similarly, in F* we allow ourselves to use rule K directly instead of going through eK followed by exportation.

 

Substructural logics in the Proof Editor

In practice, it is tedious to write out all the low-level details of substructural proofs, so while the proof editor does accept R and F* in addition to classical logic, its handling of bunches is somewhat streamlined in comparison with the official version above. Firstly, associativity and commutativity are built in, so the bunch  X; ((Y; X); (Z; Y))  for example will be written as  X; X; Y; Y; Z  where the sub-bunches are simply listed in lexicographic order. The distinction between commas and semicolons is important, however, so parentheses must be used for example to distinguish  (X, Y); Z  from  X, (Y; Z). Secondly, since the comma symbolises set union, repetitions do not count in comma-separated bunches. Hence  X, Y, X  will be written as  X, Y. The effect of this is that the rule eW is never needed, as it is incorporated into the bunch notation exactly as in the usual classical system.

The structural rules are also incorporated in a way designed to make them easier to use. As noted, eW is avoided altogether. The eK rule is needed sometimes, but one appeal to it can cover any number of eK steps. The proof editor will accept the move from a sequent  X ⊢ A  to  Y ⊢ A  provided Y can be obtained from X by any number of applications of eK (and of course eW) which may be anywhere inside different sub-bunches.

In F*, the rules K and exportation allow weakening with respect to the semicolon as well as the comma. The proof editor does not distinguish between them, calling them both "weakening". In F*, eK also disappears, being absorbed into the weakening rule, so one step of weakening can encompass any number of applications of K (or exportation) and eK. It also allows vacuous discharge, just as in classical logic, in the rules IMPI, NOTI and RAA, so many proofs do not require the structural rules to be noted explicitly at all.

In R, there is no vacuous discharge, and no K, so explicit use of eK is sometimes required. However, R does have importation and its equivalent W. Again, the proof editor does not distinguish between them, allowing both (along with eW) under the name "contraction". Unlike the weakening rule, however, this only allows one semicolon to be treated per proof step. Explicit appeal to the contraction rule can sometimes be avoided as it is additionally built into the notion of assumption discharge. Two or more occurrences of an assumption in the same top-level bunch may be discharged together, as in:

SP {p IMP (p IMP q) ⊢ p IMP q} PL {1} {1} {p IMP (p IMP q)} {A} PL {2} {2} {p} {A} PL {1;2} {3} {p IMP q} {1, 2 IMPE} PL {1;2;2} {4} {q} {2, 3 IMPE} PL {1} {5} {p IMP q} {8 [2] IMPI} EP

The standard (unrestricted) quantifier rules are available, so proofs in full first order relevant and fuzzy logics can be edited with the tool. Restricted quantifiers are also implemented in the proof editor, as are the rules for free logic, so you may experiment with those if you wish.

Identity (=) can be given introduction and elimination rules very similar to those for classical logic, and the proof editor will accept it on that basis, but it should be noted that there is no consensus among supporters of relevant logic as to how identity should be handled. The existing rules allow us to prove the sequent  a = b  ⊢  (GOOD AND p) IMP p  (where GOOD is defined as NOTBAD) whose relevant validity is in doubt. For that reason, =I and =E have not been included among the official rules defining the logics.