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 Reed Mullanix on 2024-11-13 at 18:03

@ncf @jonmsterling AFAIK there is no good introductory textbooks that do this. The options seem to range from neutral to actively harmful.

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

Descendants

Written by chris martens on 2024-11-13 at 18:07

@jonmsterling @totbwf @ncf not a textbook, but maybe https://www.cs.cmu.edu/~fp/courses/15814-f21/lectures/17-natded.pdf does what you’re after?

=> More informations about this toot | More toots from chrisamaphone@hci.social

Written by chris martens on 2024-11-13 at 18:08

@jonmsterling @totbwf @ncf and for the quantifiers: https://www.cs.cmu.edu/~crary/317-f24/lectures/06-quant.pdf

(cc @OscarCunningham )

=> More informations about this toot | More toots from chrisamaphone@hci.social