Statements not only update our current knowledge, but also have other dynamic effects. In particular, suggestions or commands ?upgrade' our preferences by changing the current order among worlds. We present a complete logic of knowledge update plus preference upgrade that works with dynamic-epistemic-style reduction axioms. This system can model changing obligations, conflicting commands, or ?regret'. We then show how to derive reduction axioms from arbitrary definable relation changes. This style of analysis also has a product update version (...) with preferences between actions, as well as worlds. Some illustrations are presented involving defaults and obligations. We conclude that our dynamic framework is viable, while admitting a further extension to more numerical ?utility update'. (shrink)

In this paper, illocutionary acts of commanding will be differentiated from perlocutionary acts that affect preferences of addressees in a new dynamic logic which combines the preference upgrade introduced in DEUL (dynamic epistemic upgrade logic) by van Benthem and Liu with the deontic update introduced in ECL II (eliminative command logic II) by Yamada. The resulting logic will incorporate J. L. Austin’s distinction between illocutionary acts as acts having mere conventional effects and perlocutionary acts as acts having (...) real effects upon attitudes and actions of agents, and help us understand why saying so can make it so in explicit performative utterances. We will also discuss how acts of commanding give rise to so-called “deontic dilemmas” and how we can accommodate most deontic dilemmas without triggering so-called “deontic explosion”. (shrink)

There are two important aspects of any democratic decision: aggregation of preferences and deliberation about preferences. They are essential and complementary components of any decision making process. While the well-studied process of aggregation focuses on accumulating individual preferences without discussing their origin [4], deliberation can be seen as a conversation through which individuals justify their preferences, a process that might lead to changes in their opinions as they get influenced by one another. Till now, there has been a lot of (...) work on the ‘aggregation’ aspect (e.g., [12, 14, 6]). However, some recent work has focussed on the deliberation aspect as well [8, 9, 10, 15]. Sometimes, deliberation does not lead to unanimity in preferences, but the discussion can lead to some ‘preference uniformity’ (see how deliberation can help in bypassing social choice theory’s impossibility results in [5]), which might facilitate their eventual aggregation. In addition, the combination of both processes provides a more realistic model for decision making scenarios. In light of this status quo, our focus is on the formal study of achieving such preference uniformities, e.g., single-peaked, single-caved, single-crossing, value-restricted, best-restricted, worst-restricted, medium-restricted, or group-separable profiles. In this short abstract we provide our preliminary ideas towards achieving singlepeakedness of preference profiles via deliberation. In what follows, we define two preference upgrade operators based on [8, 9] and provide a preliminary discussion on how single-peaked preference profiles can be achieved through such operations. We will delve into the details of the logical language in the main paper. (shrink)

For a long time, female endorsers in advertising have been doing product information promotion in the market. However, with more and more highly educated women participating in the labor force, the conception of feminist depictions in advertising have become a perplexing issue. The traditional female role portrayals or stereotypes of the past are not able to totally reflect the expectations, behavior, attitudes, and beliefs of contemporary women. The author collected print ads as data from three types of the highest circulation (...) magazines: foreign women’s magazines, domestic women’s magazines, and domestic management magazines subscribed to in Taiwan to investigate what were the favorite feminine patterns and feminist depictions in a traditionally masculine society. The results showed classical beauty and girl-next-door images were “acceptable” gender-role behavior exposed highly in domestic magazines, which might contribute to conservative Confucian beliefs. On the other hand, being trendy was a significantly high preference for contemporary feminist depictions in foreign women's magazines; it might be considered as being due to the increased educational level of women and female labor participation rate in the work place as well as upgrading of social status. (shrink)

In this dissertation we present proof systems for several modal logics. These proof systems are based on analytic (or semantic) tableaux. -/- Modal logics are logics for reasoning about possibility, knowledge, beliefs, preferences, and other modalities. Their semantics are almost always based on Saul Kripke’s possible world semantics. In Kripke semantics, models are represented by relational structures or, equivalently, labeled graphs. Syntactic formulas that express statements about knowledge and other modalities are evaluated in terms of such models. -/- This dissertation (...) focuses on modal logics with dynamic operators for public announcements, belief revision, preference upgrades, and so on. These operators are defined in terms of mathematical operations on Kripke models. Thus, for example, a belief revision operator in the syntax would correspond to a belief revision operation on models. -/- The ‘dynamic’ semantics of dynamic modal logics are a clever way of extending languages without compromising on intuitiveness. We present ‘dynamic’ tableau proof systems for these dynamic semantics, with the express aim to make them conceptually simple, easy to use, modular, and extensible. This we do by reflecting the semantics as closely as possible in the components of our tableau system. For instance, dynamic operations on Kripke models have counterpart dynamic relations between tableaux. -/- Soundness, completeness, and decidability are three of the most important properties that a proof system may have. A proof system is sound if and only if any formula for which a proof exists, is true in every model. A proof system is complete if and only if for any formula that is true in all models, a proof exists. A proof system is decidable if and only if any formula can be proved to be a theorem or not a theorem in a finite number of steps. All proof systems in this dissertation are sound, complete, and decidable. -/- Part of our strategy to create modular tableau systems is to delay concerns over decidability until after soundness and completeness have been established. Decidability is attained through the operations of folding and through operations on ‘tableau cascades’, which are graphs of tableaux. -/- Finally, we provide a proof-of-concept implementation of our dynamic tableau system for public announcement logic in the Clojure programming language. (shrink)

If the notion of speech acts is to be taken seriously, it must be possible to treat speech acts as acts. The development of systems of DEL (dynamic epistemic logic) in the last two decades suggests an interesting possibility. These systems are developed on the basis of static epistemic logics by introducing model updating operations to interpret various kinds of speech acts including public announcements as well as private information transmissions as what update epistemic states of agents involved. The methods (...) used in developing DEL can be used to develop logics that deal with a much wider variety of speech acts. For example, in ECL (Eliminative Command Logic) of Yamada (2007a) and ECL II of Yamada (2007b), similar model updating operations are introduced tointerpret acts of commanding as what update deontic aspects of the situations in which agents are involved. In Yamada (2008a), ECL II is further extended so as to model acts of promising along with acts of commanding. Moreover, in Yamada (2008b), ECL II is combined with a modified version of DEUL (dynamic epistemic upgrade logic) introduced in van Benthem & Liu (2007). In the resulting logic DDPL (dynamic deontic preference logic), illocutionary acts of commanding are differentiated from preference upgrading perlocutionary acts. The development of these logics suggests a recipe for developing logics that deal with various specific speech acts: first, carefully identify the aspects affected by the speech acts you want to study; second, find the modal logic that characterizes the aspects in question; and finally, add dynamic modalities that stand for the types of the speech acts being studied and define model updating operation that interprets these speech acts as what update the very aspects. (shrink)

Nonindexical Context-Dependence and the Interpretation as Abduction Approach Inclusive nonindexical context-dependence occurs when the preferred interpretation of an utterance implies its lexically-derived meaning. It is argued that the corresponding processes of free or lexically mandated enrichment can be modeled as abductive inference. A form of abduction is implemented in Simple Type Theory on the basis of a notion of plausibility, which is in turn regarded a preference relation over possible worlds. Since a preordering of doxastic alternatives taken for itself (...) only amounts to a relatively vacuous ad hoc model, it needs to be combined with a rational way of learning from new evidence. Lexicographic upgrade is implemented as an example of how an agent might revise his plausibility ordering in light of new evidence. Various examples are given how this apparatus may be used to model the contextual resolution of context-dependent or semantically incomplete utterances. The described form of abduction is limited and merely serves as a proof of concept, but the idea in general has good potential as one among many ways to build a bridge between semantics and pragmatics since inclusive context-dependence is ubiquitous. (shrink)

In order to fully implement the new development concept, bring into full play the potential of sports development, and maintain the resilience of China’s sports development. This paper studies the resilience evaluation and spatial correlation of Chinese sports development under the new development concept. First, we constructed Resilience Evaluation Indexes System for Sports Development in China based on the analysis of the resilience features of sports development and the DPSIR model, which is from the five aspects of “driving force – (...) pressure – state – influence – response.” Second, used Coefficient of Variation and Technique for Order Preference by Similarity to an Ideal Solution Method to measure the resilience level of sports development in 31 provinces in China from 2013 to 2017. Then, we introduced the obstacle degree model to identify the obstacle factors that hinder the resilience of Chinese sports development in different periods. Finally, we used the global and local Moran indexes to analyze the spatial correlation of China sports regional development. The results showed that: overall, the development level of sports resilience in 31 provinces in China showed an upward trend from 2013 to 2017, while some provinces showed obvious fluctuations. The obstacles to the development of sports resilience in China mainly include sports scientific research equipment, the number of national fitness monitoring stations, the number of national fitness centers, the full-time equivalent of personnel, and the number of sports scientific research projects. The response subsystem is the main obstacle factor that affects the improvement of the resilience level of sports development in China. There is a positive spatial autocorrelation between the resilience level of sports development and regional spatial distribution, and the correlation shows a weakening trend, and the internal difference is significant. Finally, we concluded that we must take the new development philosophy as the guiding principle. First, we should stick to innovation-driven development to fully upgrade the resilience of China’s sports development. Second, we should adhere to the principle of coordinated development to promote the overall and balanced development of sports. Lastly, we should promote shared development so as to deliver benefits for all in an equal way. (shrink)

The present paper covers technological changes in the coal mining process. Coal is the main domestic energy resource in Ukraine. In this context such issues as upgrading of conventional technologies and introduction of innovative developments need early solution. Technology is a driving force of strategic development of enterprises in all industries, including the mining. Technological aspects and their interrelation with competitiveness were explored and substantiated by I. Ansoff, who also identified three possible variability levels of technology: 'stable', 'productive' and 'changeable'. (...) 'Stable' technology is virtually unchangeable throughout the life cycle of demand. It is intrinsic to coal production as coal has been mined for centuries and in spite of changes in mining techniques, the demand for it is high enough. This technology originated approximately in the late 18th century when the first mines appeared in the Donets Basin. 'Productive' technology means the traditional one within which various innovations are introduced. In the early development period of the mining industry only pillar mining was used. Two new directions were subsequently developed: shortwall and longwall mining. Winning mechanization in European countries was achieved through development of longwall machines. The USA preferred shortwall mining of coal seams. The above mining alternatives were examined at Donbas mines, the results compared by such parameters as the number of workers and their labor capacity. The necessity of introduction and further improvement of 'manless' mining flow diagrams was substantiated. Some methods for roadway maintenance without repairs were described. The measures required for roadway maintenance without repairs under different conditions can be divided into a number of groups: ways of roadway protection, use of supports with improved yielding, an increased cross-sectional area and longitudinal section of workings during driving, reinforcement of seam bearing rock, application of mine overhead carriers. 'Changeable' technology comprises such unconventional techniques as underground gasification, hydrogenization and hydraulic coal mining by boreholes as well as ancillary recovery of methane gas. (shrink)

Purpose This study aims to understand the allure and danger of fake news in social media environments and propose a theoretical model of the phenomenon. Design/methodology/approach This qualitative research study used the uses and gratifications theory approach to analyze how and why people used social media during the 2016 US presidential election. Findings The thematic analysis revealed people were gratified after using social media to connect with friends and family and to gather and share information and after using it as (...) a vehicle of expression. Participants found a significant number of fake news stories on social media during the 2016 US presidential election. Participants tried to differentiate between fake news and real news using fact-checking websites and news sources and interacted with the social media users who posted fake news and became part of the echo chamber. Behaviors like these emerged in the analysis that could not be completely explained by UGT and required further exploration which resulted in a model that became the core of this study. Research limitations/implications This is a small-scale exploratory study with eight diverse participants, findings should not be generalized to larger populations. Time-specific self-reporting of information from social media and fake news during the 2016 US presidential election. Upgrading public policies related to social media is recommended in the study, contributing to burgeoning policy discussions and provides recommendations for both purveyors of social media and public policymakers. Practical implications Upgrade in public policies related to social media is recommended in the study and contributes to burgeoning policy discussions and provides recommendations for both purveyors of social media and public policymakers. Social implications Social media users are spending increased time on their preferred platforms. This study increases the understanding of the nature, function and transformation of virtual social media environments and their effects on real individuals, cultures and societies.What is original/of value about the paper?This exploratory study establishes the foundation on which to expand research in the area of social media use and fake news. Originality/value This exploratory study establishes the foundation to expand research in the area of social media use and fake news. (shrink)

Moodle is applied as an online learning management system in the Faculty of Medicine, Thammasat University (TU), where the curriculum has been based on problem-based learning (PBL) since 2015. Little research on the effectiveness of Moodle and students’ attitudes during their studies at the pre-clinical medical level within a PBL curriculum has been conducted. Hence, this cross-sectional study focuses on second- and the third-year (MD-2 and MD-3) preclinical medical students’ attitudes towards Moodle and its effectiveness in the PBL curriculum by (...) using a 27-itemed self-constructed online questionnaire. Additionally, students’ preferences as regards the materials managed by the Moodle platform were also evaluated as students’ preferred behaving style (SPBS). After obtaining ethical approval from the Human Ethics Committee of TU No. 1 (Faculty of Medicine), the data was collected and analyzed by medians and inter-quartile ranges, Mann-Whitney U test, and Spearman correlation (ρ). After analyzing the data, the results indicated the following: (1) the top four attitudes scores, (2) the two lowest-attitude scores, (3) the top five effectiveness scores (Ef), (4) the three lowest effectiveness scores, and (5) the top three SPBS scores. Interestingly, a stronger positive Spearman’s correlation (ρ) between ‘Prefer doing quizzes in Moodle to in classroom’ and ‘Moodle enhances learning capability’ was found for MD-3 compared with MD-2. This study reports that Moodle is preferable as a platform supporting students’ self-learning within a PBL curriculum. However, to use the Moodle platform to the highest benefit, instructors need to upgrade its capabilities, especially in the area of student-teacher interaction and the enhancement of students’ critical thinking and creativity, as demonstrated by the lowest scores obtained in this study. (shrink)

Architectural Drawings as Investigating Devices explores how the changing modes of representation in architecture and urbanism relate to the transformation of how the addressees of architecture and urbanism are conceived. The book diagnoses the dominant epistemological debates in architecture and urbanism during the 20th and 21st centuries. It traces their transformations, paying special attention to Le Corbusier and Ludwig Mies van der Rohe’s preference for perspective representation, to the diagrams of Team 10 architects, to the critiques of functionalism, and (...) the upgrade of the artefactual value of architectural drawings in Aldo Rossi, John Hejduk, Peter Eisenman, and Oswald Mathias Ungers, and, finally, to the reinvention of architectural programme through the event in Bernard Tschumi and the Office for Metropolitan Architecture (OMA). Particular emphasis is placed on the spirit of truth and clarity in modernist architecture, the relationship between the individual and the community in post-war era architecture, the decodification of design process as syntactic analogy and the paradigm of autonomy in the 1970s and 1980s architecture, the concern about the dynamic character of urban conditions and the potentialities hidden in architectural programme in the post-autonomy era. This book is based on extensive archival research in Canada, the USA and Europe, and will be of interest to architects, artists, researchers and students in architecture, architectural history, theory, cultural theory, philosophy and aesthetics. (shrink)

Except in extraordinary circumstances, patients' clinical care should reflect their preferences. Incapacitated patients cannot report their preferences. This is a problem. Extant solutions to the problem are inadequate: surrogates are unreliable, and advance directives are uncommon. In response, some authors have suggested developing algorithmic "patient preference predictors" (PPPs) to inform care for incapacitated patients. In a recent paper, Earp et al. propose a new twist on PPPs. Earp et al. suggest we personalize PPPs using modern machine learning (ML) techniques. (...) In this paper, I argue that, contrary to Earp et al.'s claim, personalized patient preference predictors are neither technically feasible nor ethically desirable. (shrink)

Several areas of welfare economics seek to evaluate states of affairs as a function of interpersonally comparable individual utilities. The aim is to map each state of affairs onto a vector of individual utilities, and then to produce an ordering of these vectors that can be represented by a mathematical function assigning a real number to each. When this approach is used in intertemporal contexts, a central theoretical question concerns the evaluative weight to be applied to utility coming at different (...) times. This question concerns the rate of pure time preference, which is one key determinant of the social discount rate. This article argues that the standard philosophical account of pure time preference is mistaken, because it ascribes to economists a methodological commitment they need not, and often do not, accept. This in turn undercuts the most common philosophical objection to pure time preference, which traces at least to Rawls’s A Theory of Justice. The article then evaluates three further objections to pure time preference, concluding that it might still be defensible under certain circumstances. The article closes by articulating a final argument that is suggested by the “Social, Economic and Ethical Concepts and Methods” chapter of the most recent Intergovernmental Panel on Climate Change report. If this further argument is sound, it would constitute a decisive objection to pure time preference as it currently figures in much intertemporal welfare economics. (shrink)

The standard approach to treatment decision making for incapacitated patients often fails to provide treatment consistent with the patient’s preferences and values and places significant stress on surrogate decision makers. These shortcomings provide compelling reason to search for methods to improve current practice. Shared decision making between surrogates and clinicians has important advantages, but it does not provide a way to determine patients’ treatment preferences. Hence, shared decision making leaves families with the stressful challenge of identifying the patient’s preferred treatment (...) option. To address this concern, the present paper proposes to incorporate the use of a “Patient Preference Predictor” (PPP) into the shared decision-making process between surrogates and clinicians. A PPP would predict which treatment option a given incapacitated patient would most likely prefer, based on the individual’s characteristics and information on what treatment preferences are correlated with these characteristics. Use of a PPP is likely to increase the chances that incapacitated patients are treated consistent with their preferences and values and might reduce the stress and burden on their surrogates. Including a PPP in the shared decision-making process therefore has the potential to realize important ethical goals for making treatment decisions for incapacitated patients. The present paper justifies this approach on conceptual and normative grounds. (shrink)

Hausman and McPherson defend welfare economics by claiming that even if welfare does not consist in preference satisfaction, preferences still provide good, if fallible, evidence of welfare. I argue that this strategy does not yet fully solve the problems for welfare economics stemming from the preference satisfaction theory of welfare. More work is needed to show that our self-interested preferences are sufficiently reliable, or in some other sense our best, evidence of well-being. Thus, my aim is to identify (...) the challenges that remain and clarify what additional work is needed before Hausman and McPherson's defence of welfare economics succeeds. (shrink)

It is well-established that the experience of nature produces an array of positive benefits to mental well-being. Much less is known about the specific attributes of green space which produce these effects. In the absence of translational research that links theory with application, it is challenging to design urban green space for its greatest restorative potential. This translational research provides a method for identifying which specific physical attributes of an environmental setting are most likely to influence preference and restoration (...) responses. Attribute identification was based on a triangulation process invoking environmental psychology and aesthetics theories, principles of design founded in mathematics and aesthetics, and empirical research on the role of specific physical attributes of the environment in preference or restoration responses. From this integration emerged a list of physical attributes defining aspects of spatial structure and environmental content found to be most relevant to the perceptions involved with preference and restoration. The physical attribute list offers a starting point for deciphering which scene stimuli dominate or collaborate in preference and restoration responses. To support this, functional definitions and metrics—efficient methods for attribute quantification are presented. Use of these research products and the process for defining place-based metrics can provide (a) greater control in the selection and interpretation of the scenes/images used in tests of preference and restoration and (b) an expanded evidence base for well-being designers of the built environment. (shrink)

While very much in Sen's camp in rejecting revealed preference theory and emphasizing the complexity, incompleteness, and context dependence of preference and the intellectual costs of supposing that all the factors influencing choice can be captured by a single notion of preference, this essay contests his view that economists should recognize multiple notions of preference. It argues that Sen's concerns are better served by embracing a single conception of preference and insisting on the need for (...) analysis of the multiple factors that determine ‘preference’ so conceived. (shrink)

Mark Johnson’s work The Meaning of the Body presents John Dewey’s pragmatism and pragmatist aesthetics as the forerunners of the anti-Cartesian embodied enactive approach to human experience and meaning. He rejects the Kantian noncognitive character of aesthetics and emphasizes that aesthetics is the study of the human capacity to experience the bodily conditions of meaning constitution that grows from our bodily conditions of life. Using Mark Johnson’s view as a starting-point, this paper offers the beginning of an enactive approach to (...) aesthetic preference contributing to bringing human aesthetic behavior research closer to the enactive approach to human experience. Following enactive studies on bodily sense-making and embodied emotions, I identify the bodily conditions of meaning constitution in which aesthetic preference is grounded with the subject’s self-regulatory visceral embodied constitution of viable degrees of value of the environmental factors according to her bodily structure. Unlike mainstream aesthetic preference research in empirical aesthetics, I claim that the subject’s aesthetic preference constitution requires the lived experience of the bodily conditions of meaning constitution through the conscious experience of the subjectively aroused lived body. The implausibility of the mind/body dichotomy of current aesthetic preference research is highlighted. (shrink)

According to standard rational choice theory, as commonly used in political science and economics, an agent's fundamental preferences are exogenously fixed, and any preference change over decision options is due to Bayesian information learning. Although elegant and parsimonious, such a model fails to account for preference change driven by experiences or psychological changes distinct from information learning. We develop a model of non-informational preference change. Alternatives are modelled as points in some multidimensional space, only some of whose (...) dimensions play a role in shaping the agentís preferences. Any change in these "motivationally salient" dimensions can change the agent's preferences. How it does so is described by a new representation theorem. Our model not only captures a wide range of frequently observed phenomena, but also generalizes some standard representations of preferences in political science and economics. (shrink)

Scholars disagree about the plausibility of preference purification. Some see it as a familiar phenomenon. Others denounce it as conceptually incoherent, postulating that it relies on the psychologically implausible assumption of an inner rational agent. I argue that different notions of rationality can be leveraged to advance the debate: procedural rationality and structural rationality. I explicate how structural rationality, in contrast to procedural rationality, allows us to offer an account of the guiding idea behind preference purification that avoids (...) inner rational agents. Afterward, I address two pressing challenges against preference purification that emerge under the structural rationality account. (shrink)

Time preference reversals refers to systematic inconsistencies between preferences and valuations in intertemporal choice. When faced with a pair of intertemporal options, people preferred the smaller-sooner option but assign a higher price to the larger-later one. Different hypotheses postulate that the differences in evaluation scale or output format between the choice and the bid tasks cause the preference reversal. However, these hypotheses have not been distinguished. In the present study, we conducted a hybrid task, which shares the same (...) evaluation scale with the bid task and shares the same output format with the choice task. By comparing these three tasks, we can figure out the key reason for time preference reversal. The eye-tracking measures reflecting attention allocation, cognitive effort and information search pattern were examined. Results showed that participants' time preference and eye-tracking measures in the hybrid task were similar to those in the choice task, but different from those in the bid task. Our findings suggest that the output format is the core reason for time preference reversal and may deepen our understanding of the mechanisms that underlie time preference reversal. (shrink)

We compare two different elicitation methods for measuring risk attitudes on a sample of French farmers. We consider the lottery tasks initially proposed by Holt and Laury (Econ Rev 92:1644–1655, 2002) and by Eckel and Grossman (Evol Hum Behav 23:281–295, 2002; J Econ Behav Org 68:1–7, 2008). The main empirical result from this within-subject study is that risk preference measures are affected by the type of mechanism used. We first show that this risk preference instability can be related (...) to non-expected utility preferences of farmers. Using a risk-taking psychometric questionnaire, we then demonstrate that risk preferences of farmers are context-dependent. This may be another explanation of the observed risk preference instability. (shrink)

Preference is a key area where analytic philosophy meets philosophical logic. I start with two related issues: reasons for preference, and changes in preference, first mentioned in von Wright’s book The Logic of Preference but not thoroughly explored there. I show how these two issues can be handled together in one dynamic logical framework, working with structured two-level models, and I investigate the resulting dynamics of reason-based preference in some detail. Next, I study the foundational (...) issue of entanglement between preference and beliefs, and relate the resulting richer logics to belief revision theory and decision theory. (shrink)

Obligation describing language is hooked up with preference, a relation of what-is-better-than-what. But ordinary situations underdetermine such relations of what-is-better-than-what. Even so, there are plainly true sentences describing our obligations in those situations. This mismatch is trouble-making and getting out of the trouble requires either giving up the easy link between “ought” and preference or re-thinking the kind of things preferences can be.

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)