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)

This volume gathers together for the first time are all the key texts in a crucial debate in modern philosophy, centered on Leibniz's famous 1695 essay, the "New System of the Nature of Substances and their Communication," in which he introduced his strikingly original theory of metaphysics. His "system" became increasingly famous and drew him into discussion and development of these ideas, both in public and in private, with a variety of thinkers, most notably the great French philosopher Pierre Bayle. (...) Woolhouse's and Francks's new English edition gives the only full representation of this debate, and will therefore be essential reading for anyone who wishes to gain a proper understanding of Leibniz's philosophy and its intelletual context. All the texts are newly translated and extensively annotated; many appear in English for the first time. (shrink)

Seminar papers on Dvaitadvaita philosophy with reference to Advaitabrahmasiddhi of Madhusūdana Sarasvatī and Nyāyāmr̥ta of Vyāsatīrtha, 1460-1539.

-- v. 2. Pami︠a︡ti Vitalii︠a︡ Ivanovicha Svint︠s︡ova.

This chapter offers a proceduralist argument against capital punishment. More specifically, it contends that the possibility of irrevocable mistakes precludes the just administration of the death penalty. At stake is a principle of political morality: legal institutions must strive to remedy their mistakes and to compensate those who suffer from wrongful sanctions. The incompatibility of remedy and execution is the crux of the irrevocability argument: because the wrongly executed cannot enjoy the morally required compensation, execution is impermissible. Along with defending (...) his key premises, Yost explains the complicated role that sentencing uncertainty plays in the argument. He concludes by noting some of the flaws in substantive consequentialist and retributivist justifications of capital punishment. (shrink)

Purpose. The research is aimed at substantiation of the process of formation of various human images in the postmodernism era in the context of biophilosophy, taking into account the need to find an adequate response to historical challenges and the production of new value orientations reflecting succession of civilization development. Theoretical basis. The author in his theoretical constructs proceeds from the need of taking into account the biophilosophical aspect of postmodern man, as the one who, remaining a representative of the (...) species Homo sapiens, began to dynamically change, losing its own natural and functional qualities, acquiring to a large extent the socio-technology-related qualities. The thesis that in the postmodern society the moral and legal foundations of existence of human being, as the subject of actions and responsibility for these actions, practically coincide with the biological foundations is taken as initial argument. New biological knowledge, as well as the related technologies, orient the public consciousness towards production of fundamentally new or modernization of the existing bio-philosophical ideas. The author's vision of the anthropological collision of the Post-Modernism era is caused by the fact that the issues of a postmodern man acquire a special urgency at the end of the ХХ – early XXI century. A progressive disproportion between a human being, whose abilities as a representative of the species Homo sapiens are biologically limited, and the human community, which sees no limits in its information and technological expansion, is of current interest. Originality. The author reveals the key features of the Post-Modernism era, in which a fundamentally different civilizational space originates, and where a new type of person emerges in its internal culture, which is called the postmodern man. The postmodern man was considered through the prism of bio-philosophy. Its interest in man is caused by his or her place in nature, the prospects of development at the individual, population and species levels. Conclusions. In the process of development of bio-philosophy, its research field will be naturally expanded with the use of philosophical means of perception of life as such and filling the bio-philosophy with philosophical and biological issues. In contemporary conditions, the study of the boundaries of biological reality and its previously unknown properties, definition of new horizons of theoretical knowledge in the science of life, the critical rethinking of the concepts of biocentrism and anthropocentrism in the space of modern scientific knowledge, the definition of perspective trends in the study of man, his or her place and role in the planetary being is of great importance. (shrink)

In Seeing Things as They Are (Searle 2015), Searle developed a direct realist’s theory of perception. According to direct realism, physical objects are directly and immediately perceived. Searle claims that Berkeley’s theory of perception goes against direct realism. For Searle, Berkeley’s theory suggests that only subjective experiences (ideas) are directly and immediately perceived, not physical objects. Contrary to Searle, G. S. Pappas claims that Berkeley’s theory of perception is consistent with the view that physical objects are immediately perceivable (Pappas 1982; (...) Pappas 1987). Given the conflicting interpretations of Berkeley’s theory of perception, this paper attempts to defend Searle’s position on Berkeley’s theory of perception. It refutes Pappas’ interpretation by arguing that he is inconsistent with Berkeley’s theses of ontological phenomenalism and heterogeneity thesis. (shrink)

Plato's dialogues frequently criticize traditional Greek myth, yet Plato also integrates myth with his writing. Daniel S. Werner confronts this paradox through an in-depth analysis of the Phaedrus, Plato's most mythical dialogue. Werner argues that the myths of the Phaedrus serve several complex functions: they bring nonphilosophers into the philosophical life; they offer a starting point for philosophical inquiry; they unify the dialogue as a literary and dramatic whole; they draw attention to the limits of language and the limits of (...) knowledge; and they allow Plato to co-opt cultural authority as a way of defining and legitimating the practice of philosophy. Platonic myth, as a species of traditional tale, is thus both distinct from philosophical dialectic and similar to it. Ultimately, the most powerful effect of Platonic myth is the way in which it leads readers to participate in Plato's dialogues and to engage in a process of self-examination. (shrink)

Prologue, invitation to thinking about God In the Hebrew Bible? -- Part I, questions about God? -- Why does God in the Bible have a body? -- What do God's body parts in the Bible mean? -- Why is God angry in the Bible? -- Does God in the Bible have gender or sexuality? -- Part II, questions about God in the world? -- What can creation tell us about God? -- Who-or what-is the Satan? -- Why do people suffer (...) according to the Hebrew Bible? -- Epilogue, God in the Bible and beyond. (shrink)

This chapter is devoted to discussions about the nature of experiments in mathematics during the formative period of experimental mathematics and to a quantitative and qualitative analysis of the journal Experimental Mathematics founded in 1992. Particular attention is paid to interpret the roles of experiment and observation in the mathematical practices surrounding Experimental Mathematics.

In 2018, the Chinese scientist He Jiankui presented his research at the Second International Summit on Human Genome Editing in Hong Kong. While it was intended that he facilitate a workshop, he was instead called on to present his research in heritable human genome editing, where he made the announcement that he had taken great strides in advancement of his research, to the extent that he had gene-edited human embryos and that this had resulted in the live births of two (...) children. While his research ethic and methodology was interrogated, he insisted that two children, twin girls, had been born healthy and that there was another pregnancy (at the time) where birth of a third gene edited child would be imminent. This announcement generated a ripple effect in the scientific community and exposed the gaps in regulation and absence of law relating to the technology. This resulted in a flurry of activity and conversation around regulation of the technology, which scientists stated was not ready for human trials. This article reviews the Third Summit which was held in London in March 2023 and comments on the latest developments in the regulation of heritable human genome editing. (shrink)

Study of Pañcadaśi of Mādhava, d. 1386, compendium on Advaita philosophy.