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 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

Descendants

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