This paper contributes an analysis and formalisation of Damasio’s theory on core consciousness. Three important concepts in this theory are ‘emotion’, ‘feeling’ and ‘feeling a feeling’ . In particular, a simulation model is described of the dynamics of basic mechanisms leading via emotion and feeling to core consciousness, and dynamic properties are formally specified that hold for these dynamics at a more global level. These properties have been automatically checked for the simulation model. Moreover, a formal analysis is made (...) of relevant notions of representation used by Damasio. As part of this analysis, specifications of representation relations have been verified and confirmed against the simulation model. (shrink)

There is growing concern that decision-making informed by machine learning (ML) algorithms may unfairly discriminate based on personal demographic attributes, such as race and gender. Scholars have responded by introducing numerous mathematical definitions of fairness to test the algorithm, many of which are in conflict with one another. However, these reductionist representations of fairness often bear little resemblance to real-life fairness considerations, which in practice are highly contextual. Moreover, fairness metrics tend to be implemented in narrow and targeted toolkits that (...) are difficult to integrate into an algorithm’s broader ethical assessment. In this paper, we derive lessons from ethical philosophy and welfare economics as they relate to the contextual factors relevant for fairness. In particular we highlight the debate around acceptability of particular inequalities and the inextricable links between fairness, welfare and autonomy. We propose Key Ethics Indicators (KEIs) as a way towards providing a more holistic understanding of whether or not an algorithm is aligned to the decision-maker’s ethical values. (shrink)

Peut-on formaliser le vivant ? Peut-on réduire une plante à une simple formule mathématique ? Goethe ne l’aurait pas admis. Pour beaucoup encore, cette question ne se pose même pas tant elle peut sembler provocante et contre-nature. Dans une perspective à la fois historique et épistémologique, ce livre rend compte de travaux contemporains qui ont pourtant tous tenté de braver cet interdit. C’est en grande partie sur ce terrain, hautement problématique, que, dans les premières décennies du XXe siècle, on voit (...) naître puis s’épanouir la pratique des modèles mathématiques appliquée aux sciences végétales. On voit en particulier que ces pratiques nouvelles de modélisation entrent en concurrence avec une tradition ancienne de théorisation mathématique des formes du vivant. C’est même devant les limites des essais théoriques récurrents que le tournant formel des modèles se confirme et permet des avancées incontestables. À l’heure où toutes les sciences à objets complexes parlent beaucoup de modèles et moins de théories, est-ce le signe d’une victoire de la « modélisation » au détriment de la « théorie » ? Cette victoire est-elle définitive ? Cela a-t-il toujours un sens de les opposer ? Et qu’en est-il des « lois » ? En proposant une analyse des travaux mais aussi des positions épistémologiques de certains scientifiques impliqués, en explicitant le sens de ce qui les rapproche, de ce qui les distingue ou les oppose, cet ouvrage montre que l’émergence, l’expansion puis la diversification des pratiques de modélisation formelle du vivant ont contribué, sur le terrain scientifique lui-même, à bousculer les rapports épistémologiques traditionnels entre théories, lois et modèles tels qu’ils nous ont été légués par la physique. (shrink)

The intention of the presented paper is to establish within a certain modal semantic based on the situational ontology a description of the phenomenon of substantial change, which originally had been formulated within Aristotelian metaphysics – a theory based in reistic ontology. We understand substantial changesto be such changes whose subjects are primary substances (πρωται ουσι αι ) conceived as actually existing individual essences. The analysed changeability is of an existential character - it pertains to the existence of those substances. (...) The formalised description of the chosen changes, constructed in part (1) of the study, takes into consideration the necessary condition for their occurrence: the disappearing and coming into being of successively becoming substances. Part (2) presents the manner in which it is possible to reformulate the obtained characteristic of substantial change in order to create a description of a particular variety of situational changes, which belong, in turn, to the intended interpretation of modal sentential logic of change LCG - a calculus in which change is a primitive concept precised with the help of two one-argument operators C and G, read respectively as: it changes that…, a change is enabled by this, that ….. (shrink)

An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence.

Our everyday thinking consists of two steps: "forward" extending our beliefs, "backward" reducing them. The "forward" step is formalized by deductive logic, but existing logics formalising "rejected sentences" reasoning are unvalid for the "backward" reasoning. We need two logics: one for the set of accepted sentences, another for the set of rejected sentences. They work on the same class of sets, so the second component of the pair must be a reasoning decreasing sets of accepted sets.

RésuméL'objet du présent article est de dégager la signification philosophique des différents théoriémes de métamathématique relatifs à la puissance des formalisations. Ces théorèmes représentent la partie de l'épistémologie qui peut être exposée dans la forme technique de la science elle‐même et rassemblant les éléments d'une réflexion autocritique de la pensée mathématique sur elle‐même. Au‐delà, ils invitent à comprendre l'acte de la pensée mathématique comme déploiement d'un projet pensant supposant à la fois une initiative volontaire de la pensée, un champ intuitif (...) absolument indéfini et une exigence logique régulatrice, et amènent la philosophie de la science à se demander si, telles qu'ellcs sont, les mathématiques sont l'unique forme de synthèse rigoureuse possible entre ces trois moments de la pensée. (shrink)

We use a deep embedding of the display calculus for relation algebras RA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for RA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle/HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

Les tentatives de Michael Kosok, Dominique Dubarle,Clark Butler et Gotthard Günther de formaliser la logique dialectique de Hegel sont résumées et critiquées.

One of the basic principles of the general definition of information is its rejection of dataless information, which is reflected in its endorsement of an ontological neutrality. In general, this principles states that “there can be no information without physical implementation” (Floridi (2005)). Though this is standardly considered a commonsensical assumption, many questions arise with regard to its generalised application. In this paper a combined logic for data and information is elaborated, and specifically used to investigate the consequences of restricted (...) and unrestricted data-implementation-principles. (shrink)

ABSTRACTErnest Weinrib claims that the purpose of private law is to correct injustices between private parties and the use of private laws for consequentialist ends is a distortion. Weinrib’s primary argument highlights the distinctiveness of corrective justice and distributive justice. Weinrib claims to have an Aristotelian proof for their distinctiveness, but formalisation of and commentary on this aspect of his argument are lacking. This piece fills that gap in the literature. It provides purposely and strategically simple formal models of (...) the structure of corrective and distributive justice, and demonstrates that they are not reducible to one another and cannot be placed under a larger, non-trivial mathematical formula that generalises for even a large number of private law cases. (shrink)

We use a deep embedding of the display calculus for relation algebras ÆRA in the logical framework Isabelle /HOL to formalise a machine-checked proof of cut-admissibility for ÆRA. Unlike other “implementations”, we explicitly formalise the structural induction in Isabelle /HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules.

This book revisits psychology's appropriation of natural scientific methods. The author argues that, in order to overcome ongoing methodological debates in psychology, it is necessary to confront the problem of formalisation contained in the appropriation of methods of natural science. By doing so, the subject matter of psychology - the human being - and questions about the meaning of human existence can be brought to the centre of the discipline. Drawing on Garfinkel, Sacks, Edwards and Potter, the author sees (...) ethnomethodologically informed qualitative methods, which stem from phenomenology, as a possible alternative to statistical methods, but ultimately finds these methods to be just another method of formalisation.She returns to Husserlian phenomenology as a way to critique the centrality of method in psychology and shows that the adoption of natural scientific methods in psychology is part of the larger push to formalise and objectify all aspects of human existence. (shrink)

This paper is an exercise in the phenomenology of science. It examines the tendency to prefer formal accounts in a familiar body of experimental psychology. It will argue that, because of this tendency, psychologists of this school neglect those forms of human cognition typical of the humanities disciplines. This is not a criticism of psychology, however. Such neglect is compatible with scientific rigour, provided it does not go unnoticed. Indeed, reflection on the case in hand allows us to refine the (...) characterisation of the formalising tendency. (shrink)

Résumé Cet article examine la formalisation sémiotique de la traduction, proposée par Alexandre Ljudskanov, à travers la confrontation de son modèle avec celui de l’École de Leipzig. Alors que les allemands Kade et Neubert ne quittent pas le champ de la Translationslinguistik, le traductologue bulgare s’applique à mettre en œuvre une sémiotique du processus traductif. En partant de la prémisse que toute information n’existe que sous forme de code, il définit la traduction comme un échange communicatif entre deux systèmes (...) sémiotiques, qui demande forcément une médiation sémiotique de nature cognitive. Le modèle de Ljudskanov implique le décodage et l’encodage. Ces deux phases supposent la transformation des signes d’un code à l’autre de sorte à préserver l’information portée par le message. L’information invariante est transmise par des équivalents fonctionnels dont la pertinence et le principe de fonctionnement seront illustrés par des exemples de proverbes, d’aphorismes, d’expressions idiomatiques et leur traduction en plusieurs langues. (shrink)

Résumé Cet article examine la formalisation sémiotique de la traduction, proposée par Alexandre Ljudskanov, à travers la confrontation de son modèle avec celui de l’École de Leipzig. Alors que les allemands Kade et Neubert ne quittent pas le champ de la Translationslinguistik, le traductologue bulgare s’applique à mettre en œuvre une sémiotique du processus traductif. En partant de la prémisse que toute information n’existe que sous forme de code, il définit la traduction comme un échange communicatif entre deux systèmes (...) sémiotiques, qui demande forcément une médiation sémiotique de nature cognitive. Le modèle de Ljudskanov implique le décodage et l’encodage. Ces deux phases supposent la transformation des signes d’un code à l’autre de sorte à préserver l’information portée par le message. L’information invariante est transmise par des équivalents fonctionnels dont la pertinence et le principe de fonctionnement seront illustrés par des exemples de proverbes, d’aphorismes, d’expressions idiomatiques et leur traduction en plusieurs langues. (shrink)

An ontology is a domain of knowledge structured through formal rules so that it can be interpreted and used by computers. Ontologies are becoming increasingly important in bioinformatics because they can be linked to the information in databases and their knowledge then used to query the databases. Typical examples in current use are the Gene Ontology, which incorporates much of our knowledge about gene products, and ontologies of developmental anatomy, which, for example, facilitate tissue‐based queries to gene expression databases both (...) textually and spatially. This article considers the production, formulation and types of bio‐ontologies together with the reasons why they are so useful. © BioEssays 25:501–506, 2003. © 2003 Wiley Periodicals, Inc. (shrink)

Previous research into the formalisation of statute law identified a number of uses of language which posed problems for formalisation. A previous paper argued that these uses establish the requirement that a formalisation be isomorphic, but noted that this has odd consequences. This paper expands on what these consequences are and argues that they undermine the very idea of formalisation. Therefore, the whole argument constitutes a reductio ad absurdum of the idea of formalising statute law. The (...) paper provides reasons why this activity is impossible and places the conclusion in the context of the development of modem logic, in which context it appears uncontroversial. (shrink)

This paper presents a formal reconstruction of a Dutch civil legal case in Prakken’s formal model of adjudication dialogues. The object of formalisation is the argumentative speech acts exchanged during the dispute by the adversaries and the judge. The goal of this formalisation is twofold: to test whether AI & law models of legal dialogues in general, and Prakken’s model in particular, are suitable for modelling particular legal procedures; and to learn about the process of formalising an actual (...) legal dispute. (shrink)