Valuational semantics of rule derivability (Q1815405)

Syntactic Concepts. We work with an arbitrary but fixed sentential language \(L\), for which sequents are pairs \(\langle\Gamma,A \rangle\) with \(\Gamma \subseteq L\), \(A\in L\). An \(n\)-premiss rule \(\rho\) is an \((n+1)\)-ary relation on the set of sequents. If \(\langle \sigma_0, \dots, \sigma_n \rangle\in\rho\) then \(\sigma_n\) is the conclusion-sequent and \(\sigma_0, \dots, \sigma_{n-1}\) the premiss-sequents for the application \(\langle \sigma_0, \dots, \sigma_n \rangle\) of \(\rho\). A rule \(\rho\) is derivable from a set of rules \(R\) if every set of sequents closed under each rule in \(R\) is closed under \(\rho\). Structural rules are understood in the sense of Gentzen: as rules whose applications consist of all instantiations of a sequent-to-sequent schema in which no connective of \(L\) appears (by contrast with operational rules). Closure under certain structural rules is necessary and sufficient for a set of sequents to constitute a consequence relation; these are the rules \((\mathbb{R})=\) the zero-premiss rule \(\{ \langle \{A\}, A\rangle \mid A\in L\}\), \((\mathbb{M}) =\) the one-premiss rule \(\{\langle \langle \Gamma, A\rangle, \langle \Delta,A \rangle\rangle \mid \Gamma \subseteq \Delta \subseteq L\}\), and the cut or transitivity rule \((\mathbb{T})\) which we will further specify here. Let \(S= \{(\mathbb{R}), (\mathbb{M}), (\mathbb{T})\}\). Semantic Concepts. A valuation (for \(L)\) is a mapping from the set of formulas (of \(L)\) to the two element set \(\{T,F\}\) of truth-values. A sequent \(\sigma= \langle \Gamma,A \rangle\) holds on a valuation \(v\) if \(v(C)=T\) for all \(C\in\Gamma\) implies \(v(A)= T\). For a class \(V\) of valuations, we say sequent \(\sigma\) is \(V\)-valid if \(\sigma\) holds on each \(v\in V\). The local range, \(\text{Loc} (R)\), of a collection of rules \(R\) is the set of all valuations \(v\) such that for any \(\langle \sigma_0, \dots, \sigma_n \rangle\in\rho \in R\) if each of \(\sigma_0, \dots, \sigma_{n-1}\) holds on \(v\), then \(\sigma_n\) holds on \(v\). The global range, \(\text{Glo} (R)\), of a collection \(R\) of rules is the class of sets \(V\) of valuations such that for any \(\langle \sigma_0, \dots, \sigma_n \rangle \in\rho \in R\) if each of \(\sigma_0, \dots, \sigma_{n-1}\) is \(V\)-valid then \(\sigma_n\) is \(V\)-valid. The local and global consequence operations \(LCn\) and \(GCn\) are closure operations defined on the set of rules by: \[ LCn (R) = \biggl\{\rho \mid \text{Loc} (R) \subseteq \text{Loc} \bigl(\{\rho\} \bigr) \biggr\}, \quad GCn (R) = \biggl\{\rho\mid \text{Glo} (R) \subseteq \text{Glo} \bigl(\{\rho\} \bigr) \biggr\}. \] Connections. The main connection between the above syntactic and semantic concepts is given by: \(\rho\in GCn(R)\) if and only if \(\rho\) is derivable from \(R \cup S\). By contrast, the local consequences of a set of rules \(R\) are not guaranteed to be derivable from \(R\) with assistance of the structural rules \(S\). (Examples are given.) Reference. The role of the `global' concepts here is a vindication of the emphasis placed on them in a related context by \textit{J. W. Garson} [``Categorical semantics'', in: J. M. Dunn and A. Gupta (eds.), Truth or consequences: Essays in honor of Nuel Belnap, 155-175, Kluwer, Dordrecht (1990)].