Ancestors

Toot

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

Descendants

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

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

Written by Tito on 2024-11-13 at 18:03

@ncf @jonmsterling What do you mean by "type-theoretic syntax"? I think you just need to annotate sequents by their free variables right?

=> More informations about this toot | More toots from tito@sciences.re

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

@tito Fair, but that kind of discipline is already some kind of type theory in my mind.

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

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

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

Written by companion_cube on 2024-11-13 at 23:43

@ncf

Is classical first-order logic bad now? Why not teach both?

@jonmsterling

=> More informations about this toot | More toots from c_cube@octodon.social

Written by Jon Sterling on 2024-11-13 at 23:45

@c_cube @ncf The issue is that this kind of “theorem” should not even be true in classical FOL, but is an accident of the fact that old school logicians (1) never conceived the possibility of empty sorts, and (2) do not understand variables.

Classical FOL is good. Teaching Forall=>Exists is malpractice.

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

Written by companion_cube on 2024-11-13 at 23:55

@jonmsterling

Ah, fair enough. I suppose it's a good theorem if you're using untyped FOL (90s style) but with types it's a bit more dicey (or, at least, opinionated). Although all ATPs I know of just assume sorts are not empty, iirc so they can use skolemization.

@ncf

=> More informations about this toot | More toots from c_cube@octodon.social

Written by Jon Sterling on 2024-11-13 at 23:59

@c_cube @ncf Yes… It is one of those things that could make sense as an admissible rule, depending on what sorts you have, but which cannot be derived in a way that respects variable scope. The usual “proofs” are just invalid in this sense — but these invalid proofs fail to cause problems because the sorts are interpreted by nonempty sets.

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