I know i can represent that as ~(Av1)~(v1=v1)
A = for all
E= there exist.
Is this on the right track?
: A(v1) initial sequent note the A is a formula
: (Av1)(A(v1))
: ??
Could you say what proof system you are using? See this sticky thread. Is it sequent calculus?
As emakrov said, this depends on what proof system you're using.
In one system, such a proof is simple:
1. Ax x=x ... axiom of identity theory
2. x=x ... universal instantiation
3. Ex x=x ... existential generalization
First, it's not propositional, but first-order calculus since your formulas include an existential quantifier and a binary equality predicate.
Post numbers are locates in the Bali Hai-colored bar above each post. Post #3 is located here.
Of various deductive system that I know, introduction and elimination occur in natural deduction. Usually ND is formulated so that derivations consist of formulas; however, there is also a sequent presentation where all open assumptions are collected in the left-hand side of sequents. In any case, MoeBlee's outline is pretty close.
To have a precise derivation, please provide the rules of universal elimination, existential introduction and describe how equality is incorporated into the system.