# Maths - Sequent Calculus

In sequent calculus the notation for judgments is extended to have the following form:

 antecedent or context sequence of formulas considered conjunctively - all assumed to be true turnstile symbol succedent sequence of formulas considered disjunctively - at least one is true A1,A2,A3...An B1,B2,B3...Bn

This means that whenever every Ai is true then at least one Bi is true.

Where:

• A and B are formulae of first-order predicate logic (can also restrict this to propositional logic),
• Γ, Δ, Σ, and Π are finite, possibly empty, sequences of formulae called contexts. The order of formulae do not matter.

### Combining Rules

 Γ Δ Σ Π Γ,Σ Δ, Π
We can combine the above two rules to give the rule below the line.
 Γ A A Π Γ Π
If the antecedent of one rule is the same as the succedent of another rule it is possible to chain the rules together, cancelling out the common term. This is a special case of the cut rule below.

### Arguments, proofs or derivations in this language.

#### Identity Axiom Rule

'A' a given term is assumed to be true. So A implies itself. This has the role of the identity.

 A A
(I)

#### Cut Rule

 Γ Δ, A A, Σ Π Γ,Σ Δ, Π
(Cut)

This rule allows us to eliminate A from the result.

 Can we interpret this in terms of subsets? #### /\ Rules

Here are the rules for conjunction (and). Some versions of the introduction rule don't include Δ and Π.

Elimination Introduction
 Γ,A Δ Γ,A/\B Δ
(/\L1)
 Γ,B Δ Γ,A/\B Δ
(/\L2)
 Γ A,Δ Σ B,Π Γ,Σ Δ,Π,A/\B
(\/R)

As an example of how to interpret /\L1 it means whenever we can prove that Δ can be concluded from some sequence of formulae that contain A, then one can also conclude Δ from the stronger assumption, that A/\B holds. When Γ,A/\B is on the left side then it is equivalent to Γ,A,B so the rule is just saying that we can just add an arbitary B to the left hand side which is one of the weakening rules below.

 Here is an attempt to represent L1 in terms of subsets. This seems to work fine in these terms. that is if the intersection of Γ and A is a subset of Δ. then the intersection of Γ and A/\B must be a (possibly smaller) subset of Δ. #### \/ Rules

Here are the rules for disjunction (or).

Elimination Introduction
 Γ,A Δ Σ,B Π Γ,Σ,A\/B Δ,Π
(\/L)
 Γ A,Δ Γ Δ,A\/B
(\/R1)
 Γ B,Δ Γ Δ,A\/B
\/R2)

#### -> Rules

Here are the rules for implication.

Elimination Introduction
 Γ A,Δ Σ,B Π Γ,Σ,A->B Δ,Π
(->L)

Modus ponens

 Γ,A B,Δ Γ A->B,Δ
(->R)

Conditional proof

#### ¬ Rules

Left Right
 Γ A,Δ Γ,¬A Δ
(¬L)
 Γ,A Δ Γ ¬A,Δ
(¬R)

The rule (¬R) states that, if Γ and A suffice to conclude Δ, then from Γ alone one can either still conclude Δ or A must be false(¬A holds).

Note: no rules which imply excluded middle?

#### Rules

For universal quantifier we will use the notation x:σ.A(x) which is true if A(x) is true for every 'x' in type 'σ', where:

• is start of this universal quantifier syntax.
• x is a variable which ranges over given type.
• : means 'has type'.
• σ indicates the type.
• . seperator.
• A(x) is a predicate that is a function of x.

For an intuition about the quantifier rules, consider the rule ( R). We cannot conclude that x A holds just from A[y/x]. If, however, the variable y is not mentioned elsewhere (i.e. it can still be chosen freely, without influencing the other formulae), then one may assume, that A[y/x] holds for any value of y.

• t denotes an arbitrary term,
• x and y denote variables,
• A[t/x] means that A is a function of x where x is a free variable. By substituting the term t for every free occurrence of the variable x in formula A.
Elimination Introduction
 Γ,A[t/x] Δ Γ, xA Δ
( L)
 Γ A[y/x],Δ Γ  xA,Δ
( R)

The variable y must not occur free within Γ and Δ. Alternatively, the variable y must not appear anywhere in the respective lower sequents.

 In terms of subsets. Since x is a free element of the set #### Rules

For existential quantifier we will use the notation x:σ.A(x)

• t denotes an arbitrary term,
• x and y denote variables,
• A[t/x] denotes the formula that is obtained by substituting the term t for every free occurrence of the variable x in formula A, a variable is said to occur free within a formula if it occurs outside the scope of quantifiers or Elimination Introduction
 Γ,A[y/x] Δ Γ, xA Δ
( L)
 Γ A[t/x],Δ Γ  xA,Δ
( R)

The variable y must not occur free within Γ and Δ. Alternatively, the variable y must not appear anywhere in the respective lower sequents.

 Can we interpret this in terms of subsets? #### Weakening Rules

Weakening (W) allows the addition of arbitrary elements to a sequence. This is allowed:

• In the antecedent because we can always restrict the scope of our proof
• In the succedent because we can always allow for alternative conclusions.
Elimination Introduction
 Γ Δ Γ,A Δ
(WL)
 Γ Δ Γ A,Δ
(WR)
 Here is an attempt to represent weakening in terms of subsets. Adding 'A' to the antecedent makes it smaller and adding 'A' to the succedent makes it larger, both of which preserve the subset relationship. #### Contraction Rules

Idempotence of conjunction and disjunction.

As with sets, neither the order nor (in this case) multiples of occurrences of elements of the sequences matters.

Elimination Introduction
 Γ,A,A Δ Γ,A Δ
(CL)
 Γ A,A,Δ Γ A,Δ
(CR)

#### Permutation Rules

As with sets, neither the order nor multiple of occurrences of elements of the sequences matters.

Elimination Introduction
 Γ,A,B,Σ] Δ Γ,B,A,Σ Δ
(PL)
 Γ Σ,A,B,Δ Γ Σ,B,A,Δ
(PR)

#### T and _|_ Rules

If we assume false is true then any arbitary proposition is true.

True is always true and follows from anything.

Elimination Introduction
 _|_ Δ

Ex falso quodlibet

 Γ T

Tautology introduction

 metadata block see also: Correspondence about this page Book Shop - Further reading. Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them. Commercial Software Shop Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

This site may have errors. Don't use for critical systems.