Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Let $r$ be a ternary relation symbol, $f$ a binary function symbol, and $x,y,z$ distinct variables. Let $F(x,y,z)$ be the formula $x=y \rightarrow (rfxyxz \rightarrow rfyxxz)$.

I need to show the $F$ is valid, by showing that in any interpretation $S$, $F^S(a,b,c)$ holds for any $a,b,c$.

So i know that if $F$ is $t_1(x)=t_2(x)$, then $F^S(a)$ holds iff $(t_1)^S(a)=(t_2)^S(a)$. And if $F$ is $rt_1(x)...t_n(x)$, then $F^S(a)$ holds iff $r^S((t_1)^S(a),...,(t_n)^S(a))$ holds. Not sure how to formally prove the formula though.

share|improve this question

1 Answer 1

"Not sure how to formally prove the formula though." Prove using what resources, exactly?

Standard systems of first-order logic with identity will have a version of Leibniz's Law, that says that

(i) from $x = y$ and $\varphi(x)$ you can infer $\varphi(y)$ and (ii) from $x = y$ and $\varphi(y)$ you can infer $\varphi(x)$ (for any context $\varphi(\cdot)$).

So given $x = y$ and $Rfxyxz$ you can infer $Rfxxxz$ (put $\varphi(\cdot) = Rfx\cdot xz$ and use (ii)). And from $x = y$ and $Rfxxxz$ you can infer $Rfyxxz$ (put $\varphi(\cdot) = Rf\cdot xxz$ and use (i)).

Putting those inferences together with an application of Conditional Proof will give you the proof of the given conditional that you want.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.