Classical logic does always assume that something exists though.

@NatalieClarius wrong.

@Naim $\exists x (Ax \to Ax) $is valid in Classical FOL, and it requires the universe to be non-empty.

@PW_246 No. It is valid in LK sequent calculus. This is a historical accident, not an intrinsic property of classical first-order logic. Assuming that something exists is just another axiom that has nothing to do with whether excluded middle or choice holds.

@NaïmFavier LK sequent calculus is the sequent calculus of FOL, which is Classical. What are you talking about?

It is a system for classical first-order logic. If you express classical FOL in the language of type theory there is no reason to assume existential import.

@NaïmFavier That goes against every text on Classical Logic ever. If you don’t assume an inhabited universe for every domain of your “Classical” logic, what you really have is a free logic. Just because you have LEM/Choice doesn’t mean you have Classical Logic.

@PW_246 I strongly disagree, but at this point we're disagreeing on the meaning of the word "classical" so this is perhaps pointless. See classical logic.

@NaïmFavier Classical Logic refers exactly to what is described here plato.stanford.edu/entries/logic-classical/#FeatSynt. Note in section 3 that existential intro is valid: “If we have established (or assumed) that a given object $t$ has a given property, then it follows that there is something that has that property. ($∃$I) For any closed term $t$, if $Γ⊢θ(v|t)$ then $Γ⊢∃vθ$.”

Well, it's clear that it refers to that when you use it. It doesn't refer to that when I use it.

@NaïmFavier Just because you call Free Logic with Classical Propositional Logic as the propositional portion “Classical Logic” doesn’t make it so.

Yeah, I'm with PW_246 here in that free logic is not what "classical logic" is typically understood to mean, but of course what you meant is true - perhaps one could have said it isn't valid even in "non-constructive" logics as long as they don't assume a non-empty universe, and everyone is happy.

For modern references that illustrate my point, see Awodey and Bauer's and Michael Shulman's notes on categorical logic. Both talk of classical logic, but neither repeats the historical blunder under discussion.

Someone apparently removed my first comment, so let me repost it: It's not even true classically if you don't assume that anything exists, much less constructively.

@NaïmFavier Regardless of what you call it, if your logic doesn’t have valid existential formulas, it’s not Classical Logic.

"Valid existential formulas"? What are you talking about now?

@NaïmFavier I mean exactly what I said. There are existentials that are true in Classical Logic, like $\exists x (Ax \to Ax)$

You're just stubbornly making the same point again. These are valid in the formal system you have in mind when you say "classical logic", but other people mean other things by that.