Language, Logic and Theories of Meaning
More or less a branch of Against Realism, or maybe vice versa.
- Notes on Martin Lof’s Siena Lectures. An outline for the rationale behind the constructions of intuitionistic logical inference systems, starting from Frege’s theory of meaning and culminating in Martin-Lof style dependent type theory.
- Remarks on Categorical Logic Some thoughts and sketches on presenting a non ad-hoc construction of internal logic to a category.
- The Law of Excluded Middle. Arguments for ditching the law of excluded middle.
- Further comments on Dummett’s comments on Frege. Dummett’s prose is notoriously difficult. Here I organize the main ideas and scrape off some nonessential details that are not relevant to the overall understanding of Frege’s philosophy.
- Equalities in Type Theory. While it appears that this is an article on the various notions of equalities in type theory, it actually clarifies some confusions arising in metaphysics, such as the distinction between claiming $P$ to be true, and uttering $P$, and so on.
Backgrounds on first-order logic (to the compactness theorem) and natural deduction, lambda calculus and basic type theory, Zermelo-Frankel set theory (ordinal, cardinal), and category theory (Yoneda lemma, adjunction, monad, Kan extensions) are assumed.
Philosophy of logic and mathematics, and foundations,
- Andrei Rodin - Axiomatic Method and Category Theory
- Joel David Hamkins - Lectures on the Philosophy of Mathematics
- Gottlob Frege - Complete Works
- Jean-Yves Girard - The Blind Spot
Theories of meaning and proof-theoretic semantics
- Michael Dummett - The Logical Basis of Metaphysics
- Michael Dummett - The Seas of Language
- Michael Dummett - Truth and Other Enigmas
- Christopher Gauker - Words without Meaning
- Martin Loef - Intuitionistic Type Theory (Bibliopolis book)
- Martin Loef - Siena Lectures
- Johan Georg Granstrom - Treatise on Intuitionistic Type Theory
- Sara Negri, Jan von Plato - Structural Proof Theory
- Nissim Francez - Proof-theoretic Semantics
Categorical Logic. While similar in spirit, there are roughly speaking two types of categorical logic: categorical algebra, Curry-Howard-Lambek correspondence. The former is more about universal algebra (algebraic, cartesian, coherent and geometric theories), the latter is more about topoi, cartesian closed categories and their internal logic. Their methods are relevant to foundations of mathematics.
- Colin MacLarty - Elementary Categories, Elementary Toposes
- Bart Jacobs - Categorical Logic and Type Theory
- Paul Taylor - Practical Foundations of Mathematics
- Egbert Rijke - Introduction to Homotopy Type Theory
- William Lawvere’s works