A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem A in intuitionistic logic has a unique -normal proof in NJ whenever A is (...) provable without non-prime contraction. The non-prime contraction rule in NJ is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. Our result improves the known partial positive solutions to Komori's problem. Also, we present another simple example of a minimal implicational theorem in intuitionistic logic which does not have a unique -normal proof in NJ. (shrink)

A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the following: (1) A β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK.

We show that in quantum logic of closed subspaces of Hilbert space one cannot substitute quantum operations for classical (standard Hilbert space) ones and treat them as primitive operations. We consider two possible ways of such a substitution and arrive at operation algebras that are not lattices what proves the claim. We devise algorithms and programs which write down any two-variable expression in an orthomodular lattice by means of classical and quantum operations in an identical form. Our results show that (...) lattice structure and classical operations uniquely determine quantum logic underlying Hilbert space. As a consequence of our result, recent proposals for a deduction theorem with quantum operations in an orthomodular lattice as well as a, substitution of quantum operations for the usual standard Hilbert space ones in quantum logic prove to be misleading. Quantum computer quantum logic is also discussed. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Martin Heidegger and OntologyEmmanuel Levinas (bio)The prestige of Martin Heidegger 1 and the influence of his thought on German philosophy marks both a new phase and one of the high points of the phenomenological movement. Caught unawares, the traditional establishment is obliged to clarify its position on this new teaching which casts a spell over youth and which, overstepping the bounds of permissibility, is already in vogue. For once, (...) Fame has picked one who deserves it and, for that matter, one who is still living. Anyone who has studied philosophy cannot, when confronted by Heidegger’s work, fail to recognize how the originality and force of his achievements, stemming from genius, are combined with an attentive, painstaking, and close working-out of the argument—with that craftsmanship of the patient artisan in which phenomenologists take such pride. In this study, it is important for us to understand, above all, the true intentions of our author, to illuminate what he thinks really needs to be said, and to surmise what is most critical for him.To get to the heart of Heidegger’s system, it seems fitting to begin with a problem that is generally familiar. We choose the problem of knowledge, a deeper understanding of which takes us to the very threshold of Heidegger’s thought. For this problem, central to modern philosophy, is one of the main obstacles of modern philosophy that Heidegger wishes to surmount. Neo-Kantianism, which takes knowledge as the philosophical problem of the first rank, is the movement against which Heidegger rebels with all his strength. We have, thus, every chance of gaining access to his thought by the main door, so to speak. Once inside the system we will try to trace its outlines, 2 reserving, for a second part of our work, the determination of Heidegger’s place in the history of ideas, especially in the phenomenological movement, as well as of his relations with the philosopher to whom he owes so much—Edmund Husserl. 31In its most general form, the problem of the theory of knowledge has a critical significance. It consists in delineating a domain where knowledge can be certain and in determining the criteria for the legitimate scope of knowledge. But this problem, as normal and as simple as it may appear, has deeper roots. That knowledge should need a criterion at all presupposes that truth is not identical to all that is known and that the course [End Page 11] of things can fail to correspond with the course of thought. “How does knowledge correspond to being?” is a more profound formulation of the problem of knowledge.But we are not going to touch anymore on the primordial phenomenon that generates the problem. The problem of correspondence between thing and thought presupposes a free activity of thought and its isolation in relation to the object. It is precisely this presupposition which renders their harmony and even their contact problematic. “How does the subject take leave of itself to attain the object?” is what the problem of knowledge, in the last analysis, boils down to. Its true source is thus the concept of “subject” as elaborated by modern philosophy. The cogito presided over the subject’s birth. The cogito was the affirmation of the privileged nature of the subject’s immanent sphere, of its unique place in existence; hence, the cogito was the specificity of the subject’s connection to the rest of reality, the sui generis nature which opens up the passage from immanence to transcendence, the passage from ideas contained in the thinking substance to 4 their “formal existence.”The concept of the subject, understood as a substance having a specific position in the entire domain of being, presents us with difficulties of two kinds. First, how do we understand this leave-taking from the self which the thinking substance brings about and which displays an entirely original aspect? Indeed, we could say that thought, in reaching out toward objects, does not actually take leave of itself, since its objects—considered as ideas and contents of thought—are, in a certain sense, already within it. In order to make sense of this paradox, Descartes... (shrink)

In this paper, I provide a thorough discussion and reconstruction of Bernard Bolzano’s theory of grounding and a detailed investigation into the parallels between his concept of grounding and current notions of normal proofs. Grounding (Abfolge) is an objective ground-consequence relation among true propositions that is explanatory in nature. The grounding relation plays a crucial role in Bolzano’s proof-theory, and it is essential for his views on the ideal buildup of scientific theories. Occasionally, similarities have been pointed out (...) between Bolzano’s ideas on grounding and cut-free proofs in Gentzen’s sequent calculus. My thesis is, however, that they bear an even stronger resemblance to the normal natural deduction proofs employed in proof-theoretic semantics in the tradition of Dummett and Prawitz. (shrink)

A complementary system for a given logic is a proof system whose theorems are exactly the formulas that are not valid according to the logic in question. This article is a contribution to the complementary proof theory of classical propositional logic. In particular, we present a complementary proof-net system, $$\textsf{CPN}$$ CPN, that is sound and complete with respect to the set of all classically invalid (one-side) sequents. We also show that cut elimination in $$\textsf{CPN}$$ CPN enjoys strong normalization along with (...) strong confluence (and, hence, uniqueness of normal forms). (shrink)

Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but which differs again (...) in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems. (shrink)

A notation for an ordinal using patterns of resemblance is based on choosing an isominimal set of ordinals containing the given ordinal. There are many choices for this set meaning that notations are far from unique. We establish that among all such isominimal sets there is one which is smallest under inclusion thus providing an appropriate notion of normal form notation in this context. In addition, we calculate the elements of this isominimal set using standard notations based on collapsing (...) functions. This provides a capstone to the results in [2, 6, 8, 9, 7], using further refinement of ordinal arithmetic developed in [8] which then both allows for a simple characterization of normal forms for patterns of order one and will play a key role in the arithmetical analysis of pure patterns of order two, [5]. (shrink)

I give an account of proof terms for derivations in a sequent calculus for classical propositional logic. The term for a derivation δ of a sequent Σ≻Δ encodes how the premises Σ and conclusions Δ are related in δ. This encoding is many–to–one in the sense that different derivations can have the same proof term, since different derivations may be different ways of representing the same underlying connection between premises and conclusions. However, not all proof terms for a sequent Σ≻Δ (...) are the same. There may be different ways to connect those premises and conclusions. -/- Proof terms can be simplified in a process corresponding to the elimination of cut inferences in sequent derivations. However, unlike cut elimination in the sequent calculus, each proof term has a unique normal form (from which all cuts have been eliminated) and it is straightforward to show that term reduction is strongly normalising—every reduction process terminates in that unique normal form. Further- more, proof terms are invariants for sequent derivations in a strong sense—two derivations δ1 and δ2 have the same proof term if and only if some permutation of derivation steps sends δ1 to δ2 (given a relatively natural class of permutations of derivations in the sequent calculus). Since not every derivation of a sequent can be permuted into every other derivation of that sequent, proof terms provide a non-trivial account of the identity of proofs, independent of the syntactic representation of those proofs. (shrink)

Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four-valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro’s tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in a (...) previous work we presented a sequent system for TML with the cut-elimination property. Besides, in this same work, it was also presented a sound and complete natural deduction system for this logic. In the present article we continue with the study of TML under a proof-theoretic perspective. In the first place, we show that the natural deduction system that we introduced before admits a normalization theorem. In the second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced by A. V. Figallo and P. Landini, we define a decidable tableau system adequate to check validity in the logic TML. Finally, we provide a sound and complete tableau system for TML in the original language. These two tableau systems constitute new (proof-theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras. (shrink)

Montague [7] translates English into a tensed intensional logic, an extension of the typed -calculus. We prove that each translation reduces to a formula without -applications, unique to within change of bound variable. The proof has two main steps. We first prove that translations of English phrases have the special property that arguments to functions are modally closed. We then show that formulas in which arguments are modally closed have a unique fully reduced -normal form. As a corollary, translations (...) of English phrases are contained in a simply defined proper subclass of the formulas of the intensional logic. (shrink)

In this paper I will show the problems that are encountered when dealing with uniqueness of connectives in a bilateralist setting within the larger framework of proof-theoretic semantics and suggest a solution. Therefore, the logic 2Int is suitable, for which I introduce a sequent calculus system, displaying - just like the corresponding natural deduction system - a consequence relation for provability as well as one dual to provability. I will propose a modified characterization of uniqueness incorporating such a (...) duality of consequence relations, with which we can maintain uniqueness in a bilateralist setting. (shrink)

The standard argument for the uniqueness of the Einstein field equation is based on Lovelock's Theorem, the relevant statement of which is restricted to four dimensions. I prove a theorem similar to Lovelock's, with a physically modified assumption: that the geometric object representing curvature in the Einstein field equation ought to have the physical dimension of stress-energy. The theorem is stronger than Lovelock's in two ways: it holds in all dimensions, and so supports a generalized argument for uniqueness; (...) it does not assume that the desired tensor depends on the metric only up second-order partial-derivatives, that condition being a consequence of the proof. This has consequences for understanding the nature of the cosmological constant and theories of higher-dimensional gravity. Another consequence of the theorem is that it makes precise the sense in which there can be no gravitational stress-energy tensor in general relativity. Along the way, I prove a result of some interest about the second jet-bundle of the bundle of metrics over a manifold. (shrink)

There have been numerous results showing that a measurable cardinal κ can carry exactly α normal measures in a model of GCH, where a is a cardinal at most κ⁺⁺. Starting with just one measurable cardinal, we have [9] (for α = 1), [10] (for α = κ⁺⁺, the maximum possible) and [1] (for α = κ⁺, after collapsing κ⁺⁺) . In addition, under stronger large cardinal hypotheses, one can handle the remaining cases: [12] (starting with a measurable cardinal (...) of Mitchell order α ) , [2] (as in [12], but where κ is the least measurable cardinal and α is less than κ, starting with a measurable of high Mitchell order) and [11] (as in [12], but where κ is the least measurable cardinal, starting with an assumption weaker than a measurable cardinal of Mitchell order 2). In this article we treat all cases by a uniform argument, starting with only one measurable cardinal and applying a cofinality-preserving forcing. The proof uses κ-Sacks forcing and the "tuning fork" technique of [8]. In addition, we explore the possibilities for the number of normal measures on a cardinal at which the GCH fails. (shrink)

Local proper scoring rules provide convenient tools for measuring subjective probabilities. Savage, 783–801, 1971) has shown that the only local proper scoring rule for more than two exclusive events is the logarithmic family. We generalize Savage by relaxing the properness and the domain, and provide simpler proof.

We prove there are theories (stable or countable) for which over every A there is a prime model but it is not necessarily unique. We also give a simplified proof of the uniqueness theorem for countable stable theories.

In this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method à la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be (...) well founded. MSC: 03F05, 03B15. (shrink)

We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

Theoretical works in economics usually have a core consisting of proofs that a “model-economy” has certain properties. The economist constructs a model that can be looked on as a description of an economy, and then proves that certain relations hold in this economy and/or that certain relations in this economy depend on certain specific characteristics. The model-economy is usually described as simplified or idealized.

We show that the Bub-Clifton uniqueness theorem (1996) for 'no collapse' interpretations of quantum mechanics can be proved without the 'weak separability' assumption.

The constructive functional calculus for a sequence of commuting selfadjoint operators on a separable Hilbert space is shown to be independent of the orthonormal basis used in its construction. The proof requires a constructive criterion for the absolute continuity of two positive measures in terms of test functions.

Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically (...) motivated ways? This informal question motivates the formulation of intercalation calculi. Ic-calculi are the technical underpinnings for (1) and (2), and our paper focuses on their detailed presentation and meta-mathematical investigation in the case of classical predicate logic. As a central theme emerges the connection between restricted forms of nd-proofs and (strategies for) proof search: normal forms are not obtained by removing local "detours", but rather by constructing proofs that directly reflect proof-strategic considerations. That theme warrants further investigation. (shrink)

The Löwenheim-Skolem theorem was published in Skolem's long paper of 1920, with the first section dedicated to the theorem. The second section of the paper contains a proof-theoretical analysis of derivations in lattice theory. The main result, otherwise believed to have been established in the late 1980s, was a polynomial-time decision algorithm for these derivations. Skolem did not develop any notation for the representation of derivations, which makes the proofs of his results hard to follow. Such a formal notation (...) is given here by which these proofs become transparent. A third section of Skolem's paper gives an analysis for derivations in plane projective geometry. To clear a gap in Skolem's result, a new conservativity property is shown for projective geometry, to the effect that a proper use of the axiom that gives the uniqueness of connecting lines and intersection points requires a conclusion with proper cases (logically, a disjunction in a positive part) to be proved. The forgotten parts of Skolem's first paper on the Löwenheim-Skolem theorem are the perhaps earliest combinatorial analyses of formal mathematical proofs, and at least the earliest analyses with profound results. (shrink)

Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic 64 27–94.We consider uniqueness theorems in classical analysis having the form u ε U, v1, v2 ε Vu = 0 = G→v 1 = v2), where U, V are complete separable metric spaces, Vu is compact in V and G:U x V → is a constructive function.If is proved by arithmetical means from (...) analytical assumptions x εXy ε Yx z ε Z = 0) only , then we can extract from the proof of → an effective modulus of uniqueness, which depends on u, k but not on v1,v2, i.e., u ε U, v1, v2 ε Vu, k εG, G 2-φuk→dv2-itk). Such a modulus φ can e.g. be used to give a finite algorithm which computes the zero of G on Vu with prescribed precision if it exists classically.The extraction of φ uses a proof-theoretic combination of functional interpretation and pointwise majorization. If the proof of → uses only simple instances of induction, then φ is a simple mathematical operation. (shrink)

Natural deduction (for short: nd-) calculi have not been used systematically as a basis for automated theorem proving in classical logic. To remove objective obstacles to their use we describe (1) a method that allows to give semantic proofs of normal form theorems for nd-calculi and (2) a framework that allows to search directly for normal nd-proofs. Thus, one can try to answer the question: How do we bridge the gap between claims and assumptions in heuristically (...) motivated ways? This informal question motivates the formulation of intercalation calculi. Ic-calculi are the technical underpinnings for (1) and (2), and our paper focuses on their detailed presentation and meta-mathematical investigation in the case of classical predicate logic. As a central theme emerges the connection between restricted forms of nd-proofs and (strategies for) proof search: normal forms are not obtained by removing local "detours", but rather by constructing proofs that directly reflect proof-strategic considerations. That theme warrants further investigation. (shrink)

Statman and Orevkov independently proved that cut-elimination is of nonelementary complexity. Although their worst-case sequences are mathematically different the syntax of the corresponding cut formulas is of striking similarity. This leads to the main question of this paper: to what extent is it possible to restrict the syntax of formulas and — at the same time—keep their power as cut formulas in a proof? We give a detailed analysis of this problem for negation normal form , prenex normal (...) form and monotone formulas. We show that proof reduction to NNF is quadratic, while PNF behaves differently: although there exists a quadratic transformation into a proof in PNF too, additional cuts are needed; the elimination of these cuts requires nonelementary expense in general. By restricting the logical operators to {,,,}, we obtain the type of monotone formulas. We prove that the elimination of monotone cuts can be of nonelementary complexity . On the other hand, we define a large class of problems where cut-elimination of monotone cuts is only exponential and show that this bound is tight. This implies that the elimination of monotone cuts in equational theories is at most exponential. Particularly, there are no short proofs of Statman's sequence with monotone cuts. (shrink)

Philologus, founded in 1846, is one of the oldest and most respected periodicals in the field of Classics. It publishes articles on Greek and Latin literature, historiography, philosophy, history of religion, linguistics, reception, and the history of scholarship. The journal aims to contribute to our understanding of Greco-Roman culture and its lasting influence on European civilization. The journal Philologus, conceived as a forum for discussion among different methodological approaches to the study of ancient texts and their reception, publishes original scholarly (...) contributions with a strong international focus. Publications languages are: German, English, Italian, French. As of 2014 the publication of supplementary volumes will be resumed. The series Philologus. Supplemente / Philologus. Supplementary Volumes will publish monographs and edited volumes pertaining to all aspects of the study of ancient literature and its reception, with a special focus on topics concerning literary theory, philosophy and the history of scholarship from an interdisciplinary perspective. (shrink)

For millennia, diagnosticians distinguished natural sadness that arose from social circumstances from depressive disorders that were disproportionate to their contexts. In 1980, the DSM-III transformed this tradition through equating depressive disorders with symptoms without regard to context. Nevertheless, it excluded grieving people without especially severe or enduring symptoms from diagnosis. Subsequently, considerable empirical research indicated that bereavement was not unique but a model for all stressor-maintained conditions. Yet, despite the evidence showing that the causes, prognoses, and optimal treatments for context-specific (...) depressions differ from those that aren’t, the DSM-5 removed the bereavement exclusion from the diagnostic criteria for major depression. This article considers the reasons behind this elimination and its implications for the research, labeling, and treatment of depression. (shrink)

Objective Apeiron was founded in 1966 and has developed into one of the oldest and most distinguished journals dedicated to the study of ancient philosophy, ancient science, and, in particular, of problems that concern both fields. Apeiron is committed to publishing high-quality research papers in these areas of ancient Greco-Roman intellectual history; it also welcomes submission of articles dealing with the reception of ancient philosophical and scientific ideas in the later western tradition. The journal appears quarterly. Articles are peer-reviewed on (...) a double-blind basis. Topics ancient philosophy ancient science reception of ancient philosophical and scientific ideas in the later western tradition Article formats Original Articles. (shrink)

The Nuts and Bolts of Proofs: An Introduction to Mathematical Proofs, Fifth Edition provides basic logic of mathematical proofs and shows how mathematical proofs work. It offers techniques for both reading and writing proofs. The second chapter of the book discusses the techniques in proving if/then statements by contrapositive and proofing by contradiction. It also includes the negation statement, and/or. It examines various theorems, such as the if and only-if, or equivalence theorems, the existence theorems, (...) and the uniqueness theorems. In addition, use of counter examples, mathematical induction, composite statements including multiple hypothesis and multiple conclusions, and equality of numbers are covered in this chapter. The book also provides mathematical topics for practicing proof techniques. Included here are the Cartesian products, indexed families, functions, and relations. The last chapter of the book provides review exercises on various topics. Undergraduate students in engineering and physical science will find this book accessible as well as invaluable. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:The Birth of the Psychoanalytic Hero:Freud's Platonic LeonardoJohn FarrellThough the intellectual force of Freudian psychoanalysis grows weaker and weaker with time, its importance for the understanding of twentieth-century intellectual culture only increases. Freud made psychology a key ingredient in the century's conception of its own uniqueness and modernity. He claimed to initiate a decisive break with the past, but he also claimed to recover the past, indeed all (...) of human behavior, on new, scientific grounds. What Freud proposed was not just a new way of thinking about psychology but a new psychology, one that would permit unprecedentedly intrepid investigation of the past and the unconscious sources of its ways of thinking. But whereas Freud hoped to give us a new psychology of knowledge, what he did was to reintroduce one of the oldest psychologies of knowledge in a moderately disguised form. I will attempt to show this and assess the implications through a close examination of Freud's treatment of Leonardo da Vinci, a man he considered one of the great forerunners of the modern intellect.Psychoanalysis is both a theory of the psyche and a scientific movement. Its dual nature makes it almost a unique element in the culture of modern science. Freud and his followers repudiated the separation between institutional affiliation and intellectual commitment that had been carried down from seventeenth-century England. The original form of the psychoanalytic movement was a throwback to that of the ancient philosophical academies.1 Almost from the beginning of psychoanalysis its founders had recourse to a canon of dogma with the primacy of the libido at its center. Adherence to this canon, and the rituals of initiation and training surrounding it, became the basis for [End Page 233] an exclusive intellectual and professional commitment that separated initiates from the professional community at large.It is well known that the founders of psychoanalysis made use of psychoanalytic theory to explain the movement's adversarial relationship with the outside world. The doctrine of resistance to the libido allowed Freudians to interpret the hidden motives of anyone who might disagree with them. The ire of critics could be cited as proof of the intensity of unconscious repression applied to sexuality, the incredulity of unbelievers as evidence of an unwillingness to endure the wounds to human narcissism exacted by the Freudian system, and even slips of the tongue could be turned against unwitting opponents. The fact that psychoanalysis was greeted with hostility in some quarters was taken to prove that the universal tendency of humankind was to resist its teachings, and the lapsing away of prominent disciples illustrated the difficulty of living with these hard truths. Heretics were pitied as weaklings unable to face up to the power of the unconscious, unable to keep themselves from disguising it with it some pale reflection of the ego. And so the embattled history of psychoanalysis became part of the empirical evidence of its validity in a way that could never have occurred with a theory generated in the normal research environment. The doctrine of resistance seemed to have been designed as much for polemical as for analytic purposes. Like the monster in Forbidden Planet, the fifties Freudian fairy tale, the more psychoanalysis was resisted, the more it grew. The self-confirming value that could be derived from the history of the movement as a cultural scandal even led Freud to exaggerate the hostility of his early reception and the intensity of his early isolation. With the doctrine of resistance, Freud had imported into science the style of the avant-garde, which feeds upon rejection, outrage, and the breach of bourgeois manners. The concept of "resistance to psychoanalysis" is still in use among psychoanalysts today.The argument from resistance, however useful it may have been as a defense mechanism of psychoanalytic rhetoric, leads to a troubling theoretical question: If the truths of psychoanalysis are naturally repugnant to humankind, so much so that we have a powerful constitutional tendency to hide them from ourselves, what could have liberated Freud and his followers to unearth these unwelcome secrets from the depths of their own psyches? If we take the "resistance to psychoanalysis" as a... (shrink)

Recent magnetic resonance imaging and pathological studies have indicated that axonal loss is a major contributor to disease progression in multiple sclerosis. 1 H magnetic resonance spectroscopy, through measurement of N -acetyl aspartate, a neuronal marker, provides a unique tool to investigate this. Patients with primary progressive multiple sclerosis have few lesions on conventional MRI, suggesting that changes in normal appearing white matter, such as axonal loss, may be particularly relevant to disease progression in this group. To test this (...) hypothesis NAWM was studied with MRS, measuring the concentration of N -acetyl derived groups. Single-voxel MRS using a water-suppressed PRESS sequence was carried out in 24 patients with primary progressive multiple sclerosis and in 16 age-matched controls. Ratios of metabolite to creatine concentration were calculated in all subjects, and absolute concentrations were measured in 18 patients and all controls. NA/Cr was significantly lower in NAWM in patients than in controls, as was the absolute concentration of NA. There was no significant difference in the absolute concentration of creatine between the groups. This study supports the hypothesis that axonal loss occurs in NAWM in primary progressive multiple sclerosis and may well be a mechanism for disease progression in this group. (shrink)

Philologus, founded in 1846, is one of the oldest and most respected periodicals in the field of Classics. It publishes articles on Greek and Latin literature, historiography, philosophy, history of religion, linguistics, reception, and the history of scholarship. The journal aims to contribute to our understanding of Greco-Roman culture and its lasting influence on European civilization. The journal Philologus, conceived as a forum for discussion among different methodological approaches to the study of ancient texts and their reception, publishes original scholarly (...) contributions with a strong international focus. Publications languages are: German, English, Italian, French. As of 2014 the publication of supplementary volumes will be resumed. The series Philologus. Supplemente / Philologus. Supplementary Volumes will publish monographs and edited volumes pertaining to all aspects of the study of ancient literature and its reception, with a special focus on topics concerning literary theory, philosophy and the history of scholarship from an interdisciplinary perspective. (shrink)

Hence, there is still controversy over which of the two versions of the deduction deserves priority and whether indeed any distinction between them can be maintained that would go beyond questions of presentation and involve the structure of the proof itself. Schopenhauer and Heidegger held that the first edition alone fully expresses Kant's unique philosophy, while Kant himself, as well as many other Kantians, have only seen a difference in the method of presentation.

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on assertion, denial, and bi-lateralism, (ii) remarks on compositionality in proof-theoretic semantics, and (iii) comments on falsification and co-implication. The main formal result of the paper is a normal form theorem for the natural deduction proof system N2Int (...) of the bi-intuitionistic logic 2Int. The proof makes use of the faithful embedding of 2Int into intuitionistic logic with respect to validity and shows that conversions of dual proofs can be sidestepped. (shrink)