Aspects of analytic deduction

Abstract

Let ⊢ be the ordinary deduction relation of classical first-order logic. We provide an “analytic” subrelation ⊢³ of ⊢ which for propositional logic is defined by the usual “containment” criterion

$$\Gamma \vdash ^a \varphi iff \Gamma \vdash \varphi and Atom(\varphi ) \subseteq Atom(\Gamma ),$$

whereas for predicate logic, ⊢^a is defined by the extended criterion

$$\Gamma \vdash ^a \varphi iff \Gamma \vdash \varphi and Atom(\varphi ) \subseteq ' Atom(\Gamma ),$$

where Atom(ϕ) $\subseteq '$ Atom(Γ) means that every atomic formula occurring in ϕ “essentially occurs” also in Γ. If Γ, ϕ are quantifier-free, then the notions “occurs” and “essentially occurs” for atoms between Γ and ϕ coincide. If ⊢ is formalized by Gentzen's calculus of sequents, then we show that ⊢^a is axiomatizable by a proper fragment of analytic inference rules. This is mainly due to cut elimination. By “analytic inference rule” we understand here a rule r such that, if the sequent over the line is analytic, then so is the sequent under the line. We also discuss the notion of semantic relevance as contrasted to the previous syntactic one. We show that when introducing semantic sequents as axioms, i.e. when extending the pure logical axioms and rules by mathematical ones, the property of syntactic relevance is lost, since cut elimination no longer holds. We conclude that no purely syntactic notion of analytic deduction can ever replace successfully the complex semantico-syntactic deduction we already possess.