The aim of this paper is to present a constructive solution to Frege's puzzle (largely limited to the mathematical context) based on type theory. Two ways in which an equality statement may be said to have cognitive significance are distinguished. One concerns the mode of presentation of the equality, the other its mode of proof. Frege's distinction between sense and reference, which emphasizes the former aspect, cannot adequately explain the cognitive significance of equality statements unless a clear identity criterion for (...) senses is provided. It is argued that providing a solution based on proofs is more satisfactory from the standpoint of constructive semantics. (shrink)

I argue against the interpretation of propositions as intentions and proof-objects as fulfillments proposed by Heyting and defended by Tieszen and van Atten. The idea is already a frequent target of criticisms regarding the incompatibility of Brouwer’s and Husserl’s positions, mainly by Rosado Haddock and Hill. I raise a stronger objection in this paper. My claim is that even if we grant that the incompatibility can be properly dealt with, as van Atten believes it can, two fundamental issues indicate that (...) the interpretation is unsustainable regardless: (1) it is hard to determine, without appealing to propositional intentions on pain of circularity, what intention a proof-object should be understood as a fulfillment of; (2) due to a difficult fulfillment dilemma, it is unclear, at best, what the object of an intention corresponding to a proposition is. (shrink)

In a series of papers Ladyman and Presnell raise an interesting challenge of providing a pre-mathematical justification for homotopy type theory. In response, they propose what they claim to be an informal semantics for homotopy type theory where types and terms are regarded as mathematical concepts. The aim of this paper is to raise some issues which need to be resolved for the successful development of their types-as-concepts interpretation.

It is often claimed that the theory of function levels proposed by Frege in Grundgesetze der Arithmetik anticipates the hierarchy of types that underlies Church’s simple theory of types. This claim roughly states that Frege presupposes a type of functions in the sense of simple type theory in the expository language of Grundgesetze. However, this view makes it hard to accommodate function names of two arguments and view functions as incomplete entities. I propose and defend an alternative interpretation of first-level (...) function names in Grundgesetze into simple type-theoretic open terms rather than into closed terms of a function type. This interpretation offers a still unhistorical but more faithful type-theoretic approximation of Frege’s theory of levels and can be naturally extended to accommodate second-level functions. It is made possible by two key observations that Frege’s Roman markers behave essentially like open terms and that Frege lacks a clear criterion for distinguishing between Roman markers and function names. (shrink)

The Covid-19 pandemic creates an unprecedented threatening situation worldwide with an urgent need for critical reflection and new knowledge production, but also a need for imminent action despite prevailing knowledge gaps and multilevel uncertainty. With regard to the role of research ethics in these pandemic times some argue in favor of exceptionalism, others, including the authors of this paper, emphasize the urgent need to remain committed to core ethical principles and fundamental human rights obligations all reflected in research regulations and (...) guidelines carefully crafted over time. In this paper we disentangle some of the arguments put forward in the ongoing debate about Covid-19 human challenge studies and the concomitant role of health-related research ethics in pandemic times. We suggest it might be helpful to think through a lens differentiating between risk, strict uncertainty and ignorance. We provide some examples of lessons learned by harm done in the name of research in the past and discuss the relevance of this legacy in the current situation. (shrink)

It is shown that in a linearly ordered MV-algebra A , the implication is unique if and only if the identity function is the unique De Morgan automorphism on A . Modulo categorical equivalence, our uniqueness criterion recalls Ohkuma's rigidness condition for totally ordered abelian groups. We also show that, if A is an Archimedean totally ordered MV-algebra, then each non-trivial De Morgan automorphism of the underlying involutive lattice of A yields a new implication on A , which is not (...) isomorphic to the original implication. (shrink)

In this paper, I revisit Frege's theory of sense and reference in the constructive setting of the meaning explanations of type theory, extending and sharpening a program–value analysis of sense and reference proposed by Martin-Löf building on previous work of Dummett. I propose a computational identity criterion for senses and argue that it validates what I see as the most plausible interpretation of Frege's equipollence principle for both sentences and singular terms. Before doing so, I examine Frege's implementation of his (...) theory of sense and reference in the logical framework of Grundgesetze, his doctrine of truth values, and views on sameness of sense as equipollence of assertions. (shrink)

My first aim in this paper is to use time diagrams in the style of Brentano to analyze constructions in Brouwer's separable mathematics more precisely. I argue that constructions must involve not only pairing and projecting as basic operations guaranteed by the intuition of twoity, as sometimes assumed in the literature, but also a recalling operation. My second aim is to argue that Brouwer's views on the intuition of twoity and arithmetic lead to an ontological explosion. Redeveloping the constructions of (...) natural numbers and systems sketched in an appendix to Brouwer's Cambridge lectures, I observe that the only plausible way he can make some elementary arithmetic in his separable mathematics is by allowing for the same canonical number to be determined by multiple separable entities, resulting in an overabundant mathematical ontology. (shrink)

Susi offers a novel non-coherence theory of digital human rights to explain the change in meaning and scope of human rights rules, principles, ideas and concepts, and the interrelationships and related actors, when moving from the physical domain into the online domain. The transposition into the digital reality can alter the meaning of well-established offline human rights to a wider or narrower extent, impacting core concepts such as transparency, legal certainty and foreseeability. Susi analyses the 'loss in transposition' of some (...) core features of the rights to privacy and freedom of expression. The non-coherence theory is used to explore key human rights theoretical concepts, such as the network society approach, the capabilities approach, transversality, and self-normativity, and it is also applied to e-state and artificial intelligence, challenging the idea of the sameness of rights. This title is part of the Flip it Open programme and may also be available Open Access. Check our website Cambridge Core for details. (shrink)

This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...) implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. (shrink)

This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell, but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only primitive logical (...) connectives and necessity as the only primitive modal operator. The full source code is available online and has been typechecked with Lean 3.4.2. (shrink)

BackgroundHealth data-driven activities have become central in diverse fields (research, AI development, wearables, etc.), and new ethical challenges have arisen with regards to privacy, integrity, and appropriateness of use. To ensure the protection of individuals’ fundamental rights and freedoms in a changing environment, including their right to the protection of personal data, we aim to identify the ethical approaches adopted by scientists during intensive data exploitation when collecting, using, or sharing peoples’ health data.MethodsTwelve scientists who were collecting, using, or sharing (...) health data in different contexts in Sweden, were interviewed. We used systematic expert interviews to access these scientists’ specialist knowledge, and analysed the interviews with thematic analysis. Phrases, sentences, or paragraphs through which ethical values and norms were expressed, were identified and coded. Codes that reflected similar concepts were grouped, subcategories were formulated, and categories were connected to traditional ethical approaches.ResultsThrough several examples, the respondents expressed four different ethical approaches, which formed the main conceptual categories: consideration of consequences, respect for rights, procedural compliance, and being professional.ConclusionsTo a large extent, the scientists’ ethical approaches were consistent with ethical and legal principles. Data sharing was considered important and worth pursuing, even though it is difficult. An awareness of the complex issues involved in data sharing was reflected from different perspectives, and the respondents commonly perceived a general lack of practical procedures that would by default ensure ethical and legally compliant data collection and sharing. We suggest that it is an opportune time to move on from policy discussions to practical technological ethics-by-design solutions that integrate these principles into practice. (shrink)

Schoolgirls writing short stories have surrendered themselves to some rules of a game, which, according to Ricoeur and Gadamer, delimits a field where everything ’is played’, and thereby, ’shatters the seriousness’ of ’the self-presence of a subject’. This article proposes that this field has a serious side of its own that reveals something true about the everyday reality of being a girl. The proposed worlds in the girls’ short stories are places from which research on women’s lives should begin is (...) a central argument, along with the contention that for the researcher to be able to take the seriousness of this playful writing into account, she also has to assume the position of a playful figure. The article suggests that the empirical data of schoolgirl writing invited the researcher to think Ricoeur and feminist epistemology together. Further, a suggestion is that the roles of reading given by the texts have consequences for a ’new’ process-oriented writing pedagogy and the teacher of writing as well. (shrink)

Abstract The role accorded to the public by scientists and philosophers of science has undergone an essential historical change in the last three centuries. Public participation in (witnessing of) scientific experiments was considered an important requirement for 17th century experimenters (e.g. for Boyle or Pascal). The cognitive role played by lay persons was later substantially downgraded; witnessing went out of fashion, while science became more and more esoteric and a matter for experts only. Part of this process was that all (...) scientific disciplines became intensively compartmentalized and in consequence a rather puzzling or even paradoxical situation appeared: that the scientists themselves were and are being reduced epistemically to the status of lay persons, outside of their proper field of expertise (as was pointed out by J. Hardwig). The paper deals with some cognitive aspects of this historical process. (shrink)

Graphical AbstractThe finding that viruses with RNA and DNA genomes can recombine to produce chimeric entities provides valuable insights into the origin and evolution of viruses. It also substantiates the hypothesis that certain groups of DNA viruses could have emerged from plasmids via acquisition of capsid protein-coding genes from RNA viruses.

This paper aims to answer the question of whether or not Frege's solution limited to value-ranges and truth-values proposed to resolve the "problem of indeterminacy of reference" in section 10 of Grundgesetze is a violation of his principle of complete determination, which states that a predicate must be defined to apply for all objects in general. Closely related to this doubt is the common allegation that Frege was unable to solve a persistent version of the Caesar problem for value-ranges. It (...) is argued that, in Frege’s standards of reducing arithmetic to logic, his solution to the indeterminacy does not give rise to any sort of Caesar problem in the book. (shrink)

The aim of the present thesis is twofold. First we propose a constructive solution to Frege's puzzle using an approach based on homotopy type theory, a newly proposed foundation of mathematics that possesses a higher-dimensional treatment of equality. We claim that, from the viewpoint of constructivism, Frege's solution is unable to explain the so-called ‘cognitive significance' of equality statements, since, as we shall argue, not only statements of the form 'a = b', but also 'a = a' may contribute to (...) an extension of knowledge. Second, we study this higher-dimensional account of equality from a constructive (computational) standpoint and, based on these considerations, we offer a new perspective to the project proposed by Peter Aczel of developing conventions and notations for an informal style of doing mathematics in type theory. To that end, we adopt the cubical type theory of Angiuli, Favonia and Harper, a framework that can be seen as constructive refinement of the ideas of homotopy type theory. (shrink)

I discuss problems with Martin-Löf's distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf's claim that all judgments of the forms a : A and a = b : A are analytic is unfounded. As I shall show, when A evaluates to a dependent function type (x : (...) B) → C, all judgments of these forms fail to be analytic and therefore end up as synthetic. Going beyond the scope of Martin-Löf's original distinction, I also argue that all hypothetical judgments are synthetic and show how the analytic-synthetic distinction reworked here is capable of accommodating judgments of the forms A type and A = B type as well. Finally, I consider and reject an alternative account of analyticity as decidability and assess Martin-Löf's position on the analytic grounding of synthetic judgments. (shrink)

This article proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our presentation (...) to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman–Hilton duality. (shrink)

A new deontic logic, Action Type Deontic Logic, is presented. To motivate this logic, a number of benchmark cases are shown, representing inferences a deontic logic should validate. Some of the benchmark cases are singled out for further comments and some formal approaches to deontic reasoning are evaluated with respect to the benchmark cases. After that follows an informal introduction to the ideas behind the formal semantics, focussing on the distinction between action types and action tokens. Then the syntax and (...) semantics of Action Type Deontic Logic is presented and it is shown to meet the benchmarks. Finally, possibilities for further research are indicated. In the appendix, decidability of the satisfiability of formulas is proved via a technique known from monadic First Order Logic. (shrink)

This paper investigates the acquisition of residual verb second (V2) in three corpora consisting of data from Norwegian-English bilinguals (Emma, Emily, and Sunniva) in order to determine to what extent these structures are affected by cross-linguistic influence (CLI) from Norwegian V2. The three girls exhibit three different patterns with regard to the relevant constructions. They are very target-like in their use of auxiliaries in the relevant structures. However, when it comes to do-support, Emily and Sunniva are equally target-like, while Emma (...) mainly produces non-target-like structures. These either involve the omission of do, or non-target-like movement of a lexical verb. Furthermore, Emma also allows verb movement across the subject with both lexical verbs and auxiliaries in topicalized structures, suggesting that she has overgeneralized residual V2 across verb types and clause types. Emily, on the other hand, is very target-like in structures involving residual V2 in English, but also allows auxiliaries and dummy-do to move across the subject in topicalized structures, overgeneralizing residual V2 to apply to non-subject-initial declaratives. Finally, Sunniva, is very precocious and very target-like in all the relevant structures, which may be an indication of acceleration due to CLI from Norwegian V2. We discuss these results with reference to language balance, finding that the measures available to us suggest that the differences between the children cannot straightforwardly be explained by language dominance. Instead, we suggest that these results can be accounted for by ambiguity in the English system, leaving the data open to several possible interpretations when acquired in contact with the consistent V2 system in Norwegian. This has several consequences: (i) the three girls’ parsers interpret the input differently, (ii) differences between the three children are qualitative rather than quantitative, and (iii) there has to be some mechanism that ensures that the children can ‘recover’ from these non-target-like grammars. In this paper, we will focus on the first two issues. (shrink)

Robotic systems consisting of a neuron culture grown on a multielectrode array which is connected to a virtual or mechanical robot have been studied for approximately 15 years. It is hoped that these MEA-based robots will be able to address the problem that robots based on conventional computer technology are not very good at adapting to surprising or unusual situations, at least not when compared to biological organisms. It is also hoped that insights gained from MEA-based robotics can have applications (...) within human enhancement and medicine. In this paper, I argue that researchers within this field risk overstating their results by not paying enough attention to fundamental challenges within the field. In particular, I investigate three problems: the coding problem, the embodiment problem and the training problem. I argue that none of these problems have been solved and that they are not likely to be solved within the field. After that, I discuss whether MEA-based robotics should be considered pop science. Finally, I investigate the ethical aspects of this research. (shrink)

This comprehensive volume features the proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, held in Hangzhou, China on September 8-9 and 11-12, 2023. The collection offers a diverse range of papers that explore the intersection of logic, artificial intelligence, and law. With contributions from some of the leading experts in the field, this volume provides insights into the latest research and developments in the applications of logic in (...) these areas. It is an essential resource for researchers, practitioners, and students interested in the latest advancements in logic and its applications to artificial intelligence and law. (shrink)

BackgroundInnovations in technology have contributed to rapid changes in the way that modern biomedical research is carried out. Researchers are increasingly required to endorse adaptive and flexible approaches to accommodate these innovations and comply with ethical, legal and regulatory requirements. This paper explores how Dynamic Consent may provide solutions to address challenges encountered when researchers invite individuals to participate in research and follow them up over time in a continuously changing environment.MethodsAn interdisciplinary workshop jointly organised by the University of Oxford (...) and the COST Action CHIP ME gathered clinicians, researchers, ethicists, lawyers, research participants and patient representatives to discuss experiences of using Dynamic Consent, and how such use may facilitate the conduct of specific research tasks. The data collected during the workshop were analysed using a content analysis approach.ResultsDynamic Consent can provide practical, sustainable and future-proof solutions to challenges related to participant recruitment, the attainment of informed consent, participant retention and consent management, and may bring economic efficiencies.ConclusionsDynamic Consent offers opportunities for ongoing communication between researchers and research participants that can positively impact research. Dynamic Consent supports inter-sector, cross-border approaches and large scale data-sharing. Whilst it is relatively easy to set up and maintain, its implementation will require that researchers re-consider their relationship with research participants and adopt new procedures. (shrink)