Natural Deduction (FeedBack)

Question

I am looking for feedback to three proofs (alternatively derivations) that I have constructed. The first is:

Theorem. Injectivity does not imply surjectivity.

Proof: Suppose $\{\phi\} \vdash \theta$. Then according to the soundness theorem we have $\{\phi\} \models \theta$, which is to say that for every valuation $v$, $[[\phi]]_{v}=1 \implies [[\theta]]_{v}=1$. However, consider the following structure $\langle \mathbb{N};; +, \cdot, 1 \rangle$ which gives rise to the following formula $\exists x_{1}(x_{0} \dot{=} f_{2}(f_{1}(\overline{c}_{0},\overline{c}_{0}),x_{1}))$.Now, from this formula we define a function as follows:

$$f:\mathbb{N} \to \mathbb{N}, $$ $$f(x)=2x$$

This function is clearly injective. However it is equally clear that it is not surjective, as there are elements in the range that the function does not map to, more specifically all odd numbers. Thus, we have a case where $[[\{\phi\}]]_{v}=1$ while $[[\{\theta\}]]_{v}=0$, which shows $\{\theta \}$ is not a logical consequence of $\{\phi\}$ ($\{\phi\} \not \models \{\theta\}$). Hence, by the completeness theorem we have $\{\phi\} \not \vdash \theta$, or in more informal terms, the injective property does not imply the surjective property. $\square$

The two other proofs are a bit more complicated to present. As far as I can tell (and believe me I have tried), Math Stack Exchange does not support bussproof, which is a LateX package that enables users to construct proof trees. Furthermore, I haven't been able to simply attach a PDF file of the derivations (again Math Stack Exchange does not support it). As a result, I have decided to post my codes, hoping you (the community) still are willing to provide some feedback.

Answer 1

1. The counterexample to injectivity implying surjectivity is presented in a quite unnecessary laborious way. You will be marked down for obfuscation.

2. The universally quantified wffs at the top of both branches of the first displayed proof shouldn't be at the same level as the existential. Move the existentials down five lines, and then you need to repeat the conclusion of the sub proof. Thus ...

$\quad\quad\quad\quad\quad\quad\varphi\\ \quad\quad\quad\quad\quad\quad\ldots\\ \quad\quad\quad\quad\quad\quad\ldots\\ \quad\quad\exists x\varphi\quad\quad C\\ \quad\quad -----\\ \quad\quad\quad\quad C$

See van Dalen section 2.9, or other texts.

Here's the proof done Fitch-style: Natural Deduction and Identity .

[Yes, it would be good if we could use bussproofs here!]

Answer 2

I have made changes to the derivations - does this look better? Moreover, is the second derivation convincing (or rightly performed)?

Answer 3

I have a new suggestion as to how to correct my mistake in 0.2; namely I introduce an assumption $f(f(x)) \dot{=} f(a)$ as the minor premise while I at the same time derive $f(f(x)) \dot{=} f(a) \to f(x) \dot{=}a$ as the major premise (from injectivity). Then, I use $\exists E$ at the next step to conclude $f(x) \dot{=} a$. From thereon, I use the Idempotence property to arrive at my desired conclusion. Does this sound more reasonable?