Evgeny.Makarov said:
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.
