2

In my experience, textbooks and introductory material on type theory (or constructive logic systems) are remarkably devoid of metaphor. I never found any introductory text in those fields that proceeded in a way similar to other areas of logic, based on set theory, where you can choose to introduce the subject "intuitively" (metaphorically), and gradually advance towards more abstract and drier approaches.

My question is if this is an essential linguistic feature of the treatment of type theory in texts (in other words, the imperviousness to metaphor is an epistemological issue), or if it is just a preferable, recomendable, theoretical strategy.

Improve this question
2
  • Russell gives some interesting "concrete" analogies in his treatment, doesn't he? (The barber of the regiment, for instance, shaves everyone who doesn't shave themselves -- so who shaves the barber?) – Joseph Weissman♦ May 5 '15 at 20:35
  • That story is related to the paradox he encountered while working on his "Principia Mathematica". It impacted the Frege's treatise on the foundations of arithmetic, showing that his axioms produced inconsistencies. Type theory was proposed by Russell to avoid such pitfalls, but my question focuses on more recent literature. – André Souza Lemos May 5 '15 at 22:47
1

I doubt this is something essential to type theory per se; but more due to the pervasive mode of mathematical and scientific writing; the art of exposition, I think has been gradually lost.

Lagrange for example prided himself that his mathematical works had no diagrams. Vladimir Arnold had complained about an excessive Bourbakiste approach to mathematics that instead of clarifying the main ideas and sign-posting significance rather hid everything under a thick encrustation of formalism; most of which hid that little of any additional significance was being said.

Certain type theories are related to certain categories - for example the simply typed lambda calculus to closed Cartesian categories and some of these can be presented more naturally as string diagrams; and these can be understood topologically in a natural way.

I'd argue this is a kind of diagrammatic analogy.

In Set Theory, elements and sets are basic; and the notion of a function is derived; Topos Theory takes sets and functions (ie objects and morphisms) as basic; and elements as derived: Lawvere said he wanted to do set theory without elements.

This isn't quite a metaphor, or even an analogy but it works quite well in the way it turns Set Theory 'on its head'; rather like how Marxism as economic philosophy turned Hegel 'on his head'. One might call it a slogan; perhaps even a'mission statement'.

Improve this answer
5
  • Yes, the connection between type theory and category theory allows us to express ourselves using diagrams of objects and arrows, but these are not conceptual metaphors, at least not in this context. – André Souza Lemos May 6 '15 at 22:55
  • I do believe that mathematical thinking is in general relatable to conceptual metaphors (I follow George Lakoff and Rafael Núñez on that assumption: en.wikipedia.org/wiki/Where_Mathematics_Comes_From), but I would like to know if constructive logic could be an exception. Even if that's the case, I strongly believe that the subject has always been presented in an excessively dogmatic style, even by authors that allegedly write for beginners. – André Souza Lemos May 6 '15 at 22:55
  • Sure diagrams aren't metaphors; but they're at times a better arrangement of information that allows for better understanding. – Mozibur Ullah May 7 '15 at 13:11
  • The string diagrams that I mentioned above aren't the same as the usual category-theoretic diagrams; have a look at this; actually I recall seeing a very brief description of linear logic by the metaphor of a menu in a French restaurant; that's probably more appropriate to your question. – Mozibur Ullah May 7 '15 at 13:15
  • 1
    It maybe because constructive logic is going against mainstream classical logic; that the style of writing becomes dogmatic; plus there's fewer people working with it so the general ideas being not widely understood and relied on have to be explicated time and again; for example every mathematician 'knows' set theory without knowing ZFC; you can go very far just using the metaphor of Venn Diagrams. – Mozibur Ullah May 7 '15 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.