Locality for classical logic. (English) Zbl 1131.03030

Brünnler, Kai

Notre Dame J. Formal Logic 47, No. 4, 557-580 (2006).

The scope of the paper under review is in the calculus of structures, a rather rapidly growing area founded by A. Guglielmi [“A system of interaction and structure”, ACM Trans. Comput. Log. 8, No. 1, 1–64 (2007)]. The propositional formulas of this calculus are generated by a countable set of atomic variables (\(p,q,r,\cdots\)) and the constants \({\mathtt t},{\mathtt f}\) (for truth and falsity), plus the structures \([S,T]\) and \((S,T)\) which are the disjunction and conjunction of the formulas \(S\) and \(T\). Negation \(\overline{S}\) of a formula \(S\) is defined inductively by de Morgan’s laws: \(\overline{{\mathtt t}}={\mathtt f}\), \(\overline{{\mathtt f}}={\mathtt t}\), \(\overline{[S,T]}=(\overline{S},\overline{T})\), \(\overline{(S,T)}=[\overline{S},\overline{T}]\), and \(\overline{\overline{S}}=S\). Predicate formulas are constructed by adding the quantifiers \(\forall\) and \(\exists\); their negations are also governed by de Morgan’s laws: \(\overline{\forall x R}=\exists x \overline{R}\) and \(\overline{\exists x R}=\forall x \overline{R}\). A formula context is a structure \(S\{\}\) with exactly one hole \(\{\}\); the formula \(S\{R\}\) results from \(S\{\}\) by filling the hole with the formula \(R\). The rules of this calculus are so-called “deep inference” in the sense that they can apply deep inside a formula of the premise. Thus the rules are of the form \(S\{T\} / S\{R\}\). The propositional fragment of the system studied in the paper is axiomatized by the identity rule \(S\{{\mathtt t}\} / S\{[R,\overline{R}]\}\), the cut rule \(S\{(R,\overline{R})\} / S\{{\mathtt f}\}\), the weakening rules \(S\{{\mathtt f}\} / S\{R\}\) and \(S\{R\} / S\{{\mathtt t}\}\), the switch rule \(S\{([R,U],T)\} / S\{[(R,T),U]\}\), and the contraction rules \(S\{[R,R]\} / S\{R\}\) and \(S\{R\} / S\{(R,R)\}\). The predicate counterpart also includes the rules \[ \begin{aligned} S\{\forall x [R,T]\} &/ S\{[\forall x R, \exists x T]\}, \\ S\{(\exists x R,\forall x T)\} &/ S\{\exists x (R,T)\}, \\ S\{R[x/t]\} &/ S\{\exists x R\}, \quad\text{and}\\ S\{\forall x R\} &/ S\{R[x/t]\}.\end{aligned} \]
It is proved in the paper that (the propositional and predicate fragments of) the above calculus is sound and complete, and moreover one can eliminate the cut rule. The significance of this calculus, over the sequent calculus, is that one can reduce the identity, cut, weakening and contraction rules to the atomic cases. And, for that, one needs to add the medial rules \[ \begin{aligned} S\{[(R,U),(T,V)]\} / S\{([R,T],[U,V])\} \quad &\text{(for the propositional part) and} \\ {\begin{aligned} S\{[\exists x R,\exists x T]\} &/ S\{\exists x [R,T]\},\\ S\{\forall x (R,T)\} &/ \{\forall x R,\forall x T\}, \\ S\{[\forall x R,\forall x T]\} &/ S\{\forall x [R,T]\}, \\ S\{\exists x (R,T)\} &/ S\{(\exists x R,\exists x T)\} \end{aligned}} \quad &\text{(for the predicate part).}\end{aligned} \]
This reduction to the atomic cases is not possible in the sequent calculus (see, e.g., the author’s paper [K. Brünnler, “Two restrictions on contraction”, Log. J. IGPL 11, No. 5, 525–529 (2003; Zbl 1051.03047)]), and, as the author argues, the above medial rules have no analogues in the sequent calculus.

Reviewer: Saeed Salehí (Zanjan)

MSC:

03F05	Cut-elimination and normal-form theorems
03F07	Structure of proofs

Keywords:

cut elimination; deep inference; locality; calculus of structures

Citations:

Zbl 1051.03047