Discussion on answer by Bumble: Can it be proven from pure logic that at least one thing exists?

“we would have to change our rules and make them unnecessarily fiddly for most purposes” — this is a big overstatement. The required change (annotating inference judgements with a context of variables) is a small bit of extra work upfront, but far from making things fiddlier, it simplifies many aspects of the logic down the line. It’s also required anyway for many other generalisations (e.g. multi-sorted logics). Early approaches to free logic certainly added significant complication; but modern treatments really require just a slight, and very natural, tweak.

It seems to me that in order to get step 2, you have assumed a exists already.

@usul is correct. The fault is the conclusion: 3. (∃x)(x = a) existential generalisation. You can't just assert existential import.

@Bumble, I think the point is that a proof that something exists is circular if it depends on assuming that something exists. And this proof does. That doesn't make it wrong, just meaningless. Not that I personally have any objection to assuming that something exists.