It seems underemphasized that the parsimony of ZFC in the way of ‘types’ (having only one sort called sets) has the following practical and notational virtue: you can get by with a single type of the quantifier , and a … Continue reading
This serial will provide, in many and short installments, created every now and then, provide a new translation into English of, and commentary on, the German original of Bernard Bolzano’s 1837 classic book ‘Wissenschaftslehre’. I omit the front-matter and table … Continue reading
There is a body of results in higher category theory which this expository blog post will present you a toy version of. Not to bias this post too much, and not to slight said body of results (they actually are … Continue reading
In one of his very useful writings, Robert Harper writes the following thoughtful sentence: But the upshot of Gödel’s Theorem is that as soon as we fix the concept of formal proof, it is immediate that it is not an … Continue reading
The following is an illustration of a very widely known, yet not widely-enough-known basic connection between things. Explanations will not be given. They can easily be found, given internet access. This connection gives a structure and systematic explanation for some … Continue reading
One should intentionally take an intensional view on the things one cares about.
If one cares for categories, one should intentionally take an intensional view on them: axioms matter. In particular, associativity is an axiom. But it is excusable that one sometimes forgets that associativity is axiomatic: so many categories are concretizable (and then, … Continue reading