|
|
|
|
X, A, B ⊢ Y |
AND ⊢ |
|
X, A AND B ⊢ Y |
|
|
|
|
X1 ⊢ A, Y1 |
X2 ⊢ B, Y2 |
⊢ AND |
|
X1, X2 ⊢ A AND B, Y1, Y2 |
|
|
|
X1, A ⊢ Y1 |
X2, B ⊢ Y2 |
OR ⊢ |
|
X1, X2, A OR B ⊢ Y1, Y2 |
|
|
|
|
X ⊢ A, B, Y |
⊢ OR |
|
X ⊢ A OR B, Y |
|
|
|
X ⊢ A, Y |
NOT ⊢ |
|
X, NOTA, ⊢ Y |
|
|
|
|
X, A ⊢ Y |
⊢ NOT |
|
X ⊢ NOTA, Y |
|
|
|
X1 ⊢ A, Y1
|
X2, B ⊢ Y2
|
IMP ⊢
|
|
X1, X2, A IMP B ⊢ Y1, Y2,
|
|
|
|
|
X, A ⊢ B, Y |
⊢ IMP |
|
X ⊢ A IMP B, Y |
|
|
|
X, Atv ⊢ Y |
ALL ⊢ |
|
X, ALLv A ⊢ Y |
|
|
|
| X ⊢ A, Y |
⊢ ALL |
m not in any
formula in X or Y |
|
X ⊢ ALLv Avm, Y |
|
|
|
X, A ⊢ Y |
SOME ⊢ |
m not in any
formula in X or Y |
|
X, SOMEv Avm ⊢ Y |
|
|
|
|
X ⊢ Atv, Y |
⊢ SOME |
|
X ⊢ SOMEv A, Y |
|
|
|
In reading the rules, it must be remembered that the objects on
the two sides of each sequent are sets, so for instance
X, A, B is the set X ∪
{A, B} where it is allowed that A
or B, or even both of them, may be members
of X. In all of the rules, X and Y
are whatever occurs above or below the line in addition to the
specified formulae, and may be any sets of formulae
whatsoever. In particular, they may be empty.
Note that the structural rule of monotonicity (or weakening) is
not stipulated explicitly as one of the primitive rules of the
system, but it holds anyway in virtue of the general form taken
by the axiom (rule A). Contraction is also not explicitly
assumed, but it also holds, because the formulae are taken in
sets and X ∪ X is the same set
as X. The other standard structural rule of exchange
(permuting the order of formulae on one side of a sequent) holds
because this is another property of set union.