Natural deduction: True iff not false

[Fredrik]

I'm studying a book on logic, and I'm having difficulties with the book's rules of natural deduction. $P_1,P_2,\dots$ are variables that represent propositions like $x>0$. All variables and the symbols $\top$ and $\bot$ are formulas. For all formulas $\varphi,\psi$, the following strings of text are formulas too:
\begin{align*}
&\varphi\land\psi\\
&\varphi\lor\psi\\
&\varphi\to\psi
\end{align*} Edit: After taking a peak at Enderton, I realize that this isn't quite right. $\top$ and $\bot$ are not formulas. They are expressions, i.e. finite sequences of symbols, but not formulas. Also, it makes more sense to say that $(\varphi\land\psi)$ is a formula than to say that $\varphi\land\psi$ is a formula, because then we don't have to insert parentheses when we combine formulas. Instead, we can introduce a convention for when we can choose not to write out all the parentheses.

Negation and equivalence are defined as abbreviations:
\begin{align*}
&\lnot\varphi=\varphi\to\bot\\
&\varphi\leftrightarrow\psi = (\varphi\to\psi)\land(\psi\to\varphi)
\end{align*} The book defines a bunch of rules. The simplest is the conjunction introduction rule:
$$\frac{\varphi\qquad\psi}{\varphi\land\psi}$$ The complete set of rules can be found on page 40 in the English edition. Link. They are explained (partially) on the pages before that. One of my problems is that the book does a few things that seem to violate the rules. The simplest example is this:
$$\frac{\frac{{}}{\top}}{P_1\to\top}$$ How is this not a violation of the implication introduction rule? It says explicitly that we can conclude that $\varphi\to\psi$ when (and only when) we have a derivation that starts with $\varphi$ and ends with $\psi$?

I thought about viewing the above as an abbreviated notation for
$$\frac{\frac{P_1}{\top}}{P_1\to\top}$$ but that doesn't entirely make sense either, since there's no formula on top of the $\top$ in the $\top$ introduction rule. Maybe I should interpret that one similarly, i.e. as really saying that for all formulas $\varphi$, we have
$$\frac{\varphi}{\top}$$ A bigger problem for me is that I don't understand the book's derivation of $\top\leftrightarrow\lnot\bot$ on page 41. A part of it goes like this:
$$\frac{\frac{[\bot]}{\lnot\bot}}{\top\to\lnot\bot}$$ Where did that $\top$ come from? The book claims that that step is using the implication introduction rule, but if I apply that, I would end up with $\bot\to\lnot\bot$, not $\top\to\lnot\bot$.

Maybe I'm missing something obvious, but I feel like the book didn't explain the rules well enough. For example, there's nothing in the statement of the implication introduction rule that says that assumptions other than the one that's being discharged when the rule is applied can be part of the derivation, and yet we see an example of that on page 41 (example 5.4.3, the $\to I_1$ step). That example helped me understand something about that rule that I couldn't have picked up from the statement of the rule. Maybe I have missed something similar about the other rules.

By the way, is there a better way to LaTeX these derivations than to use \frac?

 

[micromass]

Your book is really lacking some rigor and it is using clumsy (but unfortunately standard) notations. I'm surprised you're using this book since it doesn't really qualify for the level of rigor I'm associating with you.

Anyway:

I thought about viewing the above as an abbreviated notation for
$$\frac{\frac{P_1}{\top}}{P_1\to\top}$$ but that doesn't entirely make sense either, since there's no formula on top of the $\top$ in the $\top$ introduction rule. Maybe I should interpret that one similarly, i.e. as really saying that for all formulas $\varphi$, we have
$$\frac{\varphi}{\top}$$

You should see the derivation rules as minimal conditions for deriving something. So if you see $\frac{}{\top}$ then it means that from the top condition " ... ", we can derive the bottom condition "true". But the top condition "..." is the minimal condition, meaning that adding literally anything else will still give a solid derivation. So $\frac{\psi}{\top}$ is still valid for any $\psi$.

For example, the conjunction introduction rule is
$$\frac{\psi~~\varphi}{\psi\wedge \varphi}$$
Again, the top conditions are $\psi$ and $\varphi$ and they are minimal, so adding another condition still gives a valid derivation, so
$$\frac{\psi~~\varphi~~\neg \psi}{\psi\wedge \varphi}$$
is valid.

Another notation then this fraction notation makes this muuuch clearer.

A bigger problem for me is that I don't understand the book's derivation of $\top\leftrightarrow\lnot\bot$ on page 41. A part of it goes like this:
$$\frac{\frac{[\bot]}{\lnot\bot}}{\top\to\lnot\bot}$$ Where did that $\top$ come from? The book claims that that step is using the implication introduction rule, but if I apply that, I would end up with $\bot\to\lnot\bot$, not $\top\to\lnot\bot$.

I'm not really sure what the brackets in $[\bot]$ are. Is it like an assumption in a proof by contradiction?

 

[micromass]

OK, so checking the notation, I think the proof is wrong. Here is a proof that I think is better. We have
$$\frac{\frac{[\bot]}{\bot}}{\bot\rightarrow \bot = \neg \bot}$$
Thus we get
$$\frac{\frac{[\top]}{\neg \bot}}{\top\rightarrow \neg \bot}$$

 

[Fredrik]

Your book is really lacking some rigor and it is using clumsy (but unfortunately standard) notations. I'm surprised you're using this book since it doesn't really qualify for the level of rigor I'm associating with you.

Haha, yes, I hear you. I have actually signed up for a course that uses it. (Long story...maybe I'll tell you in a PM). Otherwise I would have used a different book from the start, or just skimmed through something like this one to get an overview, and then moved on to a more comprehensive and rigorous book.

You should see the derivation rules as minimal conditions for deriving something. So if you see $\frac{}{\top}$ then it means that from the top condition " ... ", we can derive the bottom condition "true". But the top condition "..." is the minimal condition, meaning that adding literally anything else will still give a solid derivation. So $\frac{\psi}{\top}$ is still valid for any $\psi$.

For example, the conjunction introduction rule is
$$\frac{\psi~~\varphi}{\psi\wedge \varphi}$$
Again, the top conditions are $\psi$ and $\varphi$ and they are minimal, so adding another condition still gives a valid derivation, so
$$\frac{\psi~~\varphi~~\neg \psi}{\psi\wedge \varphi}$$
is valid.

Ahh, that clears up a few things. Thank you.

I'm not really sure what the brackets in $[\bot]$ are. Is it like an assumption in a proof by contradiction?

Most of the rules use only what's on the last line to form a new conclusion. The book calls them rules of inference. But two of the rules (implication introduction and disjunction elimination) use an entire derivation to form a new conclusion. The book calls them rules of deduction. The book says that when one of these rules is used, you need to put brackets around the assumption at the start of the derivation to label it "discharged". For example, to derive $\varphi\land\varphi\to\varphi$, you first write
$$
\frac{\varphi\land\varphi}{\varphi}\ {\scriptstyle \land\, E}
$$ The $\land\, E$ is a note that explains that we're using the conjunction elimination rule. Then when you apply the implication introduction rule, you add
$$\frac{}{\varphi\land\varphi\to\varphi}\ {\scriptstyle \to\, I_1}$$ at the bottom, and change the line at the top from $\varphi\land\varphi$ to $[\varphi\land\varphi]^1$. The subscript on the $I$ and the superscript on the bracket must be the same number, to indicate what assumption is discharged when you use the implication introduction rule.

OK, so checking the notation, I think the proof is wrong. Here is a proof that I think is better. We have
$$\frac{\frac{[\bot]}{\bot}}{\bot\rightarrow \bot = \neg \bot}$$
Thus we get
$$\frac{\frac{[\top]}{\neg \bot}}{\top\rightarrow \neg \bot}$$

OK, I see that the first part derives the formula $\bot\to\bot$, without leaving any assumptions undischarged. Since $\lnot\bot$ is just another notation for $\bot\to\bot$, it also derives $\lnot\bot$ without leaving any assumptions undischarged. But what rule are you using at the start of the second part? Is there a rule that says that we can write
$$\frac{\top}{\varphi}$$ whenever $\varphi$ is a formula that can be derived without leaving any assumptions undischarged?

 

[micromass]

OK, I see that the first part derives the formula $\bot\to\bot$, without leaving any assumptions undischarged. Since $\lnot\bot$ is just another notation for $\bot\to\bot$, it also derives $\lnot\bot$ without leaving any assumptions undischarged. But what rule are you using at the start of the second part? Is there a rule that says that we can write
$$\frac{\top}{\varphi}$$ whenever $\varphi$ is a formula that can be derived without leaving any assumptions undischarged?

Sorry, I made a "mistake". The first part is fine and shows that $\frac{}{\neg \bot}$. So again, since the top is a minimal assumption, we can add some to get $\frac{\top}{\neg \bot}$. So now the second part is fine since this implies $\top\rightarrow \neg \bot$.

 

[Fredrik]

Awsome. I think I understand now. I guess in this book's notation, the derivation of $\top\to\lnot\bot$ should look something like this:
$$\frac{\frac{\frac{[\bot]^1}{\bot}\qquad[\top]^2}{\lnot\bot}{\scriptsize \to\, I_1}}{\top\to\lnot\bot}{\scriptsize \to\, I_2}$$
Edit: I don't know, this looks weird. Is it really OK to say, in the $\to\,I_2$ step, that $\top\to\lnot\bot$, just becuase $\top$ (the one labeled 2) has been included up there, even though it's not involved in the steps that gave us $\lnot\bot$. I guess I still don't fully understand.

If the above is correct, then what if we replace the $\top$ with something silly like $\top\to\bot$? Have we derived $(\top\to\bot)\to\lnot\bot$?

I have to get some sleep in a while, so don't stay up all night working on this.

 

[Fredrik]

Yesterday I had no clue how to approach problem 5.6.1 on page 42, which asks the reader for a complete derivation of $(\lnot\varphi\to\psi)\leftrightarrow(\varphi\lor\psi)$. Today I came up with what you see below. I think I have to ask if it looks OK to you, since I still feel kind of weird about not using all of the formulas above the line to get the formula below the line. This is only half the proof, specifically the $\to$ part. The [...] represents all the details from Example 5.4.3 on page 41, which I didn't feel like typing up. Since the problem asks for a "complete derivation", I think I would have to write it all out on an exam.

$$
\frac
{\displaystyle
\frac
{
[\dots]
}
{
\varphi\lor\lnot\varphi
}
{\scriptsize\text{Ex. 5.4.3}}
\qquad
\frac
{\displaystyle
\frac
{
[\varphi]^3\quad [\lnot\varphi\to\psi]^1
}
{
\varphi\lor\psi
}
{\scriptsize\lor I}
}
{
(\lnot\varphi\to\psi)\to(\varphi\lor\psi)
}
{\scriptsize\to I_1}
\qquad
\frac
{\displaystyle
\frac
{
[\lnot\varphi]^3\quad[\lnot\varphi\to\psi]^2
}
{\displaystyle
\frac
{
\psi
}
{
\varphi\lor\psi
}
{\scriptsize\lor I}
}
{\scriptsize\to E}
}
{
(\lnot\varphi\to\psi)\to(\varphi\lor\psi)
}
{\scriptsize\to I_2}
}
{
(\lnot\varphi\to\psi)\to(\varphi\lor\psi)
} {\scriptsize\lor E_3}
$$ This stuff is a ***** to LaTeX.

I took a peak at Enderton's book, which is actually listed under "Further reading (useful supplements, not required)" on the web page for the course. What he's doing looks extremely different from what this Swedish book is doing. I thought I'd be able to just read Enderton to find out how to do this right, but I can't even tell if it's about the same topic.

I also googled "natural deduction", and it seems that every link I click takes me to a page that's about something different from what all the other sources are talking about. Different rules, different notation,... I'm not getting the impression that there's a consensus about how these things should be done.

 

[micromass]

It does look good, but the notation makes it quite difficult to understand (there's nothing you can do about that of course).

I also googled "natural deduction", and it seems that every link I click takes me to a page that's about something different from what all the other sources are talking about. Different rules, different notation,... I'm not getting the impression that there's a consensus about how these things should be done.

Haha, yes, this is true. Every different logic book has its own different rules and notations. In the end they should all be equivalent though.

 

[verty]

I'll refer you to this resource which should, I hope, be more understandable than the notes you are using.

About what you were writing about, the boxes are for assumptions. If you assume it, place a box around it, then it doesn't need to be true. An example: $[\bot] \over \lnot \bot$.

 

[Fredrik]

I'll refer you to this resource which should, I hope, be more understandable than the notes you are using.

Thanks. That does look useful. It's similar enough to the book I'm using that it should be easy to apply it to the things I have to do.

About what you were writing about, the boxes are for assumptions. If you assume it, place a box around it, then it doesn't need to be true. An example: $[\bot] \over \lnot \bot$.

See the middle part of post #4 for the book's explanation of the boxes. The formulas in boxes are assumptions that have been "discharged" because they've been used to introduce a conditional or eliminate a disjunction.

 

[Anama Skout]

By the way, is there a better way to LaTeX these derivations than to use \frac?

Use \ begin{array}{...} ... \\ \hline ... \end{array}