Ancestors

Written by Naïm Camille Favier on 2024-11-13 at 17:55

How do we stop teaching to people that ∀ implies ∃, or that anything exists, or that ∃ x. ⊤ is a theorem of "classical first-order logic"? Should we stop teaching LK/LJ sequent calculus? Are there any textbooks on first-order logic that use type theoretic syntax? @jonmsterling do you have any thoughts on this?

=> More informations about this toot | More toots from ncf@types.pl

Toot

Written by Oscar Cunningham on 2024-11-13 at 18:01

@ncf @jonmsterling I was looking for some notes like this recently and couldn't really find any. I wanted a reference for the deduction rules when the free variables have their types explicitly declared in the context. The best I could find were the notes on categorical logic by Mike Shulman and by Steve Awodey and @andrejbauer.

=> More informations about this toot | More toots from OscarCunningham@mathstodon.xyz

Descendants

Written by Naïm Camille Favier on 2024-11-13 at 18:08

@OscarCunningham Thanks, I'll have a look at those.

=> More informations about this toot | More toots from ncf@types.pl

Written by Andrej Bauer on 2024-11-13 at 22:03

@OscarCunningham @ncf @jonmsterling Bart Jacobs's book Categorical logic and type theory has lots of rules of every kind, and then some.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz