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

1. 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))
: ??

2. 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?

3. 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

4. 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.

5. 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.

6. 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

7. 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.

8. Re: How to prove this (Ev1)(v1=v1)

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!