Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created types and logic - table and all the entries to complete it.
Currently I am using this to include inside type theory - contents, which I keep reorganizing.
have added two more lines related to linear logic to the “trinitarianism dictionary” types and logic - table
Looking at this again now, I see that I have a complaint about one line in the table, I forget where this originates from, but the 5th line reads:
| logic | category theory | type theory |
|---|---|---|
| classical type theory | internal logic | classical type theory, logic programming |
That doesn’t make sense to me. What’s the interntion here? Could we clarify this?
“Classical” in the first column probably means “extensional”.
Okay, maybe that was the intention. In this case however I vote for removing that line, because this seems to make a distinction too fine-grained for the table. Later the table talks about object classifiers, after all.
I support removing that line entirely.
Thanks for the feedback, Todd! I am removing it now. We still can (and probably should) add more of what seems missing.
By the way, there is another line which I don’t understand (or not anymore, I forget what happens. I believe that I created the bulk of this table, but others edited it, too):
namely the line which under “logic” has “cut elimination” under “category theory” says “counit”. This at least needs more qualification, I’d think: counit of what?
Actually, I’m not too keen on that line either, but it refers to a specific instance of cut-elimination that is related to the counit of the hom-tensor adjunction. In terms of terms, it refers to the reduction .
Okay, I edited in what I said in #7, and filled in for a question mark. Having done that, I think these would probably read a little more nicely if instead of having the left-hand column written in the language of sequent calculus, we write it instead in the language of natural deduction (with introduction and elimination rules). But I’m not very fussed about it.
I don’t really like the line with proof net in it – it seems slightly confused to me, or needs qualification of some kind or another. Let me think on it.
Thanks for letting us know, I’ll take a look when I get the chance.
I also tweaked the file instiki.css to add a bit of padding to table cells and headings (for all tables in the nLab).
I think there are some rows in this table that are fundamentally wrong. For instance “cut elimination for implication” in logic is identified with the counit of the hom-tensor adjunction, but the counit instead corresponds most closely to the left rule for implication (even more directly the elimination rule in natural deduction). The third thing, beta-reduction does roughly correspond to the cut elimination for implication.
Then in the next line, it identifies the introduction rule for implication with the unit of the hom-tensor adjunction, which is arguably correct but then this is identified with eta-conversion which doesn’t really make any sense.
I think the right analogy would be
intro rule for implication : counit : lambda elim rule for implication : unit : application cut elimination for implication : one of the zigzag identities : beta reduction identity elimination for implication : the other zigzag identity : eta conversion
Where identity elimination is the less well known procedure where you show that the identity rule A |- A is admissible if you only assume it for base types. For instance A -> B |- A -> B is admissible by the term f : A -> B |- lambda x. f x : A -> B and the fact that this is an identity is the eta rule.
1 to 15 of 15