Abstract

The paper focuses on treating partiality within Tichý’s logical system. Tichý’s logic is two-valued and type-theoretic. His simple theory of types (and the deduction system for it) accepts both total and partial functions. Tichý’s late framework is explicitly ramified. So-called constructions (roughly: algorithms) construct, e.g., values of functions at arguments; in some cases, however, they do not construct anything at all. This special partiality phenomenon is discussed in the second part of the paper.