- Thread starter
- #1

Give a formal proof to show [tex] \forall x (0' + x' ) = (x . 0'') \vdash \exists x (x + x')= (x . x')[/tex]

I'm new to these, and this one looks like it should be easy.

What I want to do is:

1). substitute x into where there are already x's.

2). Make the statement valid for all y

3). substitute y into 0' and y' into 0''.

3). Since it's valid for all y, choose y to be 0.

Here's what I did:

1 (1) [tex] \forall x (0' + x' ) = (x . 0'')[/tex] Assumption

1 (2) [tex](0' +x')=(x.0'')[/tex] Universal Elimination rule

1 (3) [tex]\exists y (y+x')=(x.y') [/tex] Existential Introduction, 2

4 (4) [tex] y=x [/tex] Assumption

1,4 (5) [tex] \exists x (x+x')=(x.x') [/tex] Taut 3,4 <--- ?

1 (6) [tex] \exists x (x+x')= (x.x') [/tex] Existential Hypothesis, 5

I think i've got the right idea, I think the execution starts to go wrong at around line (4).

Does anyone have any ideas?

I'm new to these, and this one looks like it should be easy.

What I want to do is:

1). substitute x into where there are already x's.

2). Make the statement valid for all y

3). substitute y into 0' and y' into 0''.

3). Since it's valid for all y, choose y to be 0.

Here's what I did:

1 (1) [tex] \forall x (0' + x' ) = (x . 0'')[/tex] Assumption

1 (2) [tex](0' +x')=(x.0'')[/tex] Universal Elimination rule

1 (3) [tex]\exists y (y+x')=(x.y') [/tex] Existential Introduction, 2

4 (4) [tex] y=x [/tex] Assumption

1,4 (5) [tex] \exists x (x+x')=(x.x') [/tex] Taut 3,4 <--- ?

1 (6) [tex] \exists x (x+x')= (x.x') [/tex] Existential Hypothesis, 5

I think i've got the right idea, I think the execution starts to go wrong at around line (4).

Does anyone have any ideas?

Last edited: