In the current debate there are two epistemological approaches to the definition of ignorance: the Standard View and the New View. The former defines ignorance simply as not knowing, while the latter defines it as the absence of true belief. One of the main differences between these two positions lies in rejecting (Standard View) or in accepting (New View) the factivity of ignorance, i.e., if an agent is ignorant of φ, then φ is true. In the present article, we first (...) provide a criticism of the Standard View in favour of the New View. Secondly, we propose a formal setting to represent the notion of factive ignorance. (shrink)

A lot of attention has recently been devoted to the notion of Trustworthy AI (TAI). However, the very applicability of the notions of trust and trustworthiness to AI systems has been called into question. A purely epistemic account of trust can hardly ground the distinction between trustworthy and merely reliable AI, while it has been argued that insisting on the importance of the trustee’s motivations and goodwill makes the notion of TAI a categorical error. After providing an overview of the (...) debate, we contend that the prevailing views on trust and AI fail to account for the ethically relevant and value-laden aspects of the design and use of AI systems, and we propose an understanding of the notion of TAI that explicitly aims at capturing these aspects. The problems involved in applying trust and trustworthiness to AI systems are overcome by keeping apart trust in AI systems and interpersonal trust. These notions share a conceptual core but should be treated as distinct ones. (shrink)

This article investigates the connections between the logics of being wrong, introduced in Steinsvold (2011, Notre Dame J. Form. Log., 52, 245–253), and factive ignorance, presented in Kubyshkina and Petrolo (2021, Synthese, 198, 5917–5928). The first part of the paper provides a sound and complete axiomatization of the logic of factive ignorance that corrects errors in Kubyshkina and Petrolo (2021, Synthese, 198, 5917–5928) and resolves questions about the expressivity of the language. In the second half, it is shown that the (...) relationship between the two logics suggests an alternative axiomatization for the logic of factive ignorance, the adequacy of which is easily proved via straightforward translations. (shrink)

Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of NI\ is assumed to consist only of (...) \- and \-equations. On the basis of the categorial interpretation of NI\, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpreting NI\-derivations. We show that the Russell–Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. Finally we sketch how these results could be used to investigate the properties of connectives definable in the framework of higher-level rules. (shrink)

A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational interpretation of proofs and from the viewpoint of (...) proof-theoretic semantics. (shrink)

A comparison is given between two conditions used to define logical constants: Belnap's uniqueness and Hacking's deducibility of identicals. It is shown that, in spite of some surface similarities, there is a deep difference between them. On the one hand, deducibility of identicals turns out to be a weaker and less demanding condition than uniqueness. On the other hand, deducibility of identicals is shown to be more faithful to the inferentialist perspective, permitting definition of genuinely proof-theoretical concepts. This kind of (...) analysis is driven by exploiting the Curry–Howard correspondence. In particular, deducibility of identicals is shown to correspond to the computational property of eta expansion, which is essential in the characterization of propositional identity. (shrink)

An anti-realist theory of meaning suitable for both logical and proper axioms is investigated. As opposed to other anti-realist accounts, like Dummett-Prawitz verificationism, the standard framework of classical logic is not called into question. In particular, semantical features are not limited solely to inferential ones, but also computational aspects play an essential role in the process of determination of meaning. In order to deal with such computational aspects, a relaxation of syntax is shown to be necessary. This leads to a (...) general kind of proof theory, where the objects of study are not typed objects like deductions, but rather untyped ones, in which formulas have been replaced by geometrical configurations. (shrink)

Vlastos’ famous characterization of the Socratic elenchus focuses on two main aspects of this method: its epistemic roots and its dialogical nature. Our aim is to lay the groundwork to formally capture this characterization. To do so, first, we outline an epistemic framework in which the elenchus can be inscribed. More precisely, we focus our analysis on the passage from unconscious ignorance to conscious (or Socratic) ignorance and provide new insights about the epistemic outcome of an elenctic argument. Secondly, from (...) a logical perspective, we consider the elenchus as a dynamic exchange allowing Socrates’ respondents to revise their beliefs, on pain of inconsistency. By stressing this point, we represent this method as a process of belief revision in dynamic epistemic logic and provide a new logical solution to what Vlastos called the problem of the elenchus. (shrink)

In the current debate there are two epistemological approaches to the definition of ignorance. The Standard View defines ignorance simply as not knowing, while the New View defines it as the absence of true belief. We argue that both views provide necessary, but not sufficient conditions for ignorance, and thus do not constitute satisfactory definitions for such a notion.

In a previous paper we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models of polymorphic type theory. A different approach to extract proof-theoretic properties of natural deduction derivations was proposed in a recent series of papers on the basis of an embedding of intuitionistic propositional logic into a (...) predicative fragment of System F, called atomic System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification in terms of parametricity. (shrink)