8.3 The consistency proof -- 8.4 Applications of the consistency proof -- 8.5 Second-order arithmetic -- Problems -- Chapter 9: Set Theory -- 9.1 Axioms for sets -- 9.2 Development of set theory -- 9.3 Ordinals -- 9.4 Cardinals -- 9.5 Interpretations of set theory -- 9.6 Constructible sets -- 9.7 The axiom of constructibility -- 9.8 Forcing -- 9.9 The independence proofs -- 9.10 Large cardinals -- Problems -- Appendix The Word Problem -- Index.

Comprehensive account of constructive theory of first-order predicate calculus. Covers formal methods including algorithms and epi-theory, brief treatment of Markov’s approach to algorithms, elementary facts about lattices and similar algebraic systems, more. Philosophical and reflective as well as mathematical. Graduate-level course. 1963 ed. Exercises.

The author attacks the view that identity, Like largeness, Is a relative relation. The primary advocate of the view that identity is relative is p.T. Geach. It is argued that geach has not shown that the failure of the identity of indiscernibles principle, As a truth of logic, Forces us to stop taking indiscernibility within particular formal theories or languages as a sufficient condition for identity. The author also argues that the whole notion of relative identity, As explicated by geach, (...) Is very probably incoherent. (shrink)

The present volume is intended as an all-round introduction to constructivism. Here constructivism is to be understood in the wide sense, and covers in particular Brouwer's intuitionism, Bishop's constructivism and A.A. Markov's constructive recursive mathematics. The ending "-ism" has ideological overtones: "constructive mathematics is the (only) right mathematics"; we hasten, however, to declare that we do not subscribe to this ideology, and that we do not intend to present our material on such a basis.

Truth-maker analyses construe truth as existence of proof, a well-known example being that offered by Wittgenstein in theTractatus. The paper subsumes the intuitionistic view of truth as existence of proof under the general truth-maker scheme. Two generic constraints on truth-maker analysis are noted and positioned with respect to the writings of Michael Dummett and theTractatus. Examination of the writings of Brouwer, Heyting and Weyl indicates the specific notions of truth-maker and existence that are at issue in the intuitionistic truth-maker analysis, (...) namely that of proof in the sense of proof-object (Brouwer, Heyting) and existence in the nonpropositional sense of a judgement abstract (Weyl). Furthermore, possible anticipations in the writings of Schlick and Pfänder are noted. (shrink)

This is a long-awaited new edition of one of the best known Oxford Logic Guides. The book gives an introduction to intuitionistic mathematics, leading the reader gently through the fundamental mathematical and philosophical concepts. The treatment of various topics, for example Brouwer's proof of the Bar Theorem, valuation systems, and the completeness of intuitionistic first-order logic, have been completely revised.

This book, Foundations of Constructive Analysis, founded the field of constructive analysis because it proved most of the important theorems in real analysis by constructive methods. The author, Errett Albert Bishop, born July 10, 1928, was an American mathematician known for his work on analysis. In the later part of his life Bishop was seen as the leading mathematician in the area of Constructive mathematics. From 1965 until his death, he was professor at the University of California at San Diego.

Le 27 avril 1938, Edmund HUSSERL, l'initiateur et principal representant du courant phenomenologique dans la philosophie contemporaine, mourut a Fribourg en Brisgau, age de pres de quatre-vingts ans. Depuis la parution de ses Logische Untersuchungen en 190~ 1901, le monde philosophique international avait suivi, avec UD interet toujours croissant, les exposes successifs et de plus en plus approfondis, que le maUre fribourgeois publiait sur les prin~ cipes de sa methode, dite pMnomenologique, sur les applications concretes de celle-ci aux problemes philosophiques (...) les plus divers, ainsi que sur la phenomenologie comme systeme philo­ sophique autonome et pour ainsi dire "autarchique". Ces publi­ cations, relativement peu nombreuses, mais fort remarquees des leur parution, furent etudiees avec le plus grand soin par les representants les plus autorises des differents courants de la pensee contemporaine. Les critiques, il va sans dire, ne manquerent point. On attira l'attention sur le caractere plutöt programmatique de ces etudes, sur la terminologie fort neuve, quelque peu arbitraire, parfois meme deroutante, dont se servait l'auteur, sur son pen­ chant prononce pour des distinctions subtiles et pour des defini­ tions minutieuses a l'exces, sur la difficulte de son style et les complications parfois inutiles de son expose, enfin et surtout -­ au moins depuis 1913 - sur le caractere audacieux de sa theorie de la reduction, presentee par lui avec une insistance toute par­ ticuliere comme le fondement dernier et indispensable de toute phenomenologie presente ou future. (shrink)

Without violating the spirit of Game-Theoretical semantics, its results can be re-worked in Martin-Löf''s Constructive Type Theory by interpreting games as types of Myself''s winning strategies. The philosophical ideas behind Game-Theoretical Semantics in fact highly recommend restricting strategies to effective ones, which is the only controversial step in our interpretation. What is gained, then, is a direct connection between linguistic semantics and computer programming.

Martin-Löf's constructive type theory forms the basis of this paper. His central notions of category and set, and their relations with Russell's type theories, are discussed. It is shown that addition of an axiom - treating the category of propositions as a set and thereby enabling higher order quantification - leads to inconsistency. This theorem is a variant of Girard's paradox, which is a translation into type theory of Mirimanoff's paradox (concerning the set of all well-founded sets). The occurrence of (...) the contradiction is explained in set theoretical terms. Crucial here is the way a proof-object of an existential proposition is understood. It is shown that also Russell's paradox can be translated into type theory. The type theory extended with the axiom mentioned above contains constructive higher order logic, but even if one only adds constructive second order logic to type theory the contradictions arise. (shrink)

This book traces the development of formal logic from its origins inancient Greece to the present day. The authors first discuss the work oflogicians from Aristotle to Frege, showing how they were influenced by thephilosophical or mathematical ideas of their time. They then examinedevelopments in the present century.

Die einwandfreie Bestimmung der Begriffe ist die Grundlage einer jeden wissenschaftlichen Arbeit. Im Sinne der modernen Logik und Axiomatik hat erstmals Walter Dubislav die Methode des Definierens von Begriffen systematisch wie auch an Beispielen entwickelt. Sein Werk zeichnet sich durch klare Gedankenführung und didaktisches Geschick bei der Vermittlung philosophischer Sachverhalte aus, und es diskutiert alle einschlägigen Fragen, die sich dem an Methoden interessierten Wissenschaftler stellen. Es hat daher auch heute noch seinen systematischen Wert. Den gegenwärtigen Stand der Forschung im B...

In recent years, several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-L f. Well suited as a theory for program construction, it makes possible the expression of both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. This book contains a thorough introduction to type theory, (...) with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples. (shrink)

It is the aim of INDICES to document recent explorations in the various fields of philosophical logic and formal linguistics and their applications in other disciplines. The main emphasis of this series is on self-contained monographs covering particular areas of recent research and surveys of methods, problems, and results in all fields of inquiry where recourse to logical analysis and logical methods has been fruitful. INDICES will contain monographs dealing with the central areas of philosophical logic (extensional and intensional systems, (...) indexical logics, non-classical logics, philosophy of logic, etc.) as well as studies in which these systems are applied to specific issues in philosophy, in the formal semantics of natural languages, the foundations of linguistic theory, in computational linguistics, and in theoretical computer science. Constructive type theory was first presented in 1970, by the Swedish logician Per Martin-Lof. It has become one of the main approaches used in the foundations of mathematics and computer science. But it has remained relatively unknown among linguists and philosophers, although it provides a considerable extension of the concepts and techniques of logic. The book first gives an introduction to type theory from the point of view of linguistics and the philosophy of language. Type theory is then applied in the areas of quantification, anaphora, temporal reference, and the structure of text and discourse. By virtue of the type-theoretical concepts of proof object and context, various phenomena of dependence and progression in language can be discussed in precise terms, and several well-known problems can be solved. A categorial grammar is presented togenerate formally a fragment of English, together with an example of a computer implementation. (shrink)

First-order logic. The origin of modern foundational studies. Frege's system and the paradoxes. The teory of types. Zermelo-Fraenkel set theory. Hilbert's program and Godel's incompleteness theorems. The foundational systems of W.V. Quine. Categorical algebra.

In seiner letzten Schrift unternimmt Husserl den Versuch, auf dem Wege einer teleologisch-historischen Besinnung auf die Ursprünge unserer kritischen wissenschaftlichen und philosophischen Situation die Notwendigkeit einer transzendentalphänomenologischen Umwendung der Philosophie zu begründen. Er geht von seinem Begriff der "Lebenswelt" aus und entwickelt eine auf diesen Zentralbegriff seiner Spätphilosophie gegründete eigenständige Einleitung in die transzendentale Phänomenologie.

Mit den "Ideen zu einer reinen Phänomenologie und phänomenologischen Philosophie" von 1913, von ihm selbst nur als eine "Allgemeine Einführung in die reine Phänomenologie" angezeigt, zog Edmund Husserl die Konsequenz aus seinen Logischen Untersuchungen (PhB 601), die ihn 1900/01 berühmt gemacht hatten: Ausgehend von der dort entwickelten Phänomenologie der intentionalen Erlebnisse sieht er jetzt in der Aufdeckung der Leistungen des "reinen Bewußtseins", dem die uns bekannte natürliche Welt nur als "Bewußtseinskorrelat" gegeben ist, den eigentlichen Gegenstand philosophischer Erkenntnis und in den (...) von ihm eingeführten methodologischen Begriffen der "Reduk tion" und der "Epoché" den Weg, sich über die Beschaffenheit dieses "reinen Bewußtseins", aus dem alle Erkenntnis entspringt, Klarheit zu verschaffen. Die Ausgabe bietet Husserls Schrift text- und seitengleich nach Band III/1 der Husserliana, herausgegeben von Karl Schuhmann; beigegeben sind Husserls Nachwort zu den Ideen von 1930 aus Band V der Husserliana, herausgegeben von Marly Biemel, sowie ein umfangreiches Namen- und Sachregister von Elisabeth Ströker. (shrink)