Dag Prawitz (1971) put forward the idea that an admissible reduction process does not affect the identity of proofs represented by derivations in natural deduction. The idea relies on his conjecture that two derivations represent the same proof if and only if they are equivalent in the sense that they are reflexive, transitive and symmetric closure of the immediate reducibility relation. Schroeder-Heister and Tranchini (2017) accept Prawitz’s conjecture and propose the triviality test as the criterion for admissible reductions. (...) In the present paper, we will consider two main troubles of the triviality test. The first is the obscurity of a method of evaluating admissible reductions. The second is the circularity problem that the triviality test already assumes the set of admissible reduction procedures. For the solution of the problems, we will propose the spoiler test which immunes the problems of the triviality test and has the role of the criterion for admissible reductions. At last, we shall cover a plausible problem of the spoiler test that can be caused by Crabbé’s case. (shrink)

We propose a novel, ontological approach to studying mathematical propositions and proofs. By “ontological approach” we refer to the study of the categories of beings or concepts that, in their practice, mathematicians isolate as fruitful for the advancement of their scientific activity (like discovering and proving theorems, formulating conjectures, and providing explanations). We do so by developing what we call a “formal ontology” of proofs using semantic modeling tools (like RDF and OWL) developed by the computer science community. (...) In this article, (i) we describe this new approach and, (ii) to provide an example, we apply it to the problem of the identity of proofs. We also describe open issues and further applications of this approach (for example, the study of purity of methods). We lay some foundations to investigate rigorously and at large scale intellectual moves and attitudes that underpin the advancement of mathematics through cognitive means (carving out investigationally valuable concepts and techniques) and social means (like communication, collaboration, revision, and criticism of specific categories, inferential patterns, and levels of analysis). Our approach complements other types of analysis of proofs such as reconstruction in a deductive system and examination through a proof-assistant. (shrink)

Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal form in natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the (...) same generality if after generalizing maximally the rules involved in them they yield the same premises and conclusions up to a renaming of variables. These two proposals proved to be extensionally equivalent only for limited fragments of logic. The normalization proposal stands behind very successful applications of the typed lambda calculus and of category theory in the proof theory of intuitionistic logic. In classical logic, however, it did not fare well. The generality proposal was rather neglected in logic, though related matters were much studied in pure category theory in connection with coherence problems, and there are also links to low-dimensional topology and linear algebra. This proposal seems more promising than the other one for the general proof theory of classical logic. (shrink)

In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system (...) of Wansing's bi-intuitionistic logic 2Int, which I will turn into a term-annotated form. Therefore, we need a type theory that extends to a two-sorted typed lambda-calculus. I will present such a term-annotated proof system for 2Int and prove a Dualization Theorem relating proofs and refutations in this system. On the basis of these formal results I will argue that this gives us interesting insights into questions about sense and denotation as well as synonymy and identity of proofs from a bilateralist point of view. (shrink)

This article is a methodological discussion of formal approaches to the question of identity of proofs from a philosophical standpoint. First, an introduction to the question of identity of proofs itself is given, followed by a brief reconstruction of the so-called normalisation thesis, proposed by Dag Prawitz in 1971, in which some of its core mathematical and conceptual traits are presented. After that, a comparison between the normalisation thesis and the more well-known Church-Turing thesis on computability (...) is carried out in three main parts: the first dedicated to highlighting some of the analogies between them; the second, their most remarkable differences; and the third, to the possible relations of dependence between the two. Based on these considerations, some concluding remarks concerning the potential of the normalisation thesis and similar approaches to the question of identity of proofs are made in the last section. (shrink)

In considering the possibility that the fundamental particles of matter might violate Leibniz's Principle, one is confronted with logical proofs that the Principle is a Theorem of Logic. This paper shows that the proof of that theorem is not universal enough to encompass entities that might not be unique, and also strongly suggests that photons, for example, do violate Leibniz's Principle. It also shows that the existence of non-individuals would imply the breakdown of Quine's criterion of ontological commitment.

The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes second-order logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can (...) be justified in a proof-theoretical manner. (shrink)

The aim of this chapter is to explore to some extent the relationship between identity and necessity in logic and metaphysics. First, I provide a historically-based summary of proofs of the necessity of identity, highlighting the importance of the role that self-identity plays. Second, I introduce two examples of metaphysical topics where the necessity of identity has played a pivotal role: the necessary a posteriori, and the coincidence of material objects. I argue that important aspects (...) of these debates rest on how we represent identity. Third, I consider some recent work on generalized identity. This opens up new prospects for explaining why identity is necessary. (shrink)

We study natural deduction systems for a fragment of intuitionistic logic with propositional identity from the point of view of proof-theoretic semantics. We argue that the identity connective is a natural operator to be treated under the elimination rules as basic approach.

This paper draws attention to a proof of the necessity of identity given by Arthur Prior. In its simplicity, it is comparable to a proof of Quine's, popularised by Kripke, but it is slightly different. Prior's Polish notation is transcribed into a more familiar idiom. Prior's proof is followed by a proof of the necessity of difference, possibly the first such proof in the literature, which is also repeated here and transcribed. The paper concludes with a brief discussion of (...) Prior's views on identity and difference over time. (shrink)

The generality of a derivation is an equivalence relation on the set of occurrences of variables in its premises and conclusion such that two occurrences of the same variable are in this relation if and only if they must remain occurrences of the same variable in every generalization of the derivation. The variables in question are propositional or of another type. A generalization of the derivation consists in diversifying variables without changing the rules of inference. This paper examines in the (...) setting of categorial proof theory the conjecture that two derivations with the same premises and conclusions stand for the same proof if and only if they have the same generality. For that purpose generality is defined within a category whose arrows are equivalence relations on finite ordinals, where composition is rather complicated. Several examples are given of deductive systems of derivations covering fragments of logic, with the associated map into the category of equivalence relations of generality. This category is isomorphically represented in the category whose arrows are binary relations between finite ordinals, where composition is the usual simple composition of relations. This representation is related to a classical representation result of Richard Brauer. (shrink)

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus \(\mathtt{SC2Int}\) for the bi-intuitionistic logic \(\mathtt{2Int}\). A distinctive feature of \(\mathtt{SC2Int}\) is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of \(\mathtt{SC2Int}\), in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, (...) mediated through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of \(\mathtt{2Int}\). By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in \(\mathtt{SC2Int}\) is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. (shrink)

Normal 0 false false false MicrosoftInternetExplorer4 /* Style Definitions */ table.MsoNormalTable {mso-style-name:"Table Normal"; mso-tstyle-rowband-size:0; mso-tstyle-colband-size:0; mso-style-noshow:yes; mso-style-parent:""; mso-padding-alt:0in 5.4pt 0in 5.4pt; mso-para-margin:0in; mso-para-margin-bottom:.0001pt; mso-pagination:widow-orphan; font-size:10.0pt; font-family:"Times New Roman"; mso-ansi-language:#0400; mso-fareast-language:#0400; mso-bidi-language:#0400;} Focusing mainly on a number of unpublished texts by Collingwood, especially his “Lectures on the Ontological Proof of the Existence of God,” the study examines the English philosopher’s innovative interpretation of the Anselm’s main contribution to the philosophical-theological tradition. Collingwood insightfully shows how the ontological argument can be used in (...) analyzing and discussing the religious experience, not in trying to formulate a logical proof of God’s existence. When abstracted from the individual’s practical religious life, that is, from the experience of prayer, worship, and the like, mind’s awareness of God cannot be understood. Resorting mainly to Anselm, Augustine, Thomas Aquinas, and Descartes, Collingwood argues that the externality of the Platonic absolute is that of an absolute transcendent whereas the Christian God is not only conceived as the transcendent cause of all things, but also as the immanent spirit in them. By asserting the unity of the mind—regarded as identical with its acts—this interpretation is meant to serve both as a means towards self-knowledge, and as a starting point for a future conceptual unification of religion and philosophy. (shrink)

We give a simple proof of the canonicity of Sahlqvist identities, using methods that were introduced in a paper by Jónsson and Tarski in 1951.

Since the beginning of human history, there has been no society that did not have any religion. Man meets his need to believe, encoded in his nature by turning to God. God has not left humans alone in their journey on earth, and from time to time, He has intervened in the world through his prophets. The prophethood, which constitutes one of the main subjects of theology, is an important institution in God-human communication. The messengers chosen by God convey to (...) people the information that they received through revelation and offer teachings that will bring them to salvation. The idea of salvation by God when suffering or feeling helpless has driven people to the expectation of a savior. Nearly all religions except Shintoism have the awaited savior belief in the world. Accordingly, the savior will emerge in an environment of chaos where disasters are experienced, and a moral collapse is observed. The expected savior will drive people away from this turmoil, bring them happiness, well-being, and lead them to salvation. Although there is a savior belief in Judaism and Christianity, Muslims claim that the awaited savior in these religions is Muhammad. Muslim thinkers who believe that Muhammad was heralded in previous scripts, tried to find evidence on the subject from the Bible. One of the Islamic scholars who did researches for this purpose is Shamsuddin al-Samarqandi. Shamsuddin Mohammed b. Ashraf al-Husayni al-Samarqandi is an important Turkish-Islamic scholar who lived in Turkestan at the end of the 7th century and the first quarter of the 8th century. Samarqandi is a versatile scholar who produced important works in various fields such as philosophy, logic, mathematics, discussion, debate and astronomy. Shamsuddin al-Samarqandi is one of the eminent scholars who have written his name in the history of science and philosophy with his works. He adopted a critical and analytical style in almost every field, putting the science of logic at the center of his system. His constructive criticisms had an important function in understanding and interpreting the ideas of numerous thinkers, from Greek philosophers to Islamic philosophers and representatives of philosophical theology. In addition to all these, Samarqandi did not hesitate to criticize the Christian and Jewish belief systems, religions such as Sanawiyyah and Zoroastrianism, and the teachings of the naturalist philosophers regarding the relationship between God and the world in the light of rational and scriptural evidence. Samarqandi, who distinguished himself in rational sciences, also showed himself with his background in theology. Due to his exceptional intellectual interest, he analyzes some key concepts and divine codes related to the Bible, making original inferences about the loyalty of Muhammad, the prophet of Islam. Samarqandi interprets some passages of the Torah and the New Testament, which he considers as signs of Muhammad's prophethood, in the axis of language, logic and the rules of shariah, and concludes that Muhammad is the last prophet to be announced. The conceptual framework that he mostly focuses on in this regard contains Mount Paran, Paraklite, comparison with Moses, and the good news given to the Ishmaelites. Samarqandi makes inferences about the environment in which Muhammad appeared, his qualities, and his lineage, based on the aforementioned concepts. Samarqandi also responds to the criticisms raised by the Ahl al-Kitab about the principles, such as the abolition of other religious rules constituting the basis of Muhammad's legitimacy and establishment of Islam instead, and him being a universal prophet. An important privilege of Samarqandi is that he not only grounds his claims on a theoretical scale but also engages in debates with the leaders of the Ahl al-Kitab. Although Samarqandi exhibits a satisfactory analytical attitude in most of his claims, he displays a sophisticated approach based on the method of coercion (ilzām) in some of his claims. Although he adheres to the tradition of beshair al-nubuwwah in general, he gives a different perspective and strong reasoning to the same evidence within the tradition with the effect of his identity as a verifier (muhaqqik). (shrink)

Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of NI\ is assumed to consist only (...) of \- and \-equations. On the basis of the categorial interpretation of NI\, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpreting NI\-derivations. We show that the Russell–Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. Finally we sketch how these results could be used to investigate the properties of connectives definable in the framework of higher-level rules. (shrink)

From the point of view of proof-theoretic semantics, we examine the logical background invoked by Neil Tennant's abstractionist realist account of mathematical existence. To prepare the way, we must first look closely at the rule of existential elimination familiar from classical and intuitionist logics and at rules governing identity. We then examine how well free logics meet the harmony and uniqueness constraints familiar from the proof-theoretic semantics project. Tennant assigns a special role to atomic formulas containing singular terms. This, (...) we find, secures harmony and uniqueness but militates against the putative realism. (shrink)

This open access book investigates the role played by identity of proofs in proof-theoretic semantics. It develops a conception of proof-theoretic semantics as primarily concerned with the relationship between proofs (understood as abstract entities) and derivations (the linguistic representations of proofs). It demonstrates that identity of proof is a key both to clarify some —still not wholly understood— notions at the core of proof-theoretic semantics, such as harmony; and to broaden the range of the phenomena (...) which can be analyzed using the tools of this semantic paradigm, so as to include for instance paradoxes. The volume covers topics such as the philosophical significance of different criteria of identity of proofs, and adequacy conditions for an intensional account of the notion of harmony. The author also examines the Prawitz-Tennant analysis of paradoxes by investigating on the one hand the prospects of turning it into a theory of meaning for paradoxical languages, and on the other hand two distinct kinds of phenomena, first observed by Crabbe and Ekman, showing that the Tennant-Prawitz criterion for paradoxicality overgenerates. This volume is of interest to scholars in formal and philosophical logic. (shrink)

Can unattended objects by seen? Ned Block has claimed they can on the basis of “identity-crowding.” This paper summarizes the ensuing debate with particular emphasis on the role of unconscious perception. Although unconscious perception plays an important role, it cannot support conscious object-seeing in identity-crowding. Nevertheless, unconscious perception assists in making successful judgments about unseen objects. Further, compelling conceptual evidence against seeing unattended objects places the burden of proof on Block. I argue that countability is necessary for seeing (...) objects and sufficient for attention to them; thus, no unattended objects are seen. (shrink)

In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the (...) results are strengthened to height-preserving statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained. (shrink)

Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is (...) shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed. (shrink)

I conclude that it is more accurate to say that, rather than trying to make logic metaphysical, Leibniz tries, in the context of a theistic system, to make metaphysics logical. ;I begin with a study of the principle of identity of indiscernibles, and show how it is best thought of as a principle which follows from a metaphysical interpretation of the principle of sufficient reason. It has been traditional to interpret the principle of identity of indiscernibles as primarily (...) a merely logical principle, and thus as either trivially true, if Leibniz succeeds in proving it, or else false or contingently true. I argue that it is instead necessarily true in a non-trivial or metaphysical sense, because the principles on which it is based are themselves of this metaphysical character, contrary to what is often assumed. ;In the second chapter, I show how God's activity and a metaphysical interpretation of the principle of sufficient reason underlie Leibniz's account of space and time. ;In the third chapter, I discuss the principle of sufficient reason in detail, showing that it actually consists of three separate principles: the principle of grounds, that every true proposition has a proof a priori; the principle of reason, that God does nothing without a sufficient reason; and the principle of causation, that every event has a cause. That each of these is considered a principle of sufficient reason is explained by Leibniz's equivocal use of the term 'reason.' I show that, of the various versions of the principle of sufficient reason, only the principle of reasons provides an adequate foundation for Leibniz's principle of identity of indiscernibles and theory of space and time. Furthermore, since chapters one and two show how the activity of God is presupposed by Leibniz's metaphysics, for Leibniz to derive his metaphysics from his logic, as some would have us suppose, he would have to provide a satisfactory a priori demonstration of God's existence. But this, I argue, he cannot do. Thus God's existence and rationality, rather than subject-predicate logic, are the foundations of Leibniz's metaphysics. ;It is commonplace, when writing about Leibniz, to give primacy to his logic over his metaphysics, and indeed to try to assimilate the latter to the former. In this essay, however, I give priority to Leibniz's metaphysical pronouncements, apart, as much as possible, from logical and linguistic considerations. (shrink)

Published in 1903, this book was the first comprehensive treatise on the logical foundations of mathematics written in English. It sets forth, as far as possible without mathematical and logical symbolism, the grounds in favour of the view that mathematics and logic are identical. It proposes simply that what is commonly called mathematics are merely later deductions from logical premises. It provided the thesis for which _Principia Mathematica_ provided the detailed proof, and introduced the work of Frege to a wider (...) audience. In addition to the new introduction by John Slater, this edition contains Russell's introduction to the 1937 edition in which he defends his position against his formalist and intuitionist critics. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Feminist Studies 41, no. 3. © 2015 by Feminist Studies, Inc. 623 Jaye Cee Whitehead, Kath Bassett, Leia Franchini, and Michael Iacolucci “The Proof Is in the Pudding”: How Mental Health Practitioners View the Power of “Sex Hormones” in the Process of Transition In the United States today, popular discourse touts the power of “sex hormones” and hormone receptors in the brain to chemically produce gender expressions (manifested in (...) physical sex traits, behaviors, and attitudes) and identities (a sense of self as feminine or masculine). These accounts range from common assumptions that Western ideals of femininity (such as empathy understanding, cooperative orientation, nurturing behavior) and masculinity (rational/spatial understanding, competitive orientation, violent behavior) are produced by corresponding sex hormones, to studies that reduce complex gender identities and macrosocial economic phenomena to presocial, binary, hormonal processes.1 For sociologists, accounts that reduce complex identities to internal hormonal reactions are problematic for two primary reasons: first, they are inaccurate because they fail to examine how hormonal reactions are embedded in a complex cultural process of meaning and interpretation; second, they operate as bioreductive ideologies that obscure the social power inherent to the process of gender identity construction. In what follows, we extend both of these insights by examining mental health 1. For an example of a hybrid popular-scientific account of the power of sex hormones to destabilize economic structures, see Jon Coates and Joe Herbert, “Endogenous Steroids and Financial Risk Taking on a London Trading Floor,” Proceedings of the National Academy of Sciences 105, no. 16 (April 2008): 6167–72. 624 Whitehead, Bassett, Franchini, and Iacolucci practitioners’ divergent interpretations of the power of sex hormones in the process of gender transition.2 In doing so, we examine the cultural power of sex hormones in crafting gender identities without reproducing reductionist interpretations of trans embodiment. Perhaps what is most perplexing about the way we speak of sex hormones is that we know it is inaccurate to describe these hormones as sexed; scientists have acknowledged since the 1930s that they are neither sex specific in their function, nor in terms of their location in male or female bodies.3 In her extensive historicization of sex hormones, Anne Fausto-Sterling concludes that it is more accurate to call androgen- and estrogen-based hormones, “steroid hormones” as they have functions that are not confined to corresponding sexed bodies. In fact she urges scientists to “break out of the sex hormone straightjacket” and to look at steroids as just one of a number of components that are important to the creation of sex and gender, including environment and experience.4 Scholars also point to an inextricable link between the chemical operation of hormones and the social process of constructing meaning, both at the level of social interaction and macrocultural constructions of sex categories and gender ideologies.5 While brain organization/activation theory attributes sex and gender differences to hormonal interactions within the developing brain, Fausto-Sterling questions the distinction between activation and organization by pointing out how “the brain can respond to hormonal stimuli with anatomical changes…hormonal systems, after all, respond exquisitely to experience, be it in the form of nutrition, stress, or sexual activity (to name but a few possibilities ).”6 Drawing from Elizabeth Grosz, Fausto-Sterling argues that the power of hormones is best understood according to the model of the 2. “Gender transition” is a controversial phrase, as it implies that transgendered individuals who receive hormone therapy are changing identities. We are only using it for lack of clear alternative phrasing, not because we believe body modifications change gender identities. 3. See Anne Fausto-Sterling, Sexing the Body: Gender Politics and the Construction of Sexuality (New York: Basic Books, 2000); Rebecca Jordan-Young, Brainstorm: The Flaws in the Science of Sex Differences (Cambridge, MA: Harvard University Press, 2010); and Nelly Oudshoorn, Beyond the Natural Body: An Archeology of Sex Hormones (New York: Routledge, 1994). 4. Fausto-Sterling, Sexing the Body, 193–94. 5. Fausto-Sterling, Sexing the Body. 6. Ibid., 232. Whitehead, Bassett, Franchini, and Iacolucci 625 Möbius strip, wherein internal components of the self are always connected to and continuous with outer components such as culture and environment.7 In other... (shrink)

Leibniz propôs que demonstrações fossem reformuladas como deduções a partir de identidades, e que proposições do tipo A = A fossem a fonte única de verdade. Neste artigo, procuro explicar essa teoria da prova (e do conhecimento), assim como seus conceitos elementares, ou seja, os conceitos de identidade, verdade (ou possibilidade) e proposição (inclusive a teoria leibniziana da redutibilidade a proposições sujeito-predicado). Leibniz proposed that demonstrations be reformulated as deductions from identities, and that propositions of the type A = A (...) be the only source of truth. In this article, I aim to explain this theory of proof (and knowledge), as well as its elementary concepts, such as identity, truth (or possibility) and proposition (including Leibniz's theory of reducibility of propositions to subject-predicate form). (shrink)

The essential structure of proofs is proposed as the basis for a measure of complexity of formulas in FOL. The motivating idea was the recognition that distinct theorems can have the same derivation modulo some non essential details. Hence the difficulty in proving them is identical and so their complexity should be the same. We propose a notion of complexity of formulas capturing this property. With this purpose, we introduce the notions of schema calculus, schema derivation and description complexity (...) of a schema formula. Based on these concepts we prove general robustness results that relate the complexity of introducing a logical constructor with the complexity of the component schema formulas as well as the complexity of a schema formula across different schema calculi. (shrink)

In 2004 Atserias, Kolaitis, and Vardi proposed $\text {OBDD}$ -based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of an identically false $\text {OBDD}$ from $\text {OBDD}$ s representing clauses of the initial formula. All $\text {OBDD}$ s in such proofs have the same order of variables. We initiate the study of $\text {OBDD}$ based proof systems that additionally contain a rule that allows changing the order in $\text {OBDD}$ s. At first we consider a (...) proof system $\text {OBDD}$ that uses the conjunction rule and the rule that allows changing the order. We exponentially separate this proof system from $\text {OBDD}$ proof system that uses only the conjunction rule. We prove exponential lower bounds on the size of $\text {OBDD}$ refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for $\text {OBDD}$ proofs and the second one extends the result of Tveretina et al. from $\text {OBDD}$ to $\text {OBDD}$.In 2001 Aguirre and Vardi proposed an approach to the propositional satisfiability problem based on $\text {OBDD}$ s and symbolic quantifier elimination $ algorithms). We augment these algorithms with the operation of reordering of variables and call the new scheme $\text {OBDD}$ algorithms. We notice that there exists an $\text {OBDD}$ algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time, but we show that there are formulas representing systems of linear equations over $\mathbb {F}_2$ that are hard for $\text {OBDD}$ algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over $\mathbb {F}_2$ that correspond to checksum matrices of error correcting codes. (shrink)

What general conclusions can be drawn about the reception of zymase, its relation to the larger shift from a protoplasm to an enzyme theory of life, and its status as a social phenomenon?The most striking and to me unexpected pattern is the close correlation between attitude toward zymase and professional background. The disbelief of the fermentation technologists, Will, Delbrück, Wehmer, and even Stavenhagen, was as sharp and unanimous as the enthusiasm of the immunologists and enzymologists, Duclaux, Roux, Fernback, and Bertrand, (...) and of Pfeffer, the experimental plant physiologist. Other skeptics—Voit, Kupffer, and Fischer—were conservatives in traditional fields. In all these cases it seems clear that professional commitments and outlook profoundly influenced the reception of zymase.In some cases there is a correlation with a specific earlier statement favoring the protoplasm theory or predicting a fermentation enzyme. Reynolds Green is a striking case of both. In 1893 he stated his belief that life processes in higher plants and fungi were identical, both being mediated by protoplasm.109 Thus he claimed that digestion was not carried out by enzymes, as in higher animals, but by the whole protoplasm, and so too fermentation in yeast: “All the metabolic processes must be carried out in the unicellular organism in the same mass of protoplasm.”110 But Green also insisted that there was no essential difference between “organized” and “unorganized ferments”; enzymes were simply more highly differentiated and specialized forms of primitive protoplasm. He spoke of “the alcoholic ferment” (that is, enzyme), and of intracellular enzymes—very advanced beliefs for 1893. Thus it is understandable why Green saw no reason to doubt his first negative results with yeast juice, and rushed into print. But it is also understandable that he persisted and soon became an outspoken advocate of Buchner's view; like Wroblewski and Pfeffer, he had already accepted the idea of an intracellular fermentation enzyme.The physiological chemists also fit the pattern in a special way. Physiological chemistry is generally regarded as the source of biochemistry; indeed, many early biochemists were trained in physiological chemistry, and imbibed there a progressive interest in enzymes and metabolism. It is not surprising, therefore, that on the whole Neumeister, Madfadyen, Wroblewski, and Loew accepted cell-free fermentation. But what is surprising, and significant, is the diversity of opinion in this group, from Abeles' living protoplasm to Wroblewski's organized array of active proteins. The feelings of the physiological chemists were mixed, and there was enough of the old protoplasm view in Macfadyen's and even Wroblewski's views to allow Buchner to see them as attacks on zymase. The ideas of physiological chemistry were also changing; the idea of protoplasm was already adjusting to the new interest in enzymes in the early 1890's. But in contrast to immunochemistry, the change in physiological chemistry was gradual, uneven, undramatic, and relatively invisible. For the new biochemistry, the tradition of physiological chemistry was the source of traditional conservatism as well as of new ideas of enzymes.In general, then, I claim that it was not experimental facts that determined attitudes toward zymase so much as previous commitments, experience, and expectations. Initially, at least, zymase was less a determinant of opinion than a touchstone of pre-existing opinion. Like a prism, it revealed the spectrum of existing attitudes toward vital phenomena.Also relevant here is the fact that the experimental evidence was entirely ambiguous; the interpretation of Buchner's experiments with antiseptics or dried yeast depended entirely on how far one was willing to stretch the scope of the terms “protoplasm” and “enzyme”. Likewise, how important one judged the instability of zymase to be, or the low level of in vitro activity, depended largely on one's point of view. There was no crucial experiment, no certain proof. Logically zymase could be regarded as protoplasm. A. Fischer did so in 1900;111 Macfadyen was still wavering in 1907;112 and Beijerinck was holding out as late as 1916.113 There were undoubtedly others. Besides the special case of Reynolds Green and the technologists, there are no recorded cases of conversion.But if there was no evidence to convert a dedicated protoplasmist, there was plenty to encourage a dedicated belief in the enzyme theory, and that, I believe, is precisely what happened. The arguments of Buchner et al in support of zymase had the greatest effect not on the protoplasmists but on those who were already predisposed toward the biochemical view. The zymase debate enabled the emerging group of biochemists to recognizethemselves as a group with a community of out-look and objectives; it brought the issue of protoplasm vs. enzyme into the open and gave it a specific and concrete issue on which to turn. The debate sharpened the biochemists' awareness that their point of view was becoming the new mainstream of biochemical thought.All this of course had an important secondary effect on those who opposed the new view, or who were not immediately concerned with it. After the zymase debate, it would have been almost impossible to ignore the new ideas; the dramatic and wide publicity the debate enjoyed would have made it difficult not to take sides. Buchner's successful defense of zymase itself became an important influence on opinion; the new movement had to be looked at with respect. But the primary effect of the debate, I assert, was on those who were already inclined to the new view. The outcome was not a mass conversion of individuals, nor the ejection of one idea by another. The sides probably did not change much; the real change was in the way each side regarded itself and its place in history. The zymase debate may perhaps best be regarded as a process of selection. Buchner's party became aware of itself as the new progressive point of view, while those holding the traditional view could no longer expound it publicly without appearing obstinate or old-fashioned. Thus the way was clear for the gradually wider establishment of the new ideas, especially among the new generation of biochemists. In this specific sense, the acceptance of zymase was a social phenomenon.This way of looking at the zymase debate also illuminates its coincidence with the emergence of biochemistry as a profession. The new professional trappings and organizations were the social manifestation of the new self-awareness gained from the zymase controversy. One of the most important effects on those disposed toward the new view was the awareness of an intellectual community and of the need to give that community social forms. The almost mythical importance of Buchner's “victory” over the old protoplasm theory that later became current is readily understandable. It was a useful ideology for a group anxious to assert the novelty of their approach, a novelty which they in fact felt quite keenly.But if the primary effect of the zymase controversy was on those predisposed to accept zymase, then obviously the success of zymase depended on the fact that change had already begun to occur. Indeed, one of the most striking, and again unexpected, results of this study is the extent to which the importance of enzymes was already recognized in the early 1890's. The new immunology clearly pointed the way. Macfadyen and Hans Buchner were looking for active proteins inside the cell in 1893. Reynolds Green, Wroblewski, and Pfeffer had all anticipated the discovery of a fermentation enzyme. Other discoveries in enzymology in the 1890's pointed the same way.114 Moreover, it is clear from this study that the old protoplams theory was adapting to the new discoveries concerning the importance of enzymes. The sidechains of the old protoplasm molecule were simply reinterpreted as enzymes, as in Wroblewski's theory, for example, or in Paul Ehrlich's extremely influential “sidechain theory” of antibody formation (1897). Despite the later views of Hopkins et al., the old protoplasm and the new enzyme theories were not irreconcilable; a continuity of development had already begun when zymase came so dramatically on the scene. Buchner himself observed that the difference between the two views had become largely verbal; in retrospect we might say, not verbal, but social and historical. The gap between the continuous change in ideas and the contemporary feeling of sharply discontnuous change is a measure of the elusive but real social and historical implications of the zymase debate, of the demise of an old establishment, and the emergence of a new.In retrospect, then, it is clear that a trend was already under way in various quarters when zymase appeared. But it was still a collection of isolated and dispersed events. The zymase controversy made the trend visible and gave it a dramatic unity. The debate influenced those who had already begun to change. It was so effective because things had begun to change and because it coincided with the direction of that trend. (shrink)

There are still on-going debates on what exactly is wrong with Prior’s pathological “tonk.” In this article I argue, on the basis of categorical inferentialism, that two notions of inconsistency ought to be distinguished in an appropriate account of tonk; logic with tonk is inconsistent as the theory of propositions, and it is due to the fallacy of equivocation; in contrast to this diagnosis of the Prior’s tonk problem, nothing is actually wrong with tonk if logic is viewed as the (...) theory of proofs rather than propositions, and tonk perfectly makes sense in terms of the identity of proofs. Indeed, there is fully complete semantics of proofs for tonk, which allows us to link the Prior’s old philosophical idea with contemporary issues at the interface of categorical logic, computer science, and quantum physics, and thereby to expose commonalities between the laws of Reason and the laws of Nature, which are what logic and physics are respectively about. I conclude the article by articulating the ideas of categorical logical positivism and pluralistic unified science as its goal, including the unification of realist and antirealist conceptions of meaning by virtue of the categorical logical basis of metaphysics. (shrink)

This is an abstract of the paper to be submitted to Houston Journal of Mathematics. Our nomenclature and notation will be basically those of [3]. We shall consider algebras of type : T ! N, where T is a nonempty set, and N the set of all positive integers. By V we denote the set of all variables occurring in a polynomial symbol p. An identity p = q is called strongly non-regular if it is of the form p (...) = x for some binary polynomial symbol p, such that x; y 2 V and x =6 y. Let R denote the set of all regular identities of type . If K is a class of algebras of type , then E denotes the set of all identities satised by all algebras in K. We put R = E \ R. A variety K is called strongly non-regular if E contains some strongly non-regular identity. If is a set of identities of type , then K denotes the variety of algebras of type generated by ; E() will be the set of all identities which are consequences of . We put R() = E() \ R. We write ` e if there exists a nite proof of e starting from. (shrink)

Documents, in particular identity cards, mediate relationships between individuals and institutions. Their materiality matters and actively impacts how states govern populations and their movements. In this paper, I examine one such object, the Romanian identity card. Focusing on its temporality and agency, I explore how objects and technological procedures enact race. In Romania, people without an address or proof of residence—many of them members of segregated Roma communities living in deep poverty—can only receive a temporary identity card, (...) the Carte de Idenititate Provizorie (CIP). CIP holders do not enjoy full citizenship and are deprived of various rights, such as the right to travel without a passport within the European Union. They are also exposed to heightened surveillance as they must apply annually for a new CIP. Starting from the material object of the CIP, I explore how race comes into being as a relation at the intersection of various temporalities that are folded into the rules and bureaucratic practice entailed in its issue. I offer the concept of “permanent temporality” to analyze how racialization occurs in practices of governing people and their movement in Europe. (shrink)

Patient narratives from two investigational deep brain stimulation trials for traumatic brain injury and obsessive‐compulsive disorder reveal that injury and illness rob individuals of personal identity and that neuromodulation can restore it. The early success of these interventions makes a compelling case for continued post‐trial access to these technologies. Given the centrality of personal identity to respect for persons, a failure to provide continued access can be understood to represent a metaphorical identity theft. Such a loss recapitulates (...) the pain of an individual's initial injury or illness and becomes especially tragic because it could be prevented by robust policy. A failure to fulfill this normative obligation constitutes a breach of disability law, which would view post‐trial access as a means to achieve social reintegration through this neurotechnological accommodation. (shrink)

The possibility of spectrum inversion has been debated since it was raised by Locke and is still discussed because of its implications for functionalist theories of conscious experience . This paper provides a mathematical formulation of the question of spectrum inversion and proves that such inversions, and indeed bijective scramblings of color in general, are logically possible. Symmetries in the structure of color space are, for purposes of the proof, irrelevant. The proof entails that conscious experiences are not identical with (...) functional relations. It leaves open the empirical possibility that functional relations might, at least in part, be causally responsible for generating conscious experiences. Functionalists can propose causal accounts that meet the normal standards for scientific theories, including numerical precision and novel prediction; they cannot, however, claim that, because functional relationships and conscious experiences are identical, any attempt to construct such causal theories entails a category error. (shrink)

We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the (...) two systems are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other. (shrink)

It seems that the Truth-teller is either true or false, but there is no accepted principle determining which it is. From this point of view, the Truth-teller is a hypodox. A hypodox is a conundrum like a paradox, but consistent. Sometimes, accepting an additional principle will convert a hypodox into a paradox. Conversely, in some cases, retracting or restricting a principle will convert a paradox to a hypodox. This last point suggests a new method of avoiding inconsistency. This article provides (...) a significant example. The Liar paradox can be defused to a hypodox by relatively minimally restricting three principles: the T-schema, substitution of identicals and universal instantiation. These restrictions are not arbitrary. For each, I identify the source of a contradiction given some presumptions. Then I propose each restriction as a reasonable way to deal with that source of contradiction. (shrink)

A Neuroscientist Offers Evidence of Where the Brain Ends and Consciousness Begins.

IN THE GUIDE OF THE PERPLEXED, Maimonides does not treat the doctrine of divine omniscience and divine providence in a strictly theological context. He arrives at this subject for the first time in the third section of the Guide, after he has concluded the thematic treatment of at least the following themes: the names and attributes of God ; the proof of the existence, unity, and incorporeality of God ; the separate intelligences and the order of the world ; the (...) creation of the world ; and prophecy. Directly following the discussion of prophecy is the thematic interpretation of ma‘aseh merkabah —Ezekiel 1 and 10—. This interpretation concludes with the remark that while all of the preceding “up to this chapter,” that is, I 1–III 7, is indispensable for the understanding of ma‘aseh merkabah, the discussion “after this chapter,” that is, from III 8 to the end, will in no way—neither in a detailed manner nor in the form of hints—involve “this subject,” namely ma‘aseh merkabah. Accordingly, Maimonides immediately turns to “other subjects.” Now, for Maimonides ma‘aseh merkabah is identical with metaphysics. The closing remark at the end of Guide III 7 means, then, that while all preceding discussions are of a metaphysical character, the following discussions will not belong to metaphysics. The subjects of the nonmetaphysical section of the Guide are: divine providence ; and the purpose of the Torah in general and of its arrangements in particular. Whatever else may be the case with regard to the plan of the Guide, it is certain that Maimonides, through precisely this plan, excludes the question of divine omniscience and of divine providence from the subject matter of metaphysics. (shrink)

The abolition of slavery after the Revolution of 1789 has always been hailed by the French secular State as proof of the progressivist nature of the Republic. Nevertheless, there has never been any attempt to seriously confront the French involvement in the trade of slaves, which lasted for two centuries. France, a colonial power until the 1960s, which still retains several overseas possessions with an Afro-Caribbean population, has a large resident black population in the mainland which feels it has been (...) deprived of its memory and history and seeks official recognition of the role of the State in the trade of slaves. This article tries to show how a black collective identity and consciousness emerged around the fight for the recognition of slavery as a crime against humanity and the claim for financial compensation. This black collective identity competes with the Jewish community, which was granted financial compensation for the Shoah and which successfully lobbied the State to recognize that it was partly responsible for the genocide in World War II. While some radical black activists seek an alliance with part of the Islamic movement, they are also competing over the recognition of their collective identity by the State with the growing Muslim community whose memory is that of colonization and second-class citizenship. (shrink)

This analysis of Frege's views on language and metaphysics in On Sense and Reference, arguably one of the most important philosophical essays of the past hundred years, provides a thorough introduction to the function/argument analysis and applies Frege's technique to the central notions of predication, identity, existence and truth. Of particular interest is the analysis of the Paradox of Identity and a discussion of three solutions: the little-known Begriffsschrift solution, the sense/reference solution, and Russell's 'On Denoting' solution. Russell's (...) views wend their way through the work, serving as a foil to Frege. Appendices give the proofs of the first 68 propositions of Begriffsschrift in modern notation. This book will be of interest to students and professionals in philosophy and linguistics. (shrink)

Utpaladeva (c. 900–950 C.E.) was the chief originator of the Pratyabhijñā philosophical theology of monistic Kashmiri Śaivism, which was further developed by Abhinavagupta (c. 950–1020 C.E.) and other successors. The Ajaḍapramātṛsiddhi, “Proof of a Sentient Knower,” is one component of Utpaladeva’s trio of specialized studies called the Siddhitrayī, “Three Proofs.” This article provides an introduction to and translation of the Ajaḍapramātṛsiddhi along with the Vṛtti commentary on it by the nineteenth–twentieth century paṇḍit, Harabhatta Shastri. Utpaladeva in this work presents (...) “transcendental” arguments that a universal knower (pramātṛ), the God Śiva, necessarily exists and that this knower is sentient (ajaḍa). He defends the Pratyabhijñā understanding of sentience against alternative views of both Hindu and Buddhist schools. As elsewhere in his corpus, Utpaladeva also endeavors through his arguments to lead students to the recognition (pratyabhijñā) of identity with Śiva, properly understood as the sentient knower. (shrink)

We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley–Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities such as AB=I→BA=I.

Jean Dieudonné, the spokesman of the group of French mathematicians named Bourbaki, called mathematics the music of reason. This metaphor invites a phenomenological account of the affective, in contrast to the epistemic and discursive, nature of mathematics: What constitutes its charm? Mathematical reasoning is described as a perceptual experience, which in Husserl’s late philosophy would be a case of passive synthesis. Like a melody, a mathematical proof is manifest in an affective identity of a temporal object. Rather than an (...) exercise for its own sake, this account sheds a different light on both the epistemic limitation of mathematical science, and the discursive problem of social responsibility in mathematics – two issues at the heart of Husserl’s critique of science as well as of mid-20th century mathematics, for which Nicolas Bourbaki stands as a monument of rigor. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Hume Studies Volume 29, Number 2, November 2003, pp. 205-221 The Origin of the Indirect Passions in the Treatise: An Analogy between Books 1 and 2 HARUKOINOUE 1. The Analogy Between Book 1 and Book 2 If the central design of the Treatise is to demonstrate that "the subjects of the Understanding and Passions make a complete chain of reasoning by themselves" (T 2; SBN xii), as Hume advertises, (...) it seems unquestionable that his intention lies in the illustration of the human mind as an integrated system dependent upon the cooperation of the understanding and the passions, which are discussed separately in Book 1 and Book 2, respectively.1 What is yet to be determined is whether any internal or systematic connection between these two books was originally intended by the author. Is it too fanciful to agree with John Passmore, and to suggest that some dynamic system of the human mind would emerge when we open the door which stands between the first two books?2 The key for this door seems to be found in Hume's account of personal identity. We may well remember how he distinguished two aspects of our identity, one regarding the understanding and another regarding the passions, and claimed that the latter "serves to corroborate" the former "by the making our distant perceptions influence each other, and by giving us a present concern for our past or future pains or pleasures" (T 1.4.6.19; SBN Haruko Inoue is Professor of Philosophy, Sapporo University 3-7-3-1 Toyohira-ku, Sapporo 062-8520, Japan. e-mail: [email protected] 206 Haruko Inoue 261). It seems reasonable to agree with Jane Mclntyre, who suggests that "Hume recognized questions about personal identity not addressed in Book 1, and that Book 2 makes an important contribution to our understanding of Hume's account of the self and its identity."3 And once we get a good understanding of this integrated mechanism of the human mind operating with both wheels, as it were, of the imagination and the passions, all we have to do is to accept his invitation and enjoy the efficiency of this two-wheeled car, driving through the fields of "Morals, Politics, and Criticism." For, if we take his words in his Advertisement seriously,4 it seems quite likely that the Treatise was published first as a set of Book 1 and Book 2, as Passmore suggests,5 and that Book 3 was written as the demonstration of the consistency of his system through the application of the hypothesis established in the first two books. This paper is a modest attempt to illustrate the intimate connection between Book 1 and Book 2: the latter, planned as a proof and reinforcement of the system Hume had established in Book 1, depends on the former. His basic strategy in the Treatise is to explain both systems of the mind by means of the easy transition of the imagination, which connects different perceptions with each other according to two kinds of principles or "properties of human nature " (T 2.1.4.2; SBN 283), viz. "the association both of impressions and ideas, and the mutual assistance they lend each other" (T 2.1.5.5; SBN 284). In Book 1 Hume establishes the system of the understanding in terms of the first association, viz. the association of ideas, and in Book 2 he proceeds to illustrate the system of passions by involving not only the second association but also the concurrence of both kinds of association which he calls "a double relation of impressions and ideas." His basic strategy is thus to apply the same method of reasoning to the illustration of both systems, assuming that "there is an attraction or association among impressions, as well as among ideas" (T 2.1.4.3; SBN 283). The intimate connection between the two systems of the understanding and the passions is illustrated through the demonstration of the "influence of the imagination upon the passions" (T 2.3.6.1; SBN 424), or in terms of the dependence of the latter on the former. It is owing to the dependence of the association of... (shrink)

The first section of this paper is concerned with the intrinsic properties of elementary monadic logic (EM), and characterizations in the spirit of Lindström [2] are given. His proofs do not apply to monadic logic since relations are used, and intrinsic properties of EM turn out to differ in certain ways from those of the elementary logic of relations (i.e., the predicate calculus), which we shall call EL. In the second section we investigate connections between higher-order monadic and polyadic (...) logics.EM is the subsystem of EL which results by the restriction to one-place predicate letters. We omit constants (for simplicity) but take EM to contain identity. Let atypebe any finite sequence (possibly empty) of one-place predicate letters. A modelMof typehas a nonempty universe ∣M∣ and assigns to each predicate letterPofa subsetPMof ∣M∣.Let us take a monadic logicLto be any collection of classes of models, calledL-classes, satisfying the following:1. All models in a givenL-class are of the same type (called the type of the class).2. Isomorphic models lie in the sameL-classes.3. IfandareL-classes of the same type, thenandareL-classes. (shrink)

At some step in proving the Liar Paradox in natural language, a sentence is derived that seems overdetermined with respect to its semantic value. This is complemented by Tarski’s Theorem that a formal language cannot consistently contain a naive truth predicate given the laws of logic used in proving the Liar paradox. I argue that proofs of the Eubulidean Liar either use a principle of truth with non-canonical names in a fallacious way or make a fallacious use of substitution (...) of identicals. Tarski never committed the first fallacy and may have himself considered it fallacious. Nevertheless, I clarify that it is fallacious. I then argue substitution of identicals needs to be restricted within the scope of the truth predicate. A logic for truth implementing this restriction is a monotonic extension of a classical first order logic, or indeed a formalizable fragment of natural language. Proofs of Tarski’s Indefinability of Truth theorem are invalid in this logic. This approach generalizes to invalidate proofs of Liar-like paradoxes, particularly the predicate form of the Knower paradox. Consequently, such a logic can be further extended in a way that avoids Montague’s theorem for such a system. Yet, the semantic status of a Liar sentence is not fully resolved. It is no longer overdetermined; it is now underdetermined. (shrink)

The paper is concerned with Quine's substitutional account of logical truth. The critique of Quine's definition tends to focus on miscellaneous odds and ends, such as problems with identity. However, in an appendix to his influential article On Second Order Logic, George Boolos offered an ingenious argument that seems to diminish Quine's account of logical truth on a deeper level. In the article he shows that Quine's substitutional account of logical truth cannot be generalized properly to the general concept (...) of logical consequence. The purpose of this paper is threefold: first, to introduce the reader to the metamathematics of Quine's substitutional definition of logical truth; second, to make Boolos' result accessible to a broader audience by giving a detailed and self-contained presentation of his proof; and, finally, to discuss some of the possible implications and how a defender of the Quinean concepts might react to the challenge posed by Boolos' result. (shrink)

One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.

In Britain and, I think, America at least the “idealist movement” in philosophy is very widely regarded as a spent force, as a subject only for historical study. There are indeed different definitions of “idealism.” The term was defined explicitly by at least one distinguished British philosopher as covering “all those philosophies which agree in maintaining that spiritual values have a determining voice in the ordering of the universe.” This doctrine, though unfortunately less vocal than it was, has by no (...) means died out, and will not as long as there are theists who talk about God in any but a subjectivist sense. But a theist would not usually be called an idealist unless he based his theism on a particular kind of approach to the problems of metaphysics. Further, the term “idealist” would also be applied to a pessimist like Schopenhauer, for whom evil rather than good was conceived as predominant and whose philosophy could certainly not be described in the above terms. Some would apply it to philosophers who did not make any positive metaphysical assertion but only insisted that we had to reduce the concept of physical objects to a concept for organising human experience. Like -isms in general the term “idealism” has therefore a distinctly varied connotation; but in its most characteristic and influential form it was an attempt to give a philosophical proof of the essential doctrines of religion or at least of something which, though not identical with orthodox Christianity, provided an adequate substitute for it, being the philosophical truth which the teachings of the Church metaphorically expressed. (shrink)