diff --git a/bibliography.bib b/bibliography.bib index 5754edb..19e6380 100644 --- a/bibliography.bib +++ b/bibliography.bib @@ -1,128 +1,419 @@ -@InProceedings{martinlof1971hauptsatz, - Title = {Hauptsatz for the intuitionistic theory of iterated - inductive definitions}, - Author = {Martin-L{\"o}f, Per}, - Booktitle = {Proceedings of the 2nd Scandinavian logic symposium}, - Year = 1971, - Editor = {Fenstad, Jan Erik}, - Publisher = {North-Holland}, - Series = {Studies in Logic and the Foundations of Mathematics}, - Volume = {63}, - Pages = {179 -- 216}, -} - -@incollection{Martin-Lof-1972, - Author = {Martin-L{\"o}f, Per}, - Booktitle = {Twenty-five years of constructive type theory ({V}enice, 1995)}, - Mrclass = {03B15 (03F55)}, - Mrnumber = 1686864, - Pages = {127--172}, - Publisher = {Oxford University Press}, - Editor = {Giovanni Sambin and Jan M. Smith}, - Series = {Oxford Logic Guides}, - Title = {An intuitionistic theory of types}, - Volume = 36, - Year = 1998} - -@incollection{Martin-Lof-1973, - Author = {Martin-L{\"o}f, Per}, - Booktitle = {Logic Colloquium '73, Proceedings of the Logic Colloquium}, - Editor = {H.E. Rose and J.C. Shepherdson}, - Mrclass = {02C15 (02D99)}, - Mrnumber = {0387009 (52 \#7856)}, - Mrreviewer = {Horst Luckhardt}, - Pages = {73--118}, - Publisher = {North-Holland}, - Series = {Studies in Logic and the Foundations of Mathematics}, - Title = {An intuitionistic theory of types: predicative part}, - Volume = 80, - Year = 1975} - - -@TechReport{hml75, - author = {Hancock, Peter and Martin-L\"{o}f, Per}, - title = {Syntax and semantics of the language of primitive - recursive functions}, - institution = {University of Stockholm}, - year = 1975, - number = 3, - address = {Stockholm, Sweden} -} - -@incollection{Martin-Lof-1979, - Author = {Martin-L{\"o}f, Per}, - Booktitle = {Logic, Methodology and Philosophy of Science VI, Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover 1979}, - Editor = {L. Jonathan Cohen and Jerzy {Łoś} and Helmut Pfeiffer and Klaus-Peter Podewski}, - Doi = {10.1016/S0049-237X(09)70189-2}, - Mrclass = {03F50 (03B70 03F55 68Q45)}, - Mrnumber = {682410 (85d:03112)}, - Mrreviewer = {B. H. Mayoh}, - Pages = {153--175}, - Publisher = {North-Holland}, - Series = {Studies in Logic and the Foundations of Mathematics}, - Title = {Constructive mathematics and computer programming}, - Url = {http://dx.doi.org/10.1016/S0049-237X(09)70189-2}, - Volume = 104, - Year = 1982} - -@book{martin-lof:bibliopolis, - Author = {Martin-L{\"o}f, Per}, - Isbn = {88-7088-105-9}, - Mrclass = {03B15 (03F50 03F55)}, - Mrnumber = {769301 (86j:03005)}, - Mrreviewer = {M. M. Richter}, - Pages = {iv+91}, - Publisher = {Bibliopolis}, - Series = {Studies in Proof Theory}, - Subtitle = {Notes by Giovanni Sambin}, - Title = {Intuitionistic type theory}, - Volume = {1}, - Year = {1984}} - - -@article{martin2006100, - Author = {Martin-L{\"o}f, Per}, - Journal = {The Computer Journal}, - Number = {3}, - Pages = {345--350}, - Publisher = {BCS}, - Title = {100 years of {Z}ermelo's axiom of choice: what was the problem with it?}, - Volume = {49}, - Year = {2006}} - -@article{martin1996meanings, - title={On the meanings of the logical constants and the justifications of the logical laws}, - author={Martin-L{\"o}f, Per}, - journal={Nordic journal of philosophical logic}, - volume={1}, - number={1}, - pages={11--60}, - year={1996} -} - -@article{martin1987truth, - title={Truth of a proposition, evidence of a judgement, validity of a proof}, - author={Martin-L{\"o}f, Per}, - journal={Synthese}, - pages={407--420}, - year={1987}, - publisher={JSTOR} -} - -@incollection{martin2013verificationism, - title={Verificationism then and now}, - author={Martin-L{\"o}f, Per}, - booktitle={Judgement and the Epistemic Foundation of Logic}, - pages={3--14}, - year={2013}, - publisher={Springer} -} - -@incollection{martin1994analytic, - title={Analytic and synthetic judgements in type theory}, - author={Martin-L{\"o}f, Per}, - booktitle={Kant and contemporary epistemology}, - pages={87--99}, - year={1994}, - publisher={Springer} + +@incollection{martin-lof_intuitionistic_1998, + series = {Oxford {Logic} {Guides}}, + title = {An intuitionistic theory of types}, + volume = {36}, + booktitle = {Twenty-five years of constructive type theory ({Venice}, 1995)}, + publisher = {Oxford University Press}, + author = {Martin-Löf, Per}, + editor = {Sambin, Giovanni and Smith, Jan M.}, + year = {1998}, + mrnumber = {1686864}, + pages = {127--172} +} + +@techreport{hancock_syntax_1975, + address = {Stockholm, Sweden}, + title = {Syntax and semantics of the language of primitive recursive functions}, + number = {3}, + institution = {University of Stockholm}, + author = {Hancock, Peter and Martin-Löf, Per}, + year = {1975} +} + +@incollection{martin-lof_constructive_1982, + series = {Studies in {Logic} and the {Foundations} of {Mathematics}}, + title = {Constructive mathematics and computer programming}, + volume = {104}, + url = {http://dx.doi.org/10.1016/S0049-237X(09)70189-2}, + booktitle = {Logic, {Methodology} and {Philosophy} of {Science} {VI}, {Proceedings} of the {Sixth} {International} {Congress} of {Logic}, {Methodology} and {Philosophy} of {Science}, {Hannover} 1979}, + publisher = {North-Holland}, + author = {Martin-Löf, Per}, + editor = {Cohen, L. Jonathan and Łoś, Jerzy and Pfeiffer, Helmut and Podewski, Klaus-Peter}, + year = {1982}, + doi = {10.1016/S0049-237X(09)70189-2}, + mrnumber = {682410 (85d:03112)}, + pages = {153--175} +} + +@book{martin-lof_intuitionistic_1984, + series = {Studies in {Proof} {Theory}}, + title = {Intuitionistic type theory}, + volume = {1}, + isbn = {88-7088-105-9}, + publisher = {Bibliopolis}, + author = {Martin-Löf, Per}, + year = {1984}, + mrnumber = {769301 (86j:03005)} +} + +@article{martin-lof_meanings_1996, + title = {On the meanings of the logical constants and the justifications of the logical laws}, + volume = {1}, + number = {1}, + journal = {Nordic journal of philosophical logic}, + author = {Martin-Löf, Per}, + year = {1996}, + pages = {11--60} +} + +@article{martin-lof_definition_1966, + title = {The definition of random sequences}, + volume = {9}, + issn = {0019-9958}, + url = {https://www.sciencedirect.com/science/article/pii/S0019995866800189}, + doi = {10.1016/S0019-9958(66)80018-9}, + abstract = {Kolmogorov has defined the conditional complexity of an object y when the object x is already given to us as the minimal length of a binary program which by means of x computes y on a certain asymptotically optimal machine. On the basis of this definition he has proposed to consider those elements of a given large finite population to be random whose complexity is maximal. Almost all elements of the population have a complexity which is close to the maximal value. In this paper it is shown that the random elements as defined by Kolmogorov possess all conceivable statistical properties of randomness. They can equivalently be considered as the elements which withstand a certain universal stochasticity test. The definition is extended to infinite binary sequences and it is shown that the non random sequences form a maximal constructive null set. Finally, the Kollektivs introduced by von Alises obtain a definition which seems to satisfy all intuitive requirements.}, + language = {en}, + number = {6}, + urldate = {2021-05-24}, + journal = {Information and Control}, + author = {Martin-Löf, Per}, + month = dec, + year = {1966}, + pages = {602--619}, +} + +@article{martin-lof_algorithms_1969, + title = {Algorithms and {Randomness}}, + volume = {37}, + issn = {0373-1138}, + url = {https://www.jstor.org/stable/1402117}, + doi = {10.2307/1402117}, + abstract = {La mesure de complexité de Kolmogoroff est employée, premièrement, pour préciser la notion d'une séquence fortuite finie et, deuxièmement, pour donner une nouvelle définition de l'entropie d'un système mécanique statistique.}, + number = {3}, + urldate = {2021-05-24}, + journal = {Revue de l'Institut International de Statistique / Review of the International Statistical Institute}, + author = {Martin-Löf, P.}, + year = {1969}, + note = {Publisher: [International Statistical Institute (ISI), Wiley]}, + pages = {265--272} +} + +@article{martin-lof_notes_1970, + title = {Notes on {Constructive} {Mathematics}}, + journal = {Almqvist \& Wiksell}, + author = {Martin-Löf, Per}, + year = {1970} +} + +@article{martin-lof_theory_1971, + title = {A theory of types (preprint)}, + journal = {Stockholm University}, + author = {Martin-Löf, Per}, + year = {1971} +} + +@article{martin-lof_complexity_1971, + title = {Complexity oscillations in infinite binary sequences}, + volume = {19}, + issn = {1432-2064}, + url = {https://doi.org/10.1007/BF00534110}, + doi = {10.1007/BF00534110}, + language = {en}, + number = {3}, + urldate = {2021-05-24}, + journal = {Zeitschrift für Wahrscheinlichkeitstheorie und Verwandte Gebiete}, + author = {Martin-Löf, Per}, + month = sep, + year = {1971}, + pages = {225--230} +} + +@incollection{martin-lof_hauptsatz_1971, + series = {Proceedings of the {Second} {Scandinavian} {Logic} {Symposium}}, + title = {Hauptsatz for the {Intuitionistic} {Theory} of {Iterated} {Inductive} {Definitions}}, + volume = {63}, + url = {https://www.sciencedirect.com/science/article/pii/S0049237X08708474}, + abstract = {This chapter presents a proof theoretical analysis of the intuitionistic theory of generalized inductive definitions iterated an arbitrary finite number of times. Like the Hilbert type systems of first order predicate logic that are used, the theories of single and iterated generalized inductive definitions formulated do not lend themselves immediately to a proof theoretical analysis. Therefore, the chapter reformulates the axioms expressing the principles of definition and proof by generalized induction as rules of inference similar to those introduced by Gentzen in his system of natural deduction for first order predicate logic. As in Gentzen's case, this reformulation leads to a notable systematization that is already in the case of ordinary inductive definitions, the rules corresponding to the axioms that express the principle of definition by induction appearing as introduction rules for the inductively defined predicates, whereas the axioms that express the principle of proof by induction give rise to the corresponding elimination rules. Moreover, the generalized inductive definitions appear as inductive definitions iterated once and the iterated generalized inductive definitions as inductive definitions iterated twice or more.}, + language = {en}, + urldate = {2021-05-24}, + booktitle = {Studies in {Logic} and the {Foundations} of {Mathematics}}, + publisher = {Elsevier}, + author = {Martin-Löf, Per}, + editor = {Fenstad, J. E.}, + month = jan, + year = {1971}, + doi = {10.1016/S0049-237X(08)70847-4}, + pages = {179--216} +} + +@article{martin-lof_infinite_1972, + title = {Infinite terms and a system of natural deduction}, + volume = {24}, + url = {http://www.numdam.org/item/?id=CM_1972__24_1_93_0}, + language = {fr}, + number = {1}, + urldate = {2021-05-24}, + journal = {Compositio Mathematica}, + author = {Martin-Löf, Per}, + year = {1972}, + pages = {93--103}, +} + +@book{martin-lof_intuitionistic_1972, + title = {An intuitionistic theory of types}, + url = {10.1093/oso/9780198501275.003.0010}, + abstract = {An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis.}, + author = {Martin-Löf, Per}, + year = {1972}, +} + +@article{martin-lof_notion_1974, + title = {The {Notion} of {Redundancy} and {Its} {Use} as a {Quantitative} {Measure} of the {Discrepancy} between a {Statistical} {Hypothesis} and a {Set} of {Observational} {Data} [with {Discussion}]}, + volume = {1}, + issn = {0303-6898}, + url = {https://www.jstor.org/stable/4615544}, + abstract = {It is proposed to supplement the critical level, as used in ordinary significance testing, by a measure of the magnitude of the departure of the observed set of data from the hypothesis to be tested. This measure, which is called the redundancy, appears in two versions, one microcanonical (or combinatorial) and the other canonical (or parametrical). The microcanomical redundancy is obtained by dividing minus the logarithm of the critical level by the Boltzmann entropy of the experiment and the canonical redundancy by dividing minus the logarithm of the likelihood ratio by the Gibbsian entropy. An approximation theorem shows that the former may be approximated asymptotically by the latter. The problem of calibrating the redundancy scale is discussed in connection with a series of examples, and, finally, certain considerations concerning the size of a statistical experiment are given which are based on the redundancy rather than the power function.}, + number = {1}, + urldate = {2021-05-24}, + journal = {Scandinavian Journal of Statistics}, + author = {Martin-Löf, Per}, + year = {1974}, + note = {Publisher: [Board of the Foundation of the Scandinavian Journal of Statistics, Wiley]}, + pages = {3--18} +} + +@incollection{martin-lof_intuitionistic_1975, + series = {Logic {Colloquium} '73}, + title = {An {Intuitionistic} {Theory} of {Types}: {Predicative} {Part}}, + volume = {80}, + shorttitle = {An {Intuitionistic} {Theory} of {Types}}, + url = {https://www.sciencedirect.com/science/article/pii/S0049237X08719451}, + abstract = {The theory of types is intended to be a full-scale system for formalizing intuitionistic mathematics as developed. The language of the theory is richer than the languages of traditional intuitionistic systems in permitting proofs to appear as parts of propositions so that the propositions of the theory can express properties of proofs. There are axioms for universes that link the generation of objects and types and play somewhat the same role for the present theory as does the replacement axiom for Zermelo–Fraenkel set theory. The present theory is based on a strongly impredicative axiom that there is a type of all types in symbols. This axiom has to be abandoned, however, after it has been shown to lead to a contraction. This chapter discusses Normalization theorem, which can be strengthened in two ways: it can be made to cover open terms and it can be proved that every reduction sequence starting from an arbitrary term leads to a unique normal term after a finite number of steps. The definition of the notion of convertibility and the proof that an arbitrary term is convertible can no longer be separated because the type symbols and the terms are generated simultaneously.}, + language = {en}, + urldate = {2021-05-24}, + booktitle = {Studies in {Logic} and the {Foundations} of {Mathematics}}, + publisher = {Elsevier}, + author = {Martin-Löf, Per}, + editor = {Rose, H. E. and Shepherdson, J. C.}, + month = jan, + year = {1975}, + doi = {10.1016/S0049-237X(08)71945-1}, + pages = {73--118} +} + +@incollection{martin-lof_about_1975, + series = {Proceedings of the {Third} {Scandinavian} {Logic} {Symposium}}, + title = {About {Models} for {Intuitionistic} {Type} {Theories} and the {Notion} of {Definitional} {Equality}}, + volume = {82}, + url = {https://www.sciencedirect.com/science/article/pii/S0049237X08707274}, + abstract = {This chapter is devoted to the formulation of the most natural notion of model for intuitionistic theories that either are type theories by their very definition or may be viewed as such because of the correspondence between formulae and type symbols. The chapter analyzes the notion of definitional equality and its formal counterpart, convertibility, and advocates a change in the current definition of convertibility for systems in which explicit definitions are represented by means of lambda abstraction rather than the introduction of constants or the special constants called combinators. Because of the correspondence between lambda terms and natural deductions, this change is equally called for in Prawitz's definition of convertibility for natural deductions. The chapter also outlines that the transition to intuitionistic abstractions on the metalevel is essential and nontrivial; essential, because they are the most fruitful notion of model, the interpretation of the convertibility relation conv, is standard, that is, it is interpreted as definitional equality in the model, and definitional equality is a notion that is unmentionable within the classical set theoretic framework.}, + language = {en}, + urldate = {2021-05-24}, + booktitle = {Studies in {Logic} and the {Foundations} of {Mathematics}}, + publisher = {Elsevier}, + author = {Martin-Löf, Per}, + editor = {Kanger, Stig}, + month = jan, + year = {1975}, + doi = {10.1016/S0049-237X(08)70727-4}, + pages = {81--109} +} + +@article{martin-lof_reply_1975, + title = {Reply to {Sverdrup}'s {Polemical} {Article} {Tests} without {Power}}, + volume = {2}, + issn = {0303-6898}, + url = {https://www.jstor.org/stable/4615598}, + number = {3}, + urldate = {2021-05-24}, + journal = {Scandinavian Journal of Statistics}, + author = {Martin-Löf, Per}, + year = {1975}, + note = {Publisher: [Board of the Foundation of the Scandinavian Journal of Statistics, Wiley]}, + pages = {161--165} +} + +@article{martin-lof_sensereference_2001, + title = {The {Sense}/{Reference} {Distinction} in {Constructive} {Semantics}}, + language = {en}, + author = {Martin-Löf, Per}, + year = {2001}, + pages = {18}, +} + +@misc{martin-lof_note_1976, + title = {A note to {Michael} {Dummett}}, + author = {Martin-Löf, Per}, + year = {1976} +} + +@article{martin-lof_exact_1977, + title = {Exact tests, confidence regions and estimates}, + volume = {36}, + issn = {1573-0964}, + url = {https://doi.org/10.1007/BF00486113}, + doi = {10.1007/BF00486113}, + abstract = {This paper proposes a uniform method for constructing tests, confidence regions and point estimates which is called exact since it reduces to Fisher's so-called exact test in the case of the hypothesis of independence in a 2 × 2 contingency table. All the wellknown standard tests based on exact sampling distributions are instances of the exact test in its general form. The likelihood ratio and x2 tests as well as the maximum likelihood estimate appears as asymptotic approximations to the corresponding exact procedures.}, + language = {en}, + number = {2}, + urldate = {2021-05-24}, + journal = {Synthese}, + author = {Martin-Löf, P.}, + month = oct, + year = {1977}, + pages = {195--206} +} + +@inproceedings{martin-lof_lecture_1983, + title = {Lecture notes on the domain interpretation of type theory}, + booktitle = {Workshop on {Semantics} of {Programming} {Languages}, {Chalmers}}, + author = {Martin-Löf, Per}, + year = {1983} +} + +@inproceedings{martin-lof_logic_1987, + title = {The logic of judgements}, + booktitle = {Workshop on {General} {Logic}, {Laboratory} for {Foundations} of {Computer} {Science}, {University} of {Edinburgh}}, + author = {Martin-Löf, Per}, + year = {1987} +} + +@article{martin-lof_truth_1987, + title = {Truth of a {Proposition}, {Evidence} of a {Judgement}, {Validity} of a {Proof}}, + volume = {73}, + issn = {0039-7857}, + url = {https://www.jstor.org/stable/20116466}, + number = {3}, + urldate = {2021-05-24}, + journal = {Synthese}, + author = {Martin-Löf, Per}, + year = {1987}, + note = {Publisher: Springer}, + pages = {407--420} +} + +@article{martin-lof_philosophical_1987, + title = {Philosophical implications of type theory}, + journal = {Lectures given at the Facoltá de Lettere e Filosofia, Universitá degli Studi di Firenze, Florence, March}, + author = {Martin-Löf, P}, + year = {1987} +} + +@inproceedings{martin-lof_mathematics_1990, + address = {Berlin, Heidelberg}, + series = {Lecture {Notes} in {Computer} {Science}}, + title = {Mathematics of infinity}, + isbn = {978-3-540-46963-6}, + doi = {10.1007/3-540-52335-9_54}, + language = {en}, + booktitle = {{COLOG}-88}, + publisher = {Springer}, + author = {Martin-Löf, Per}, + editor = {Martin-Löf, Per and Mints, Grigori}, + year = {1990}, + pages = {146--197} +} + +@inproceedings{martin-lof_path_1991, + title = {A path from logic to metaphysics}, + volume = {2}, + booktitle = {Atti del {Congresso} {Nuovi} problemi della logica e della filosofia della scienza}, + author = {Martin-Löf, Per}, + year = {1991}, + pages = {141--149} +} + +@article{martin-lof_substitution_1992, + title = {Substitution calculus}, + journal = {Notes from a lecture given in Göteborg}, + author = {Martin-Löf, Per}, + year = {1992}, + pages = {141} +} + +@article{martin-lof_truth_1998, + title = {Truth and knowability: {On} the principles {C} and {K} of {Michael} {Dummett}}, + journal = {Truth in mathematics}, + author = {Martin-Löf, Per}, + year = {1998}, + note = {Publisher: Oxford: Clarendon Press}, + pages = {105--114} +} + +@incollection{parrini_analytic_1994, + address = {Dordrecht}, + title = {Analytic and {Synthetic} {Judgements} in {Type} {Theory}}, + isbn = {978-94-010-4359-5 978-94-011-0834-8}, + url = {http://link.springer.com/10.1007/978-94-011-0834-8_5}, + urldate = {2021-05-24}, + booktitle = {Kant and {Contemporary} {Epistemology}}, + publisher = {Springer Netherlands}, + author = {Martin-Löf, Per}, + editor = {Parrini, Paolo}, + year = {1994}, + doi = {10.1007/978-94-011-0834-8_5}, + pages = {87--99} +} + +@misc{martin-lof_are_2003, + title = {Are the objects of propositional attitudes propositions in the sense of propositional and predicate logic?}, + author = {Martin-Löf, Per}, + year = {2003} +} + +@article{martin-lof_normalization_2004, + title = {Normalization by evaluation and by the method of computability}, + journal = {Talk at JAIST, Japan Advanced Institute of Science and Technology, Kanazawa}, + author = {Martin-Löf, Per}, + year = {2004} +} + +@incollection{martin-lof_hilbert-brouwer_2008, + address = {Basel}, + series = {Publications des {Archives} {Henri} {Poincaré} / {Publications} of the {Henri} {Poincaré} {Archives}}, + title = {The {Hilbert}-{Brouwer} controversy resolved?}, + isbn = {978-3-7643-8653-5}, + url = {https://doi.org/10.1007/978-3-7643-8653-5_15}, + abstract = {Since this lecture is called the Beth lecture, It is natural to ask oneself what connection is there between Beth and intuitionism? and, to my mind, the most obvious answer is: the Beth models for intuitionistic propositional and predicate logic. I would like to remind you of a certain picture that we all use when thinking in terms of possible worlds, namely the picture in which we are always at a certain stage, considering a number of possible future alternatives, and then one of those alternatives is realized and we get to a new stage, at which we are faced with some other alternatives, one of those alternatives materializes, and then the whole process continues in the same way. That means that, at each moment, we are at the end of a certain path, which I will draw by a thick line, symbolizing that which has already materialized, and we are considering all possible future alternatives, one of those alternatives materializes, as a result of which the thick path gets extended, and then the pattern repeats itself: Open image in new window We all think in terms of this picture: it underlies possible world semantics, and it is natural to ask: where does it really come from? I mean: who had this picture for the first time? Most of us have probably met it in connection with Kripke semantics (Kripke 1965), but actually Kripke semantics was predated by Beth semantics by a couple of years: Beth’ papers were published in 1956 and 1959 (Beth 1956a, 1959), and Beth in turn drew on Brouwer here, because he took the nodes, or stages, to form a spread in Brouwer’s sense (Brouwer 1918B).}, + language = {en}, + urldate = {2021-05-24}, + booktitle = {One {Hundred} {Years} of {Intuitionism} (1907–2007): {The} {Cerisy} {Conference}}, + publisher = {Birkhäuser}, + author = {Martin-Löf, Per}, + editor = {van Atten, Mark and Boldini, Pascal and Bourdeau, Michel and Heinzmann, Gerhard}, + year = {2008}, + doi = {10.1007/978-3-7643-8653-5_15}, + pages = {243--256} +} + +@incollection{martin-lof_verificationism_2013, + address = {Dordrecht}, + series = {Logic, {Epistemology}, and the {Unity} of {Science}}, + title = {Verificationism {Then} and {Now}}, + isbn = {978-94-007-5137-8}, + url = {https://doi.org/10.1007/978-94-007-5137-8_1}, + abstract = {The term verificationism is used in two different ways: the first is in relation to the verification principle of meaning, which we usually and rightly associate with the logical empiricists, although, as we now know, it derives in reality from Wittgenstein, and the second is in relation to the theory of meaning for intuitionistic logic that has been developed, beginning of course with Brouwer, Heyting and Kolmogorov in the 1920s and early 1930s but in much more detail lately, particularly in connection with intuitionistic type theory. It is therefore very natural to ask how these two forms of verificationism are related to one another: was the verificationism that we had in the 1930s a kind of forerunner of what we have now, or was it something entirely different? I would like to discuss this question by considering a very particular problem, which was at the heart of Schlick’s interests, namely, the problem whether there might exist undecidable propositions or, if you prefer, unsolvable problems or unanswerable questions: it is merely a matter of wording which of these terms you choose. As I said, it is a problem which was at the heart of Schlick’s interests: it is explicitly discussed already in his early, programmatic paper Die Wende in der Philosophie in the first volume of Erkenntnis from 1930, and there is a short later paper, which has precisely Unanswerable Questions? as its title, from 1935, and he discussed it on several occasions in between also.}, + language = {en}, + urldate = {2021-05-24}, + booktitle = {Judgement and the {Epistemic} {Foundation} of {Logic}}, + publisher = {Springer Netherlands}, + author = {Martin-Löf, Per}, + editor = {van der Schaar, Maria}, + year = {2013}, + doi = {10.1007/978-94-007-5137-8_1}, + pages = {3--14} +} + +@misc{martin-lof_making_2014, + title = {Making sense of normalization by evaluation}, + abstract = {(Talk given at a workshop on Type theory and formalization of mathematics in Gothenburg, December 11th)}, + author = {Martin-Löf, Per}, + year = {2014} +} + +@article{martin-lof_100_2006, + title = {100 years of {Zermelo}'s axiom of choice: what was the problem with it?}, + volume = {49}, + issn = {1460-2067}, + shorttitle = {100 years of {Zermelo}'s axiom of choice}, + doi = {10.1093/comjnl/bxh162}, + number = {3}, + journal = {The Computer Journal}, + author = {Martin-Löf, Per}, + month = may, + year = {2006}, + note = {Conference Name: The Computer Journal}, + pages = {345--350} }