A proof-theoretic view of necessity (Q2500817): Difference between revisions

In the language of classical propositional calculus let \(D\) be an axiom system and \[ \{\varphi_{11},\dots, \varphi_{m1}\},\dots,\{\varphi_{n1},\dots, \varphi_{nm_n}\} \] be a system of alternatives satisfying natural conditions. A sentence \(\varphi= \varphi_{k,\ell_k}\) is necessary for a sentence \(\psi\) if \(D,\varphi_{1i_1},\dots, \varphi,\dots,\varphi_{n,i_n}\models\psi\) (there is a potential proof of \(\psi\) from \(\varphi\)), but \(D,\varphi_{1i_1},\dots, \varphi_{\ell i_\ell},\dots, \varphi_{ni_n}\not\models\psi\) whenever \(\varphi_{\ell i_\ell}\neq \varphi\) (there is no potential proof of \(\psi\) not using \(\varphi\)). The paper consists of motivations, justifications and possible directions of applications.