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.

We have the axioms:

  1. $\vdash x = y \to (A\to A')$ where $A'$ is the formula which is created by replacing some of the free apperances of $x$ in $A$ by $y$

  2. $\vdash x=x$ for all $x$

We need to prove that:

  1. $\vdash x=y\rightarrow y=x$

  2. $\vdash x=y \rightarrow (y=z \rightarrow x=z)$

  3. If $F$ is a function of arity 1 then: $\vdash x=y \rightarrow (F(x) \rightarrow F(y))$

I can't really figure out how to solve these and I have a test coming up, it would be a real help guys! I thank anyone who tries and helps me :]

share|improve this question
    
Hint for 1): Let $A$ be $y=y$ and $A'$ be $y=x$ and use the first axiom. I'm assuming you have the usual rules for first order predicate logic (without equality) already down. –  Harald Hanche-Olsen Jan 28 '13 at 15:59
    
Thaks! I forgot i could actually choose the A and A' –  Rachel Bernoulli Jan 28 '13 at 16:02
    
(sidenote: 1. is not an axiom, but an axiom scheme) –  Hagen von Eitzen Jan 28 '13 at 16:04
    
Axiom scheme? sorry i Just translated that from Hebrew without any knowledge of its real syntax in English so...thanks anyway I managed to solve them :) –  Rachel Bernoulli Jan 28 '13 at 16:14
add comment

1 Answer 1

up vote 1 down vote accepted

If you want to prove $x= y \implies \phi(x,y)$, apply the axiom scheme with $A : \phi(x,x)$ and $A' : \phi(x,y)$. Then you are left with proving $\phi(x,x)$ which should be straightforward.

For example for $1$, apply the axiom scheme with $A : x = x$ and $A': y = x$ (we only replace the first of the two free occurences of $x$ in $A$). Then, use reflexivity to prove $A$.

share|improve this answer
add comment

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.