Proof of $x=y \rightarrow [P(x) \rightarrow P(y)]$

I'm having a hard time with the proof $$x=y \rightarrow [P(x) \rightarrow P(y)]$$. I know that the generic steps are: (1) Given $$x=y$$. (2) Assume $$P(x)$$. (3) Since $$x=y$$ and $$P(x)$$, then, $$P(y)$$. Nevertheless, I would like a more detailed explanation on step 3. How can we infer that $$P(y)$$ derives from $$x=y$$ and $$P(x)$$, if this is exactly what we're trying to prove beforehand? As it is formulated, it seems like a self-refered proof.

All my attempts to overcome this apparent self-reference have failed. If, for example, we interpret $$P(x)$$ as logically equivalent to some truth set $$X=\{x_0, x_1... x_n\}$$, then $$P(x)$$ would mean $$x\in\{x_0, x_1... x_n\}$$, which is the same as $$x=x_0 \lor x=x_1 \lor \ldots x=x_n$$. Since $$x=y$$, then $$y=x_0 \lor y=x_1 \lor \ldots y=x_n$$, which is $$P(y)$$. However, this last inference also applies the implication $$x=y \rightarrow [P(x) \rightarrow P(y)]$$.

• What rules are you allowed to use? Dec 1 '21 at 19:02
• "First-order logic" does not refer to a unique proof system. There are many proof systems for first-order logic. Most include the substitution axiom for equality (see axiom 3 here), which has $x = y\rightarrow [P(x)\rightarrow P(y)]$ as an instance! If your proof system does not include this axiom, you need to tell us what your proof system is before it's possible to answer the question... Dec 1 '21 at 20:08
• To put it another way: In most systems for first-order logic, your formula is built into the logic itself as a basic feature of $=$. Dec 1 '21 at 20:20
• @TylerD007 If the formula is an axiom in the logic, then it has a one-line proof which is just "write down the formula". This is as good a proof as any other. For an example of a natural deduction system in which the formula is not an axiom, see the natural deduction system given here: leanprover.github.io/logic_and_proof/… Would you like to see a proof in this system? Dec 1 '21 at 20:33
• @Shaun "LL" stands for Leibniz law, in particular for OP's question, it's the first part The indiscernibility of identicals. Dec 2 '21 at 23:21

As an example, I use the natural deduction system for first-order logic defined here: https://leanprover.github.io/logic_and_proof/index.html

See Section 3 "Natural Deduction for Propositional Logic", and Section 8 "Natural Deduction for First Order Logic".

Here is the proof: $$\dfrac{\dfrac{\dfrac{\dfrac{}{x=y}1 \quad \dfrac{}{P(x)}2}{P(y)}\mathsf{sub}}{P(x)\to P(y)}2\to I}{(x=y)\to (P(x)\to P(y))}1\to I$$

• Apparently, this system treats the substitution rule as a natural deduction rule for equalities (see topic 8.4). So, since the rule is handled as a given in the system, the proof would follow the same one-line pattern as you previously described, isn't it? Back to my original question, what really intrigues me is if there is a possibility of infering $P(y)$ from $x=y$ and $P(x)$ without any given axiom (using plain natural deduction). Dec 1 '21 at 20:40
• Well, it's not "one line", it's a proof tree with four levels. But yes, I agree that it's built into the logic. Your question continues to be underspecified until you explain what you mean by "plain natural deduction". The system laid out in my link, including the substitution rule, is an extremely standard natural deduction system for first-order logic. Dec 1 '21 at 20:42
• I use the expression natural deduction as a synonym to a formal logic system that does not resort to any axiom. The goal of the proof must derive exclusively from the givens that we assume at the beggining of the proof. Dec 1 '21 at 20:47
• @TylerD007 Well, talking about provability "regardless of the logic system we use" just doesn't make any sense. What's provable always depends on the details of the logic system, there's no such thing as "provability without rules and axioms" because the rules and axioms define what counts as a proof! And once you fix a logic system, there's no difference between the sentences which are provable for trivial reasons (because they're axioms or immediate consequences of rules) and those with more complicated proofs. Dec 1 '21 at 22:29
• Last comment here: If you want to prove anything about formulas with the $=$ sign in them, you're going to have to have rules / axioms that deal with the $=$ sign. From the point of view of provability, the meaning of $=$ is determined by these rules. There's just no other way for it to happen. Dec 1 '21 at 22:31

How can we infer that $$P(y)$$ derives from $$x=y$$ and $$P(x)$$, if this is exactly what we're trying to prove beforehand? As it is formulated, it seems like a self-refered proof.

You are asking why it is that if $$P(x)$$ and $$x=y$$, then $$P(y)$$. Well, let's think about it: Suppose I tell you that Bob is 6 feet tall. I am also telling you that Bob is the brother of Jim. What can you now infer? That the brother of Jim is 6 feet tall.

In general: if I know that $$x$$ has some property, and I also know that $$x$$ and $$y$$ are the same object, then $$y$$ has that same property. Really, that's all there is to it. If you question that, I really don't know what to say. But any rational person would agree to the truth of that, and the rule simply formalizes it.

In fact, there is an even deeper 'circularity' here: How do you prove $$P \to Q$$? Well, you assume $$P$$, and then infer $$Q$$. So, you effectively show that 'if $$P$$ then $$Q$$' in order to show that $$P \to Q$$

However, despite appearances, this is not circular. Remember that a proof system is really just a purely syntactical system: it derives certain symbols strings from other symbol strings. Of course, the symbol strings can be given a semantics, and it is in that sense that the proofs are actually proofs about something. The basic idea of a formal proof, then, is to purely formalize a proof that, in some sense, already semantically exists. Indeed, most of the times that you make a formal proof, you already have a semantical/informal proof: the formal proof is to put that proof in a special language. That's the 'circularity' that you are perceiving.

You should really read 'What the Tortoise said to Achilles'. In it, the Tortoise is, like you, asking why some elementary inference would be the case. And, yes, trying to argue for it requires logic itself, so that seems circular, and if you insist to spell out the logic in terms of more logic, you do indeed end up in an infinite circular regression. But again, all that formal logic does is to formalize an elementary principle that reflects how we think and talk about the world.

• If one day tag FAQs become a thing, I nominate this Answer for inclusion. Dec 2 '21 at 17:29
• Like I said in my original post, the only way to prove the statement is to establish $P(x)$ equivalent to something, such that $x=y$ and $P(x)$ implies $P(y)$. We know that $P(x)$ is equivalent to $\forall y[x=y \rightarrow P(y)]$, but this equivalence already makes use of the substitution rule we're trying to prove beforehand. Dec 2 '21 at 22:36
• @TylerD007 Oh! Now I see what you’re trying to get at. Ok, but that is not how the proof goes. In the proof you first assume $x=y$, and then assume $P(x)$. Then you apply = Elim to get $P(y)$. Now you discharge $P(x)$ to get $P(x) \to P(y)$. Finally, discharge $x=y$ to get $x=y \to (P(x) \to P(y))$. So note: the ‘$P(x)$’ that the = Elim is applied to is just that: $P(x)$ Dec 3 '21 at 1:01
• Equality elimination tells us that for any predicate $P$, $P(x)$ and $x=y$ implies $P(y)$ (intrologic.stanford.edu/extras/equality.html). But that is exactly what we're trying to prove. In other words, what I wish is an explanation on why equality elimination is a valid rule of inference, i.e. how can we prove that $P(x) \land x=y \rightarrow P(y)$ is a tautology. Dec 3 '21 at 13:07
• @TylerD007 You are asking why it is that if $P(x)$ and $x=y$, then $P(y)$. Well, let's think about it: Suppose I tell you that Bob is 6 feet tall. I am also telling you that Bob is the brother of Jim. What can you now infer? That the brother of Jim is 6 feet tall. In general: if I know that $x$ has some property, and I also know that $x$ and $y$ are really just the same object, then $y$ has that same property. Really, that's all there is to it. If you question that, I really don't know what to say. But any rational person would agree to the truth of that, and the rule simply formalizes it. Dec 3 '21 at 17:37