Inversion in non-monotonic PTS
Antonio Piccolomini d'Aragona
Prawitz’s proof-theoretic semantics evaluates validity of proofs \(\models^{\texttt{P}}\) over atomic bases \(\mathfrak{B}\) and detour reductions. In current approaches, proofs and reductions are left out, and consequence \(\models\) is defined outright; a variant \(\models^{\texttt{S}}\), due to Sandqvist, deals with disjunction in an elimination-like way. \(\models^{\texttt{P}}\), \(\models\) and \(\models^{\texttt{S}}\) can be given in a monotonic or non-monotonic format, according to whether extensions of \(\mathfrak{B}\) are brought in when defining, by closure, consequence under assumptions. Completeness results have been proved on non-monotonic and monotonic \(\models\), and monotonic \(\models^{\texttt{S}}\) [2]. In the monotonic framework, these results adapt to \(\models^{\texttt{P}}\) modulo conditions for equivalence and completeness on \(\models^{\texttt{P}}\) [1]. I show that similar results hold in the non-monotonic approach too, via the following:
- \(\Gamma \models_\mathfrak{B} A \Leftrightarrow \Gamma \models^{\texttt{P}}_{\mathfrak{B}} A\),
- \(\Gamma \models A \Leftrightarrow \Gamma \models^{\texttt{P}} A\),
- \((\Gamma \models^{\texttt{S}}_{\mathfrak{B}} A \Rightarrow \Gamma \models^{\texttt{P}}_{\mathfrak{B}} A) \Rightarrow (\Gamma \models^{\texttt{P}}_{\mathfrak{B}} A \Rightarrow \Gamma \models^{\texttt{S}}_{\mathfrak{B}} A)\),
- \(\Sigma\) is \(\mathfrak{B}\)-complete (\(\mathfrak{B}\)-sound) on \(\Vdash\) iff \(\Gamma \Vdash_{\mathfrak{B}} A \Rightarrow \Gamma \vdash_{\Sigma \cup \mathfrak{B}} A\) (\(\Gamma \vdash_{\Sigma \cup \mathfrak{B}} A \Rightarrow \Gamma \Vdash_{\mathfrak{B}} A\)). Then, \(\Sigma\) \(\mathfrak{B}\)-complete on \(\models^{\texttt{S}} A\) and \(\mathfrak{B}\)-sound on \(\models^{\texttt{P}} \Rightarrow (\Gamma \models^{\texttt{S}} A \Leftrightarrow \Gamma \models^{\texttt{P}} A\) and \(\Sigma\) complete over \(\models^{\texttt{P}})\)
- \(\Sigma\) satisfies the export principle [2] \(\Rightarrow\) \(\Sigma\) not \(\mathfrak{B}\)-complete on \(\Vdash\).
1 also holds with classical meta-logic and a strict \(\models^{\texttt{P}}\) where closure is necessary but not sufficient for validity when \(\Gamma \neq \emptyset\). 3 also holds with \(\models\) and strict \(\models^{\texttt{P}}\).
Bibliography
- Antonio Piccolomini d’Aragona,Inversion and \(\mathfrak{B}\)-Completeness in Monotonic PTS,Forthcoming.
- Peter Schroeder-Heister,Proof-Theoretic Semantics,The Stanford Encyclopedia of Philosophy,(Edward N. Zalta, Uri Nodelman, editors).