Film and the Emotions explores the complicated relationship between filmed entertainment, such as movies and television shows, and our capacity to feel emotions. This volume of The Midwest Studies in Philosophy covers topics such as the role of imagination in our capacity to respond emotionally to films, how emotions felt in response to films relate to emotions felt about real events, and the moral implications of responding emotionally to fictions, among others. This collection includes nineteen original articles from experts on (...) film and emotion, including Noel Carroll, Gregory Currie, Susan Feagin, Stacie Friend, Robert Hopkins, Peter Lamarque and Peter Goldie, Derek Matravers, Carl Plantinga, and Murray Smith. (shrink)

In order to allow the use of axioms in a second‐order system of extracting programs from proofs, we define constant terms, a form of Curry‐Howard terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended Curry‐Howard terms are strongly normalizable.

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization (...) corresponds to term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.

In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to (...) Girard's proof using proof-nets. (shrink)

This paper introduces a natural deduction calculus for intuitionistic logic of belief \ which is easily turned into a modal \-calculus giving a computational semantics for deductions in \. By using that interpretation, it is also proved that \ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in \ showing the general structure of such a modality for belief in an intuitionistic framework.

Proofs from assumptions are amongst the most fundamental reasoning techniques. Yet the precise nature of assumptions is still an open topic. One of the most prominent conceptions is the placeholder view of assumptions generally associated with natural deduction for intuitionistic propositional logic. It views assumptions essentially as holes in proofs, either to be filled with closed proofs of the corresponding propositions via substitution or withdrawn as a side effect of some rule, thus in effect making them an auxiliary notion subservient (...) to proper propositions. The Curry–Howard correspondence is typically viewed as a formal counterpart of this conception. I will argue against this position and show that even though the Curry–Howard correspondence typically accommodates the placeholder view of assumptions, it is rather a matter of choice, not a necessity, and that another more assumption-friendly view can be adopted. (shrink)

Mathematics is about proofs, that is the derivation of correct statements; and calculations, that is the production of results according to well-defined sets of rules. The two notions are intimately related. Proofs can involve calculations, and the algorithm underlying a calculation should be proved correct. The aim of the author is to explore this relationship. The book itself forms an introduction to simple type theory. Starting from the familiar propositional calculus the author develops the central idea of an applied lambda-calculus. (...) This is illustrated by an account of Gödel's T, a system which codifies number-theoretic function hierarchies. Each of the book's 52 sections ends with a set of exercises, some 200 in total. These are designed to help the reader get to grips with the subject, and develop a further understanding. An appendix contains complete solutions of these exercises. (shrink)

The reduction of the lambda calculus to the theory of combinators in [Sch¨ onfinkel, 1924] applies to positive implicational logic, i.e. to the typed lambda calculus, where the types are built up from atomic types by means of the operation A −→ B, to show that the lambda operator can be eliminated in favor of combinators K and S of each type A −→ (B −→ A) and (A −→ (B −→ C)) −→ ((A −→ B) −→ (A −→ C)), (...) respectively.1 I will extend that result to the case in which the types are built up by means of the general function type ∀x : A.B(x) as well as the disjoint union type ∃x : A.B(x)– essentially to the theory of [Howard, 1980]. To extend the treatment of −→ to ∀ we shall need a generalized form of the combinators K and S, and to deal with ∃ we will need to introduce a new form of the combinator S.. (shrink)

This book is collection of published and unpublished essays on the philosophy of religion by Howard Wettstein, who is a widely respected analytic philosopher. Over the past twenty years, Wettstein has attempted to reconcile his faith with his philosophy, and he brings his personal investment in this mission to the essays collected here. Influenced by the work of George Santayana, Wittgenstein, and A.J. Heschel, Wettstein grapples with central issues in the philosophy of religion such as the relationship of religious (...) practice to religious belief, what is at stake in the debate between atheists and theists, and the place of doctrine in religion. His discussions draw from Jewish texts as well as Christianity, Islam, and classical philosophy. The challenge Wettstein undertakes throughout the volume is to maintain a philosophical naturalism while pursuing an encounter with God and traditional religion. In the Introduction to this volume, Wettstein elucidates the uniting themes among the collected essays. (shrink)

An exploration of Immanuel Kant's account of war and the controversies that have arisen from its interpretation. This book brings the ideas of Kant's critical philosophy to bear on one of the leading political and legal questions of our age: under what circumstances, if any, is recourse to war legally and morally justifiable?

This book shows how the traditional concerns of political theory push it increasingly into the study of international relations. This is done, first, by demonstrating how many of the issues usually dealt with by political theory, such as democracy and justice, arise within an increasingly global context and, secondly, by considering how international issues, such as colonialism and war, are best illuminated by building on the work of political theorists. The book suggests that political theory and international relations theory can (...) now both be successfully engaged in as a joint enterprise only. (shrink)

The book is a comparative analysis of all the major social science/political science grand theories. It focuses on developmentalism, dependency theory, the world systems approach, Marxism, institutionalism, rational choice, psychoanalysis, political sociology, sociobiology, environmentalism, neuro-politics, transitions to democracy, and non-Western systems of analysis. To facilitate comparison and analysis, a common framework and outline are employed throughout. An integrating introduction and conclusion help tie the book together.

Studie over het werk van de Duitse wijsgeer Friedrich Ludwig Gottlob Frege (1848-1925).

What is intellectual humility? In this essay, we aim to answer this question by assessing several contemporary accounts of intellectual humility, developing our own account, offering two reasons for our account, and meeting two objections and solving one puzzle.

The loss of the federally protected constitutional right to an abortion is a threat to the already tenuous autonomy of pregnant people, and may augur future challenges to their right to refuse unwanted obstetric interventions. Even before Roe’s demise, pregnancy led to constraints on autonomy evidenced by clinician-led legal incursions against patients who refused obstetric interventions. In Dobbs v. Jackson Women’s Health Organization, the Supreme Court found that the right to liberty espoused in the Constitution does not extend to a (...) pregnant person’s right to an abortion. With Roe’s demise, the right to request specific types of care has been vitiated. The same argument underpinning that holding may now become ballast for attacks on the traditionally more robust right, the right to refuse. Here we discuss how the elevation of fetal and embryonic rights may lead to a cascade of medical intrusions and deprivations of liberty against pregnant persons, and offer an argument opposing these improprieties. (shrink)

I shall argue that cinematic images do not have tense: not, at least, in the sense that has been ascribed to them by film theorists. This does not abolish time in cinema, for there can be temporal relations without tense, and temporal relations between cinematic images can indicate temporal relations between events depicted. But the dispensability of tense will require us to rethink our assumptions about what is sometimes called anachrony in cinema: the reordering of story-time by narrative, of which (...) the flashback is the most common example. (shrink)

The first full-scale history of cognitive science, this work addresses a central issue: What is the nature of knowledge?

There is considerable evidence that the hippocampal system contributes both to (1) the temporary maintenance of memories and to (2) the processing of a particular type of memory representation. The findings on amnesia suggest that these two distinguishing features of hippocampal memory processing are orthogonal. Together with anatomical and physiological data, the neuropsychological findings support a model of cortico-hippocampal interactions in which the temporal and representational properties of hippocampal memory processing are mediated separately. We propose that neocortical association areas maintain (...) shortterm memories for specific items and events prior to hippocampal processing as well as providing the final repositories of long-term memory. The parahippocampal region supports intermediate-term storage of individual items, and the hippocampal formation itself mediates an organization of memories according to relevant relationships among items. Hippocampal-cortical interactions produce (i) strong and persistent memories for events, including their constituent elements and the relationships among them, and (ii) a capacity to express memories flexibly across a wide range of circumstances. (shrink)

Oxford Scholarly Classics is a new series that makes available again great academic works from the archives of Oxford University Press. Reissued in uniform series design, the reissues will enable libraries, scholars, and students to gain fresh access to some of the finest scholarship of the last century.

... THIRD WORLD EPISTEMOLOGY L. Jonathan Cohen . Sir Karl Popper's striking hypothesis about a third world of objective knowledge deserves careful scrutiny ...

In challenging the prevailing paradigm for understanding how the human mind works, Patterns, Thinking, and Cognition is certain to stimulate fruitful debate.

Howard J. Curzer presents a fresh new reading of Aristotle's Nicomachean Ethics, which brings each of the virtues alive. He argues that justice and friendship are symbiotic in Aristotle's view; reveals how virtue ethics is not only about being good, but about becoming good; and describes Aristotle's ultimate quest to determine happiness.