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

: ??

Printable View

- Jul 5th 2011, 09:18 PMikurwae89How 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, 06:13 AMemakarovRe: 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, 01:11 PMMoeBleeRe: 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, 05:07 PMikurwae89Re: 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, 05:29 PMemakarovRe: 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, 03:50 AMikurwae89Re: 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, 04:17 AMemakarovRe: 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, 08:11 AMMoeBleeRe: How to prove this (Ev1)(v1=v1)