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

• Jul 5th 2011, 10:18 PM
ikurwae89
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))
: ??
• Jul 6th 2011, 07:13 AM
emakarov
Re: How to prove this (Ev1)(v1=v1)
Could you say what proof system you are using? See this sticky thread. Is it sequent calculus?
• Jul 6th 2011, 02:11 PM
MoeBlee
Re: How to prove this (Ev1)(v1=v1)
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
• Jul 6th 2011, 06:07 PM
ikurwae89
Re: How to prove this (Ev1)(v1=v1)
sorry, i wasn't aware of that. yeah i think its sequent type using rules of inference from peanos first order arithmetic.
• Jul 6th 2011, 06:29 PM
emakarov
Re: How to prove this (Ev1)(v1=v1)
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.
• Jul 7th 2011, 04:50 AM
ikurwae89
Re: How to prove this (Ev1)(v1=v1)
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
• Jul 7th 2011, 05:17 AM
emakarov
Re: How to prove this (Ev1)(v1=v1)
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.
• Jul 7th 2011, 09:11 AM
MoeBlee
Re: How to prove this (Ev1)(v1=v1)
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!