Ivo Pezlar

In this paper I will explore the question whether the Trivialization construction of transparent intensional logic (TIL) can be understood in terms of the Execution construction, specifically, in terms of its degenerate case known as the 0-Execution. My answer will be positive and the apparent contrast between the intuitive understanding of Trivialization and 0-Execution will be explained as a matter of distinct yet related informal perspectives, not as a matter of technical or conceptual differences.

Transparent intensional logic (TIL) is a well-explored type-theoretical framework for semantics of natural language. However, its treatment of polymorphic functions, which are essential for the analysis of various natural language phenomena, is still underdeveloped. In this paper, we address this issue and propose an extension of TIL that introduces polymorphism via type variables ranging over types and generalized variables ranging over constructions and types. Furthermore, we offer an analysis of sentences involving non-specific notional attitudes of the general form ‘_A_ considers (believes, desires, wants, seeks,...) something’.

In this paper, we will be interested in the notion of a computable proposition. It allows for feasible computational semantics of empirical sentences, despite the fact that it is in general impossible to get to the truth value of a sentence through a series of effective computational steps. Specifically, we will investigate two approaches to the notion of a computable proposition based on constructive type theory and transparent intensional logic. As we will see, the key difference between them is their accounts of denotations of empirical sentences.

In a recent paper by Tranchini (Topoi, 2019), an introduction rule for the paradoxical proposition ρ∗ that can be simultaneously proven and disproven is discussed. This rule is formalized in Martin-Löf’s constructive type theory (CTT) and supplemented with an inferential explanation in the style of Brouwer-Heyting-Kolmogorov semantics. I will, however, argue that the provided formalization is problematic because what is paradoxical about ρ∗ from the viewpoint of CTT is not its provability, but whether it is a proposition at all.

Nemonotónní logika vznikla za účelem systematicky zachytit tzv. zrušitelné uvažování, tj. typ každodenního uvažování, které vede jen k provizorně platným argumentům, jenž mohou být následně staženy s příchodem nových informací. Tím se ovšem nemonotónní logika dostává do ostrého kontrastu s klasickou logikou, která je monotónní, tj. žádné dodatečné premisy nemohou zrušit jednou již platné argumenty. To bylo pro mnohé dostatečným důvodem k tomu, aby nemonotónní logice upřeli status logiky. V tomto textu si ukážeme, že takový závěr je příliš unáhlený a že nemonotónní logika má právo se nazývat logikou.

Kosta Došen argued in his papers Inferential Semantics (in Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning, pp. 147–162. Springer, Berlin 2015) and On the Paths of Categories (in Piecha, T., Schroeder-Heister, P. (eds.) Advances in Proof-Theoretic Semantics, pp. 65–77. Springer, Cham 2016) that the propositions-as-types paradigm is less suited for general proof theory because—unlike proof theory based on category theory—it emphasizes categorical proofs over hypothetical inferences. One specific instance of this, Došen points out, is that the Curry–Howard isomorphism makes the associativity of deduction composition invisible. We will show that this is not necessarily the case.

Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient to proper propositions. The Curry–Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry–Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted.

The problem of hyperintensional contexts, and the problem of logical omniscience, shows the severe limitation of possible-worlds semantics which is employed also in standard epistemic logic. As a solution, we deploy here hyperintensional semantics according to which the meaning of an expression is an abstract structured algorithm, namely Tichý's construction. Constructions determine the denotata of expressions. Propositional attitudes are modelled as attitudes towards constructions of truth values. Such a model of belief is, of course, inferentially restrictive. We therefore also propose a model of implicit knowledge, which is the collection of a possible agent's explicit beliefs which are related through a derivation system mastered by the agent. A derivation system consists of beliefs and derivation rules by means of which the agent may derive beliefs different from the beliefs she is actually related to. Conditions imposed on the set of base beliefs and the set of rules capture the limitations of the agent's deriving capabilities.

The main objective of this paper is to sketch unifying conceptual and formal framework for inference that is able to explain various proof techniques without implicitly changing the underlying notion of inference rules. We base this framework upon the so-called two-dimensional, i.e., deduction to deduction, account of inference introduced by Tichý in his seminal work The Foundation’s of Frege’s Logic (1988). Consequently, it will be argued that sequent calculus provides suitable basis for such general concept of inference and therefore should not be seen just as technical tool, but philosophically well-founded system that can rival natural deduction in terms of its “naturalness”

In this paper we examine two approaches to the formal treatment of the notion of problem in the paradigm of algorithmic semantics. Namely, we will explore an approach based on Martin-Löf’s Constructive Type Theory, which can be seen as a direct continuation of Kolmogorov’s original calculus of problems, and an approach utilizing Tichý’s Transparent Intensional Logic, which can be viewed as a non-constructive attempt of interpreting Kolmogorov’s logic of problems. In the last section we propose Kolmogorov and CTT-inspired modifications to TIL-based approach. The focus will be on non-empirical problems only.

In this paper we revisit Pavel Tichý’s novel distinction between one-dimensional and two-dimensional conception of inference, which he presented in his book Foundations of Frege’s Logic (1988), and later in On Inference (1999), which was prepared from his manuscript by his co-author Jindra Tichý. We shall focus our inquiry not only on the motivation behind the introduction of this non-classical concept of inference, but also on further inspection of selected Tichý’s arguments, which we see as the most compelling or simply most effective in providing support for his two-dimensional account of inference. Main attention will be given to exposing the failure of one-dimensional theory of inference in its explanation of indirect (reductio ad absurdum) proofs. Lastly, we discuss shortly the link between two-dimensional inference and deduction apparatus of Tichý’s Transparent Intensional Logic.