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 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)

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é 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)

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)

The task of data collection is becoming routine in many disciplines and this results in increased availability of data. This routinely collected data provides a valuable opportunity for analysis with a view to support evidence based decision making. In order to confidently leverage the data in support of decision making the most appropriate statistical method needs to be selected, and this can be difficult for an end user not trained in statistics. This paper outlines an application of argumentation to support (...) the analysis of clinical data, that uses Extended Argumentation Frameworks in order to reason with the meta-level arguments derived from preference contexts relevant to the data and the analysis objective of the end user. We outline a formalisation of the argument scheme for statistical model selection, its critical questions and the structure of the knowledge base required to support the instantiation of the arguments and meta-level arguments through the use of Z notation. This paper also describes the prototype implementation of argumentation for statistical model selection based on the Z specification outlined herein. (shrink)

The task of data collection is becoming routine in many disciplines and this results in increased availability of data. This routinely collected data provides a valuable opportunity for analysis with a view to support evidence based decision making. In order to confidently leverage the data in support of decision making the most appropriate statistical method needs to be selected, and this can be difficult for an end user not trained in statistics. This paper outlines an application of argumentation to support (...) the analysis of clinical data, that uses Extended Argumentation Frameworks in order to reason with the meta-level arguments derived from preference contexts relevant to the data and the analysis objective of the end user. We outline a formalisation of the argument scheme for statistical model selection, its critical questions and the structure of the knowledge base required to support the instantiation of the arguments and meta-level arguments through the use of Z notation. This paper also describes the prototype implementation of argumentation for statistical model selection based on the Z specification outlined herein. (shrink)

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)

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)

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)

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.

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)

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)

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.

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)

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)

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.

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)

We present three natural but distinct formalisations of Einstein’s special principle of relativity, and demonstrate the relationships between them. In particular, we prove that they are logically distinct, but that they can be made equivalent by introducing a small number of additional, intuitively acceptable axioms.

This paper takes up Berman and Hafner's (1993) challenge to model legal case-based reasoning not just in terms of factual similarities and differences but also in terms of the values that are at stake. The formal framework of Prakken and Sartor (1998) is applied to examples of case-based reasoning involving values, and a method for formalising such examples is proposed. The method makes it possible to express that a case should be decided in a certain way because that advances certain (...) values. The method also supports the comparison of conflicting precedents in terms of values, and it supports debates on the relevance of distinctions in terms of values. (shrink)

Le problème de la formalisation de la logique hégélienne a fait l'objet récemment d'études d'inspiration et d'importance diverses. II y a d'abord le travail d'envergure de Gotthard Guenther sur le projet d'une logique non-aristotélicienne, le long article de Michael Kosok et la note de F. G. Asenjo.

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)

This paper compares two ways of formalising defeasible deontic reasoning, both based on the view that the issues of conflicting obligations and moral dilemmas should be dealt with from the perspective of nonmonotonic reasoning. The first way is developing a special nonmonotonic logic for deontic statements. This method turns out to have some limitations, for which reason another approach is recommended, viz. combining an already existing nonmonotonic logic with a deontic logic. As an example of this method the language of (...) Reiter's default logic is extended to include modal expressions, after which the argumentation framework in default logic of [20, 22] is used to give a plausible logical analysis of moral dilemmas and prima facie obligations. (shrink)

In preference aggregation a set of individuals express preferences over a set of alternatives, and these preferences have to be aggregated into a collective preference. When preferences are represented as orders, aggregation procedures are called social welfare functions. Classical results in social choice theory state that it is impossible to aggregate the preferences of a set of individuals under different natural sets of axiomatic conditions. We define a first-order language for social welfare functions and we give a complete axiomatisation for (...) this class, without having the number of individuals or alternatives specified in the language. We are able to express classical axiomatic requirements in our first-order language, giving formal axioms for three classical theorems of preference aggregation by Arrow, by Sen, and by Kirman and Sondermann. We explore to what extent such theorems can be formally derived from our axiomatisations, obtaining positive results for Sen’s Theorem and the Kirman-Sondermann Theorem. For the case of Arrow’s Theorem, which does not apply in the case of infinite societies, we have to resort to fixing the number of individuals with an additional axiom. In the long run, we hope that our approach to formalisation can serve as the basis for a fully automated proof of classical and new theorems in social choice theory. (shrink)