User:Kaustuv/ip/Focusing

From Wikipedia, the free encyclopedia

This page is a user's work in progress page, not an article, and may be incomplete and/or unreliable. The current version of this article is, or will be located at Focusing (proof theory).

In proof theory, focusing or focalisation is a technique of analysing the polarity of the connectives of the logic to construct derived inference rules for clumps of logical connectives. The technique proceeds by first determining which non-deterministic choices are essential to the proof, and which are superfluous; it then removes the inessential choices. This technique was first discovered by the French mathematician Jean-Marc Andreoli in the domain of logic programming in linear logic^[1]; this technique has since been extended to many different logics^[2] and forms the core of ludics.

Contents 1 Formal definition 2 Bipoles 3 See also 4 References

[edit] Formal definition

This section presents a focused sequent calculus for classical propositional linear logic, closely following Andreoli.^[1] Let the syntax of propositions (A, B, …) be:

A, B, …	::=	p
	|	A ⊗ B | 1 | A ⊕ B | 0
	|	A & B | ⊤ | A ⅋ B | ⊥

where p are the atomic propositions. The rules are as follows:

(initial)

init ⊢ p, p⊥

(positive)

⊢ Γ, A     ⊢ Δ, B  ⊗ ⊢ Γ, Δ, A ⊗ B

1 ⊢ 1

⊢ Γ, A  ⊕1 ⊢ Γ, A ⊕ B

⊢ Γ, B  ⊕2 ⊢ Γ, A ⊕ B

(negative)

⊢ Γ, A     ⊢ Γ, B  & ⊢ Γ, A & B

⊤ ⊢ Γ, ⊤

⊢ Γ, A, B  ⅋ ⊢ Γ, A ⅋ B

⊢ Γ  ⊥ ⊢ Γ, ⊥

The rules in the third line, corresponding to the negative connectives &, ⊤, ⅋ and ⊥, are all invertible; that is, the conclusion of each rule entails the premisses. Given a proof of ⊢ Γ, A & B, for example, we can find proofs of ⊢ Γ, A and ⊢ Γ, B, from which we can reconstruct ⊢ Γ, A & B using the & rule. Therefore, when searching for a proof of ⊢ Γ, A & B, we can just as well use the & rule and search for proofs of ⊢ Γ, A and ⊢ Γ, B; this is sometimes known as inversion. If the sequent contains a number of such propositions with invertible rules, then we can invert all of them and the order in which they are inverted does not matter. Andreoli called such rules asynchronous because they can be applied whatever the form of the rest of the sequent.

In contrast, the rules in the second line, corresponding to the positive connectives ⊗, 1, ⊕ (and 0), are not invertible: their conclusions do not imply their premisses. For the 1 rule, this is understood to mean that the following equivalent formulation is not invertible:

Γ empty	1′.
⊢ Γ, 1

Searching for a proof of such propositions requires making essential choices; for example, for ⊗, a choice must be made to divide the context into two parts Γ and Δ to divide amongst the premisses, and for ⊕, a choice has to be made among the available rules ⊕₁ and ⊕₂. Thus, these propositions are both sensitive to the available rules and to the context; Andreoli called these rules synchronous.

The key insight of focusing is that the proofs of a given sequent can be divided into two synchronous and asynchronous phases. Reading from the conclusion to the premisses,

• in the asynchronous phase, all negative connectives in the sequent are decomposed in arbitrary order; and
• in the synchronous phase, a single positive proposition under focus is decomposed until it becomes negative.

Andreoli distinguished the two cases syntactically by means of two different sequent forms:

⊢ Γ ⇑ Σ	asynchronous phase (Σ a context of propositions)
⊢ Γ ⇓ A	synchronous phase with A under focus.

In each case, Γ contains only synchronous propositions or atoms.

In the asynchronous phase, the asynchronous connectives in Σ are decomposed in arbitrary order. The rule for these are:

⊢ Γ ⇑ Σ, A     ⊢ Γ ⇑ Σ, B  A& ⊢ Γ ⇑ Σ, A & B

A⊤ ⊢ Γ ⇑ Σ, ⊤

⊢ Γ ⇑ Σ, A, B  A⅋ ⊢ Γ ⇑ Σ, A ⅋ B

⊢ Γ ⇑ Σ  A⊥ ⊢ Γ ⇑ Σ, ⊥

If decomposing a negative proposition reveals a positive operand, then it is transferred into the positive context Γ:

Eventually the zone Σ will become empty; sequents of the form ⊢ Γ ⇑ · are called neutral sequents. A positive proposition is selected from the neutral sequent for focus:

The positive proposition is decomposed under focus, which is inherited by its operands.

⊢ Γ ⇓ A     ⊢ Δ ⇓ B  S⊗ ⊢ Γ, Δ ⇓ A ⊗ B

S1 ⊢ · ⇓ 1

⊢ Γ ⇓ A  S⊕1 ⊢ Γ ⇓ A ⊕ B

⊢ Γ ⇓ B  S⊕2 ⊢ Γ ⇓ A ⊕ B

If this decomposition produces a negative proposition, then we transition to the asynchronous phase.

This leaves just the atomic propositions. In Andreoli's original formulation, the atoms must be assigned a positive or a negative polarity, but the choice is arbitrary as long as p^⊥ has the opposite polarity from p. If the atom under focus has compatible polarity, then the proof is finished if and only if the context matches the focused proposition.

init ⊢ p⊥ ⇓ p

init⊥ ⊢ p ⇓ p⊥

If no other case can an initial rule be applied. If an atom is found in the asynchronous phase, it is transferred to the context Γ.

For example, consider the sequent

⊢ a, a^⊥ ⊗ (a ⅋ a), a^⊥ ⊗ (a ⅋ (a^⊥ ⊗ a^⊥)).

The following is a focused proof of it, where the focused propositions in the various decide rules are coloured differently and are inherited by their subformulas up to the next decide rule.

[edit] Bipoles

[edit] See also

• Ludics, a syntax for logic built with focusing as its core
• Jumbo lambda calculus, an alternative method of constructing large inference rules that doesn't fully coincide with focusing.

[edit] References

Category:Mathematical logic Category:Proof theory