A simple sequent calculus for partial functions (Q2367544)

A sequent calculus is developed for some three-valued logic, which can be used to talk about partial functions. At first, different possibilities for defining three-valued logics are presented, the advantages and disadvantages of these logics are discussed and reasons are given for preferring one of them. The calculus chosen is called WSL (weak-strong- logic). It uses sequents of the shape \(A \lvdash B\), \(A\) and \(B\) being formulas called hypothesis resp. consequent. If false -- nonfalse -- true are the truth-values, \(A \lvdash B\) is interpreted in this way that if the hypothesis is nonfalse, then the consequent is true. This is the most restrictive possibility. For instance, \(\lvdash A\Rightarrow A\), \(A \lvdash A\), and \(\frac{1}{0}=\frac{1}{0}\lvdash \frac{1}{0}\not=\frac{1}{0}\) are not valid in WSL. Especially, the first are to get accustomed to. The very advantage of WSL is that nothing can be proven from or about something undefined. The calculus is introduced for a finitely many-sorted language. Semantics is given in such a way that the function symbols are interpreted by strict functions. Thus side- conditions can be avoided, which are necessary in other logics. Therefore symmetry is preserved and close relations to the classical Gentzen system are kept. For instance, the deduction theorem is valid. Soundness and completeness are stated. The proof of cut elimination and a proposition on the expressive completeness of the system are sketched. The known well-definedness operator \(\Delta\) can be defined as a metasymbol in WSL. As other papers on this kind of topic, the paper under review does not contain an example for the application of the logical system in describing programs in computer science.