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
right adjoint
B1,B2,B3...Bn

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

Where:

Combining Rules

Γright adjointΔ   Σright adjointΠ
Γ,Σright adjointΔ, Π
We can combine the above two rules to give the rule below the line.
Γright adjointA   Aright adjointΠ
Γright adjointΠ
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.

Aright adjointA
(I)

Cut Rule

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

This rule allows us to eliminate A from the result.

Can we interpret this in terms of subsets? cut rule

/\ Rules

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

Elimination Introduction
Γ,Aright adjointΔ
Γ,A/\Bright adjointΔ
(/\L1)
Γ,Bright adjointΔ
Γ,A/\Bright adjointΔ
(/\L2)
Γright adjointA,Δ   Σright adjointB,Π
Γ,Σright adjointΔ,Π,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 Δ.

conjunction elimination rule

\/ Rules

Here are the rules for disjunction (or).

Elimination Introduction
Γ,Aright adjointΔ   Σ,Bright adjointΠ
Γ,Σ,A\/Bright adjointΔ,Π
(\/L)
Γright adjointA,Δ
Γright adjointΔ,A\/B
(\/R1)
Γright adjointB,Δ
Γright adjointΔ,A\/B
\/R2)

-> Rules

Here are the rules for implication.

Elimination Introduction
Γright adjointA,Δ   Σ,Bright adjointΠ
Γ,Σ,A->Bright adjointΔ,Π
(->L)

Modus ponens

Γ,Aright adjointB,Δ
Γright adjointA->B,Δ
(->R)

Conditional proof

¬ Rules

Left Right
Γright adjointA,Δ
Γ,¬Aright adjointΔ
(¬L)
Γ,Aright adjointΔ
Γright adjoint¬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?

for all Rules

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

For an intuition about the quantifier rules, consider the rule (for allR). We cannot conclude that for allx 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.

Elimination Introduction
Γ,A[t/x]right adjointΔ
Γ,for allxAright adjointΔ
(for allL)
Γright adjointA[y/x],Δ
Γright adjointfor allxA,Δ
(for allR)

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 universal quantifier rule

there exists Rules

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

Elimination Introduction
Γ,A[y/x]right adjointΔ
Γ,there existsxAright adjointΔ
(there existsL)
Γright adjointA[t/x],Δ
Γright adjointthere existsxA,Δ
(there existsR)

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? exisensial qualifier

Weakening Rules

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

Elimination Introduction
Γright adjointΔ
Γ,Aright adjointΔ
(WL)
Γright adjointΔ
Γright adjointA,Δ
(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. weakening

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,Aright adjointΔ
Γ,Aright adjointΔ
(CL)
Γright adjointA,A,Δ
Γright adjointA,Δ
(CR)

Permutation Rules

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

Elimination Introduction
Γ,A,B,Σ]right adjointΔ
Γ,B,A,Σright adjointΔ
(PL)
Γright adjointΣ,A,B,Δ
Γright adjointΣ,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
 
_|_right adjointΔ
 

Ex falso quodlibet

 
Γright adjointT
 

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.

cover Modern Graph Theory (Graduate Texts in Mathematics, 184)

Terminology and Notation

Specific to this page here:

 

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

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.