# What formal proof systems are capable of proving $\forall x \exists y x = y$ without needing to apply $\forall$-I to $\exists y x = y$?

I am interested in some philosophical questions that depend on whether the open formula $$\exists y x = y$$ is a logical truth. I'm making the assumption that some logical systems are intended, in the sense that conclusions of those logical systems are ones that ought to be philosophically endorsed. On that assumption, I can clarify what I mean by "logical truth." A logical truth is a statement for which there is a proof in a logical system that is intended (in the sense above). Thus, if standard predicate logic is intended, then the following proof shows that $$\exists y x = y$$ is a logical truth:

1. $$x = x$$ (axiom)
2. $$\exists y x = y$$ (1, $$\exists$$-I)

This conclusion is philosophically problematic for me. Since I think that all logical truths ought to be considered metaphysically necessary, this commits me to the conclusion that $$\Box \exists y x = y$$ is a necessary truth, which further leads to the conclusion that $$\Box \forall x \Box \exists y x = y$$ is a a logical truth. Properly understood, this is the sort of radical conclusion philosophers/logicians should avoid. It has the consequence, for example, that there is nothing that could have failed to be something.

So, I want a logical system in which $$\exists y x = y$$ never appears as a line in any proof. But there were reasons why it was needed in standard predicate logic. The primary example is in the question's titled. Usually one must prove $$\exists y x = y$$ "on the way" to proving $$\forall x \exists y x = y$$, which is harmless, philosophically speaking.

• $\exists y(x = y)$ as such is an open sentence that has no truth value, to get one $x$ has to be quantified. The standard convention is to assume that unquantified variables are universally quantified, which makes it as harmless as $\forall x \exists y(x = y)$. I am not sure what $\exists$-I means. – Conifold Dec 20 '18 at 22:08
• Not sure but a Hilbert-type system might be able to satisfy your requirements - and one not based on "generalization rules" but one more strictly adhering to the Hilbert-type system philosophy, i.e. it has axiom schemas like $(\forall x, \forall y, \phi) \rightarrow (\forall x, \phi[y := \tau])$ and $(\forall x, \phi \rightarrow \psi) \rightarrow [(\forall x, \phi) \rightarrow (\forall x, \psi)]$. – Daniel Schepler Dec 20 '18 at 22:26
• I think you may be conflating technical issues in mathematical logic with philosophical issues. Specifically, as part of mathematics, mathematical logic is neutral as regards your metaphysical assumptions. You are making philosophical distinctions between free and bound variables that you need to clarify in mathematical terms. – Rob Arthan Dec 20 '18 at 22:34
• I suspect you will be more successful if you first determine in full what you want your semantics to be, before you go looking for a proof system. Evidently your intended semantics is not the usual semantics of first-order logic, but just randomly looking for a proof system where $\exists y x = y$ does not appear in this proof is probably not going to fit your semantics much better. – Eric Wofsey Dec 21 '18 at 4:42
• But if ∃y(x=y) has no truth value it can not possibly be a logical truth, let alone metaphysically necessary. It is just an unfinished building block for a proposition. I think you have in mind instantiated natural deduction formulas, where x is a name for "generic" individual in a subproof, at the end of which the variable is universally quantified. But a) instantiated formulas do not have the meaning you object to, and b) instantiation subproofs can be rewritten using closed formulas only even in the standard predicate calculus. – Conifold Dec 22 '18 at 0:27

• The existential specialization is basically the universal generalization. I mean you could (in classical logic) just go further and eliminate $\forall$ entirely by reducing it to $\neg\exists\neg$ (which you did as an intermediate step). That would get rid of $\forall$ introduction for sure. – Derek Elkins Dec 21 '18 at 4:08
• @DerekElkins I have a form of $\forall$-intro in my system. It just isn't required in this proof. – Dan Christensen Dec 21 '18 at 4:21
• My point is that $\forall$ introduction isn't required in any proof within a classical logic. (Of course, specific presentations of classical logic may require it but you could always make a slight variant to avoid that.) Arguably, the OP should have a hang-up with either negation or existential specialization too. – Derek Elkins Dec 21 '18 at 4:49