13
$\begingroup$

Lambek & Scott: Introduction to higher order categorical logic

says that

"For example, categorists may be unhappy when we treat categories as special kinds of deductive systems and logicians may be unhappy when we insist that deductive systems need not be freely generated from axioms and rules of inference"

I am curious about the latter: why a deductive system need not be freely generated from axioms and rules of inference?

In computer science, derivable true formulae are the ones derivable from axioms by a finite series of using inference rules, that is, an inductively defined set.

Why is this doubtful for a category theorist?

Improve this question
$\endgroup$
2
  • 4
    $\begingroup$ Since they treat categories as special kinds of deductive systems, they only mean that not all categories are inductively generated. $\endgroup$
    – François G. Dorais
    Commented Jun 21, 2017 at 14:01
  • 5
    $\begingroup$ This looks like to me: not every category is the syntactic category of a type theory. $\endgroup$
    – user40276
    Commented Jun 21, 2017 at 15:07

2 Answers 2

Reset to default
15
$\begingroup$

This sentence reads to me like "we will treat Xs as if they were special kinds of of Ys, which will make both X-theorists and Y-theorists unhappy because it is not true". Reminds me of the old joke when a patient says "Doctor, it hurts when I do this" and the doctor says "Then don't do that!"

I think a more modern thing to say is that a deductive system describes a sort of algebraic theory, where the axioms and rules of inference are the operations. The inductively defined derivable judgments are the elements of the initial/free algebra for this algebraic theory; whereas there are of course also algebras that are not free. In particular, the deductive system is a theory that is not identified with any of its algebras, either the free ones or the non-free ones. Computer scientists may be most interested in the free algebras, whereas category theorists are interested in all the algebras (although of course the free ones play an important role).

Improve this answer
$\endgroup$
10
  • 2
    $\begingroup$ The computer scientists may even retort that every algebra is free, just some algebras have some non-trivial equivalence relations defined on them (in a free way, of course)... $\endgroup$
    – cody
    Commented Jun 21, 2017 at 19:06
  • 1
    $\begingroup$ Where can I read about free and non-free algebras? $\endgroup$
    – Gergely
    Commented Jun 21, 2017 at 19:06
  • 1
    $\begingroup$ By "deductive system" is it meant the same as "theory" (in the sense of mathematical logic) or something like the system Hilbert-Frege? $\endgroup$
    – Qfwfq
    Commented Jun 21, 2017 at 21:26
  • 2
    $\begingroup$ @cody Your tongue may be in your cheek, but to a mathematician that statement is also false. Every algebra is a quotient of a free algebra, but the free generators are not uniquely determined. There is a "canonical" choice of presentation, but even so algebras cannot be identified with presentations because the categories are different. That sort of thinking leads people to do mathematics with "setoids", which is both technically cumbersome and mathematically misguided. $\endgroup$
    – Mike Shulman
    Commented Jun 22, 2017 at 10:57
  • 1
    $\begingroup$ @MikeShulman IMO, the mathematical reading of setoids is rather natural: they're just Bishop-style sets. This makes it easy to eliminate everything cumbersome about working with setoids: since dependent type theory itself can be interpreted in setoids, you can use that interpretation to move all the setoid manipulation bureaucracy out of the terms and into judgmental equality, without even giving up decidability of typechecking. (This is basically what Altenkirch and McBride's "observational type theory" does.) $\endgroup$
    – Neel Krishnaswami
    Commented Jun 22, 2017 at 15:12
6
$\begingroup$

I think the idea should pretty much like this: once you drop the requirement for the deductive system to be freely generated from the axioms by the inference rules (i.e. you accept the existence of non free deductive systems) you can start to study morphisms from the free deductive systems into not free ones (what Lambek and Scott call functors, if memory serves me well).

In this way you can hopefully prove properties of the free systems by looking to the not free ones. For instance for proving that two proofs (i.e. arrows) are different in a free deductive system you could try to find a nice functor that sends the said proofs in different arrows. Here by nice I mean that such functor sends the proofs in a different system where it is easier to prove the inequality of the two proofs.

As a example (probably a not really interesting one) you can consider the functor that goes from a syntactic-freely generated deductive system to the deductive system $\mathbb N$ (the additive monoid of natural numbers, seen as a category, hence as a deductive system), that sends every object (proposition) to the only object of the one-object category $\mathbb N$ and every morphism/proof to its length (which is indeed a natural number, that is a morphism in $\mathbb N$). This functor allows one to distinguish between two proofs because they have different length.

I suppose that someone with much more knowledge on the subject than me can provide some more interesting examples.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .