How to prove this (Ev1)(v1=v1)

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

sorry, i wasn't aware of that. yeah i think its sequent type using rules of inference from peanos first order arithmetic.

I am not sure what sequent type is. PA does not specify the rules of inference; it is a set of axioms. In any case, this is something very trivial and similar to post #3.

its propositional calculus where you start with an initial sequent and then use rules of inference such as introduction, elimination etc to deduce theorems. I have no idea what post 3 is

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.

Quote:

---

Originally Posted by emakarov

Post numbers are locates in the Bali Hai-colored bar above each post.

---

Now THAT'S specific (and color self-referential too!)! Nicely done, emakarov... Bali Hai and talley-ho!