Locality for classical logic
The scope of the paper under review is in the calculus of structures, a rather rapidly growing area founded by \textit{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 \textit{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 [\textit{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.
- On the length of medial-switch-mix derivations
- Locative ontology. I, II, III
- A Local System for Classical Logic
- Deep inference and symmetry in classical proofs
- scientific article; zbMATH DE number 4152550 (Why is no real title available?)
- Notions of locality and their logical characterizations over finite models
- A Local System for Intuitionistic Logic
- A proof calculus which reduces syntactic bureaucracy
- A logical basis for quantum evolution and entanglement
- A Characterization of Medial as Rewriting Rule
- Classical proof forestry
- Deep inference in proof search: the need for shallow inference
- Sequent systems on undirected graphs
- A strictly linear subatomic proof system
- Linearly distributive Fox theorem
This page was built for publication: Locality for classical logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2372689)
