focused proof
   HOME

TheInfoList



OR:

In mathematical logic, focused proofs are a family of analytic proofs that arise through goal-directed proof-search, and are a topic of study in structural proof theory and reductive logic. They form the most general definition of ''goal-directed'' proof-search—in which someone chooses a formula and performs hereditary reductions until the result meets some condition. The extremal case where reduction only terminates when axioms are reached forms the sub-family of ''uniform'' proofs. A sequent calculus is said to have the focusing property when focused proofs are complete for some terminating condition. For
System LK In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
,
System LJ In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
, and System LL, uniform proofs are focused proofs where all the atoms are assigned negative polarity. Many other sequent calculi has been shown to have the focusing property, notably the nested sequent calculi of both the classical and intuitionistic variants of the modal logics in the S5 cube.


Uniform proofs

In the sequent calculus for an
intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of f ...
logic, the uniform proofs can be characterised as those in which the upward reading performs all right rules before the left rules. Typically, uniform proofs are not complete for the logic i.e., not all sequents or formulas admit a uniform proof, so one considers fragments where they are complete e.g., the hereditary Harrop fragment of
Intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of f ...
logic. Due to the deterministic behaviour, uniform proof-search has been used as the control mechanism defining the
programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...
paradigm of
logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
. Occasionally, uniform proof-search is implemented in a variant of the sequent calculus for the given logic where context management is automatic thereby increasing the fragment for which one can define a logic programming langue.


Focused proofs

The focusing principle was originally classified through the disambiguation between synchronous and asynchronous connective in Linear Logic i.e., connectives that interact with the context and those that do not, as consequence of research on
logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
. They are now an increasingly important example of control in reductive logic, and can drastically improve proof-search procedures in industry. The essential idea of focusing is to identify and coalesce the non-deterministic choices in a proof, so that a proof can be seen as an alternation of negative phases ( where invertible rules are applied eagerly), and positive phases (where applications of the other rules are confined and controlled).


Polarisation

According to the rules in the sequent calculus, formulas are canonically put into one of two classes called ''positive'' and ''negative'' e.g., in LK and LJ the formula \phi \lor \psi is positive. The only freedom is over atoms are assigned a polarity freely. For negative formulas provability is invariant under the application of a right rule; and, dually, for a positive formulas provability is invariant under the application of a left rule. In either case one can safely apply rules in any order to hereditary sub-formulas of the same polarity. In the case of a right rule applied to a positive formula, or a left rule applied to a negative formula, one may result in invalid sequents e.g., in LK and LJ there is no proof of the sequent B \lor A \implies A \lor B beginning with a right rule. A calculus admits the ''focusing principle'' if when an original reduct was provable then the hereditary reducts of the same polarity are also provable. That is, one can commit to focusing on decomposing a formula and its sub-formulas of the same polarity without loss of completeness.


Focused system

A sequent calculus is often shown to have the focusing property by working in a related calculus where polarity explicitly controls which rules apply. Proofs in such systems are in focused, unfocused, or neutral phases, where the first two are characterised by hereditary decomposition; and the latter by forcing a choice of focus. One of the most important operational behaviours a procedure can undergo is ''backtracking'' i.e., returning to an earlier stage in the computation where a choice was made. In focused systems for classical and Intuitionistic logic, the use of backtracking can be simulated by pseudo-contraction. Let \uparrow and \downarrow denote change of polarity, the former making a formula negative, and the latter positive; and call a formula with an arrow neutral. Recall that \lor is positive, and consider the neutral polarized sequent \downarrow \uparrow \phi \lor \psi \implies \uparrow \phi \lor \psi, which is interpreted as the actual sequent \phi \lor \psi \implies \phi \lor \psi. For neutral sequents such as this, the focused system forces on to make an explicit choice of which formula to focus on, denoted by \langle \, \rangle . To perform a proof-search the best thing is to choose the left formula, since \lor is positive, indeed (as discussed above) in some cases there are no proofs where the focus is on the right formula. To overcome this, some focused calculi create a backtracking point such that focusing on the right yields \downarrow \uparrow \phi \lor \psi \implies \langle \phi \lor \psi \rangle, \uparrow \phi \lor \psi, which is still as \phi \lor \psi \implies \phi \lor \psi. The second formula on the right can be removed only when the focused phase has finished, but if proof-search gets stuck before this happens the sequent may remove the focused component thereby returning to the choice e.g., \downarrow \uparrow B \lor A \implies \langle A \rangle, \uparrow A \lor B must be taken to \downarrow \uparrow B \lor A \implies \uparrow A \lor B as no other reductive inference can be made. This is a pseudo-contraction since it has the syntactic form of a contraction on the right, but the actual formula doesn't exist i.e., in the interpretation of the proof in the focused system the sequent has only one formula on the right.


References

{{Reflist Logic Proof theory Reductionism Logic programming