10
$\begingroup$

In the paper Diagonal Arguments and Cartesian Closed Categories (here), Lawvere presents a fixed-point theorem that generalizes both Cantor's theorem and Gödel's (first) Incompleteness Theorem.

In order to accomplish this, Lawvere sketches briefly how a theory gives rise to a category $C$ with finite products.enter image description here

The description goes on by declaring substitution as the correspondent composition and mentioning other properties.

At first, my question was a reference request where the explicit category above is discussed less briefly, i.e., with more attention to the details.

However, since such a reference seems hard to find, I would like to ask (alternatively) for an explanation about how this category works. This is very vague, to say the least, so let me emphasize some major points:

  1. why the objects have the form $A^n\times 2^m$?
  2. what are the projections $A^n\times 2^m\to 2^m$ and $A^n\times 2^m\to A^n$?
  3. what is an arrow $A^3\to A^2$?
  4. what is an arrow $2^4\to 2^3$?

Although the list above does not explain the category $C$, I believe that if I understand these points then I will be able to do the rest.

Improve this question
$\endgroup$
17
  • 2
    $\begingroup$ Lawvere’s thesis is one possible place to start. $\endgroup$
    – Zhen Lin
    Commented Dec 12, 2020 at 15:36
  • 3
    $\begingroup$ These are known as Lawvere theories. The book Algebraic theories is a good introduction (Chapter 11 specifically covers the concept Lawvere mentions here) and The Category Theoretic Understanding of Universal Algebra is a nice survey paper. Lawvere's thesis is not a particularly accessible starting point. $\endgroup$
    – varkor
    Commented Dec 12, 2020 at 15:45
  • 2
    $\begingroup$ 1. The objects have that form because the category has finite products and is generated by $A$ and $2$. 2. The projections are the ones in the definition of binary products. 3. An arrow $A^3 \to A^2$ is a pair of of arrows $A^3 \to A$, i.e. a pair of (equivalence classes of) terms with 3 variables. 4. An arrow $2^4 \to 2^3$ is a triple of arrows $2^4 \to 2$, i.e. a triple of boolean functions with 4 variables. $\endgroup$
    – Zhen Lin
    Commented Dec 16, 2020 at 23:02
  • 1
    $\begingroup$ Actually, there are more arrows $2^4 \to 2$ than just boolean functions – rather they are (equivalence classes of) predicates with 4 propositional variables. But you get the idea. $\endgroup$
    – Zhen Lin
    Commented Dec 16, 2020 at 23:09
  • 2
    $\begingroup$ I think Zhen is saying with $2$ that the projection is literally the projection from the binary product $A^n\times2^m$ into either its first factor $A^n$ or second factor $2^m$. $\endgroup$
    – Alec Rhea
    Commented Dec 17, 2020 at 1:54

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .