Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeNov 20th 2011

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.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJan 20th 2014
• (edited Jan 20th 2014)

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?

• CommentRowNumber3.
• CommentAuthorZhen Lin
• CommentTimeJan 20th 2014

“Classical” in the first column probably means “extensional”.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJan 20th 2014

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.

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeJan 20th 2014

I support removing that line entirely.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJan 20th 2014

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?

• CommentRowNumber7.
• CommentAuthorTodd_Trimble
• CommentTimeJan 20th 2014

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 $(A \multimap B) \otimes A \to B$ of the hom-tensor adjunction. In terms of terms, it refers to the reduction $(\lambda x. \tau[x])(a) \rightsquigarrow \tau [ x/a ]$.

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeJan 20th 2014

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.

• CommentRowNumber9.
• CommentAuthorAli Caglayan
• CommentTimeAug 11th 2018
The table is broken at the moment. I tried a few trivial edits to format it like the other tables but it hasn't seemed to fix it. You can roll back all my edits. This table is used by other articles so it would be good if it can be fixed.
1. Thanks for letting us know, I’ll take a look when I get the chance.

2. Fixed table.

• CommentRowNumber12.
• CommentAuthorRichard Williamson
• CommentTimeAug 12th 2018
• (edited Aug 12th 2018)

I also tweaked the file instiki.css to add a bit of padding to table cells and headings (for all tables in the nLab).

3. I think general consensus amongst type theorists are that setoids/Bishop sets aren’t actually internal 0-groupoids; only the setoids/Bishop sets whose “relations” are (-1)-truncated are internal 0-groupoids. Also “type of type” -> “type universe”

Anonymous

• CommentRowNumber14.
• CommentAuthormaxsnew
• CommentTime2 days ago

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.