Solution: Proving Existence of x for Logic Formal Proof

[Fumbles22]

Give a formal proof to show $$\forall x (0' + x' ) = (x . 0'') \vdash \exists x (x + x')= (x . x')$$

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) $$\forall x (0' + x' ) = (x . 0'')$$ Assumption
1 (2) $$(0' +x')=(x.0'')$$ Universal Elimination rule
1 (3) $$\exists y (y+x')=(x.y')$$ Existential Introduction, 2
4 (4) $$y=x$$ Assumption
1,4 (5) $$\exists x (x+x')=(x.x')$$ Taut 3,4 <--- ?
1 (6) $$\exists x (x+x')= (x.x')$$ 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?

 

[Evgeny.Makarov]

Welcome to MHB!

First of all, you need to specify the formal system in which you construct proofs. Just like the same thought or algorithm can be expressed in many natural or programming languages, the same formula can be proved in many formalisms. Mathematical logic has many proof systems: Hilbert calculus (which has numerous axiomatizations), natural deduction, sequent calculus, semantic tableau, resolution, and so on. These systems have good mathematical properties are are legitimate objects of study. Besides, many logic textbooks (especially written by philosophers (Evilgrin)) have their own, often ad-hoc proof systems, such as the http://www.doczonline.com/wp-content/uploads/2009/02/Rules-of-Inferenceetc.pdf (PDF) from Introduction to Logic by Irving Copi. In addition, if you need to prove some obvious arithmetical fact, such as 0 ≠ 1 or x + y = y + x, you need to specify arithmetical axioms, such as Peano axioms or ring axioms.

Give a formal proof to show $$\forall x (0' + x' ) = (x . 0'') \vdash \exists x (x + x')= (x . x')$$

This is not provable because there is a counterexample. The soundness theorem for first-order logic says that if $A\vdash B$ for two formulas $A$, $B$, then $M\models A$ implies $M\models B$ for all interpretations $M$. Let $M$ be $\{0,1\}$ where $x'$ is interpreted as $x+1$ and addition and multiplication are modulo 2. Note that this is a model of ring axioms. Then $M\models\forall x\; 0' + x' = x\cdot 0''$, but $M\not\models\exists x\;x + x'=x\cdot x'$.

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.

I did not understand any of these steps until I read the following derivation. First, substituting x for x and turning $\forall x\,P(x)$ into $P(x)$ is legitimate, but suspicious and rarely used (only maybe to derive $(\forall x\,P(x))\to\exists x\,P(x)$, which itself is a suspicious law). It is not clear how you make the statement valid for all y since below you introduce the existential, and not the universal, quantifier. You can't substitute y into 0' because 0' does not have variables. One substitutes an expression E for a variable x into another expression F(x) to produce F(E).

Here's what I did:

1 (1) $$\forall x (0' + x' ) = (x . 0'')$$ Assumption
1 (2) $$(0' +x')=(x.0'')$$ Universal Elimination rule
1 (3) $$\exists y (y+x')=(x.y')$$ Existential Introduction, 2
4 (4) $$y=x$$ Assumption
1,4 (5) $$\exists x (x+x')=(x.x')$$ Taut 3,4 <--- ?
1 (6) $$\exists x (x+x')= (x\cdot x')$$ Existential Hypothesis, 5

Step (3) should be $$\exists y\; (y+x')=(x\cdot y)$$ because 0' is replaced by y. And if you want to use a fact $\exists x\,P(x)$ by considering the $x$ it talks about, you can't make any assumption about this $x$ except that $P(x)$ holds. Here, you can't assume that $y = x$ and derive $$\exists x\; (x+x')=(x\cdot x')$$ from $$\exists y\; (y+x')=(x\cdot y')$$.

Hint: You can use \cdot in LaTeX for multiplication.

 

[Fumbles22]

Welcome to MHB!

First of all, you need to specify the formal system in which you construct proofs. Just like the same thought or algorithm can be expressed in many natural or programming languages, the same formula can be proved in many formalisms. Mathematical logic has many proof systems: Hilbert calculus (which has numerous axiomatizations), natural deduction, sequent calculus, semantic tableau, resolution, and so on. These systems have good mathematical properties are are legitimate objects of study. Besides, many logic textbooks (especially written by philosophers (Evilgrin)) have their own, often ad-hoc proof systems, such as the http://www.doczonline.com/wp-content/uploads/2009/02/Rules-of-Inferenceetc.pdf (PDF) from Introduction to Logic by Irving Copi. In addition, if you need to prove some obvious arithmetical fact, such as 0 ≠ 1 or x + y = y + x, you need to specify arithmetical axioms, such as Peano axioms or ring axioms.

I'm afraid I'm just starting out, so I think some of this information has been removed from my notes in the name of simplicity. This isn't necessarily a bad thing, too much information at the start of a module would be downright confusing.

Although the question does not state it, I think x belongs in "N" (in the notes it isn't actually an N, it's a "curly N"). Any numbers we have are natural ones, $$\cdot$$ corresponds to regular multiplication and ' means "add one" (ie. $$0' = 1$$ etc).

To show you what the question answers look like, i'll post the another question I had to do. Maybe it will look familiar. Oddly, this question is worth 4 marks (so is theoretically harder), while this one is only worth 2.

1). Give a formal proof for $$\forall v ( \neg \phi \leftrightarrow \psi), \forall v \neg \psi \vdash \forall v \phi$$

Here, the first column is the "assumption column" showing what assumptions the line depends on. The second column are the line numbers, the third is the statement and the fourth column states the rule I'm using.

1 (1) $$\forall v (\neg \phi \leftrightarrow \psi)$$ Assumption
2 (2) $$\forall v \neg \psi$$ Assumption
1 (3) $$\neg \phi \leftrightarrow \psi$$ Universal Eliminator 1
2 (4) $$\neg \psi$$ Universal Eliminator 2
1,2 (5) $$\phi$$ Tautology 3,4
1,2 (6) $$\forall v \phi$$ Universal Indicator 5

Does that look like anything you've seen before?

This is not provable because there is a counterexample. The soundness theorem for first-order logic says that if $A\vdash B$ for two formulas $A$, $B$, then $M\models A$ implies $M\models B$ for all interpretations $M$. Let $M$ be $\{0,1\}$ where $x'$ is interpreted as $x+1$ and addition and multiplication are modulo 2. Note that this is a model of ring axioms. Then $M\models\forall x\; 0' + x' = x\cdot 0''$, but $M\not\models\exists x\;x + x'=x\cdot x'$.

I haven't encountered much of this yet.

I did check when I couldn't get the question to work out on the module website. There isn't an errata about it. I might send my tutor an email about it anyway.

I did not understand any of these steps until I read the following derivation. First, substituting x for x and turning $\forall x\,P(x)$ into $P(x)$ is legitimate, but suspicious and rarely used (only maybe to derive $(\forall x\,P(x))\to\exists x\,P(x)$, which itself is a suspicious law). It is not clear how you make the statement valid for all y

But I didn't make it valid for all y. I chose $$y=0'$$, replaced accordingly and put $$\exists y$$. I'm pretty sure this is valid, here's an example from the course notes:

Show that $$\forall x (x+0)=x \vdash \exists x (x+x)=x$$

1 (1) $$\forall x(x+0)=x$$ Assumption
1 (2) $$(0+0)=0$$ Universal Eliminator.1
1 (3) $$\exists x(x+x)=x$$ Existential Introduction 2

In a sense, we've almost used that $$\forall x P(x) \rightarrow \exists x P(x)$$ law you were talking about. In this case, our $$P(x)$$ on line (1) turns into a $$Q(x)$$ on line (3).

In this case they do what I do and replace $$0$$ with $$x$$.

Anyway, in the meantime i'll send a message to my tutor asking whether the question is actually doable.

EDIT: I tried to reply to your PM, but my "score" isn't high enough. I'll reply to it when it hits 5.

 

[Evgeny.Makarov]

Wow. I can't believe I did not see a double prime in

\[\forall x (0' + x' ) = (x . 0'') \vdash \exists x (x + x')= (x . x')\]

and in two other places. I thought it was a single prime. My vision is really going down, and I am not kidding: I wear contact lenses whose diameter is about 2cm.

Basically, you need to instantiate x with 0' in the assumption and then replace all occurrences of 0' back with x using existential introduction. Sorry about the previous misleading reply.

1 (1) $$\forall v (\neg \phi \leftrightarrow \psi)$$ Assumption
2 (2) $$\forall v \neg \psi$$ Assumption
1 (3) $$\neg \phi \leftrightarrow \psi$$ Universal Eliminator 1
2 (4) $$\neg \psi$$ Universal Eliminator 2
1,2 (5) $$\phi$$ Tautology 3,4
1,2 (6) $$\forall v \phi$$ Universal Indicator 5

Does that look like anything you've seen before?

This looks like natural deduction, but it allows propositional reasoning in one step.

 

[Fumbles22]

I managed to do it. Oddly enough, I used the method that the book!

For some reason. I couldn't get it to work yesterday. Today it worked like a charm.

Thanks for your help Makarov.