Scope of Assumptions in Propositional Logic.

Question

From 11, 12 in the book Logic in Computer Science by M. Ryan and M. Huth:

**

"What we are saying is: let’s make the assumption of ¬q. To do this, we open a box and put ¬q at the top. Then we continue applying other rules as normal, for example to obtain ¬p. But this still depends on the assumption of ¬q, so it goes inside the box. Finally, we are ready to apply →i. It allows us to conclude ¬q → ¬p, but that conclusion no longer depends on the assumption ¬q. Compare this with saying that ‘If you are French, then you are European.’ The truth of this sentence does not depend on whether anybody is French or not. Therefore, we write the conclusion ¬q → ¬p outside the box."

**

My question is about the scope of assumptions in propositional logic and proving techniques. I am not sure I fully understand what this text is trying to say.

How can an assumption only have scope inside the box, but once you finish what you want to prove it is no more part of the assumption box and is accessible universally in the proof? WHY is this possible? Why does it not break things in the proof? This looks too convenient and random.

Secondly, I do not understand the French and European example connection to what is written in this text. If somebody could please connect this example to what the author is actually trying to explain through this.

Answer 1

once you finish what you want to prove it is no more part of the assumption box and is accessible universally in the proof?

This is not what happens. You open a proof box with $\neg q$, and within the proof box $\neg q$ holds. Then you do some reasoning and conclude $\neg p$. Within the proof box, starting at that line, $\neg p$ holds. Once you close the box, neither $\neg q$ nor $\neg p$ is directly accessible: what you are allowed to conclude from the box as a whole is $\neg q \to \neg p$. Because you were able to derive $\neg p$ from the assumption $\neg q$, the implication $\neg q \to \neg p$ holds.

I do not understand the French and European example connection to what is written in this text.

Suppose you start a proof box with the assumption "Let $x$ be French." Then the statement "$x$ is French" holds inside the proof box. By doing some reasoning, you are able to conclude "$x$ is European"; this statement still goes inside the proof box. Then you can draw as a conclusion of the whole proof box that "If $x$ is French, then $x$ is European." However, this does not say that $x$ -- whatever it refers to -- is French! It just says that if $x$ is French, then $x$ is European. In particular, you do not "have access" to the "$x$ is French" that was true inside the proof box.

Answer 2

In the calculus there are different types of rules; some allow us to "discharge" assumptions, like e.g. $\to$-intro; others do not.

The "mechanism" is quite simple: we can made whatever assumption we want, but every "result" we get applying the rules to it will depend on the assumption made.

This "mechanism" is made visible through the box-device : the box is opened with the assumption and all the formula derived by way of rules inside the box are dependent on the assumption.

This means that we have correctly derived them, provided that the assumption holds.

When we use a rule that allows us to discharge assumptions, we step outside the box and the result is no longer dependent on the assumption we have discharged.

---

Consider this simple example :

Assumption : "$n$ is divisible by $4$" (i.e. $n= 4 \times k$, for some $k$)

Here we are assuming an "hypotheses" (it is not true in general that every number is divisible by four).

Then we apply some simple "arithmetical transformations" : $n=(4 \times k)=(2 \times 2 ) \times k= 2 \times (2 \times k) = 2 \times l$.

Thus, we have derived : $n= 2 \times l$, for some $l$, that means : "$n$ is divisible by $2$".

Now we can apply $\to$-intro and conclude with :

"if $n$ is divisible by $4$, then $n$ is divisible by $2$".

What we have done ? we have discharged the initial assumption (closed the box) and proved the general result that holds for every $n$.

Answer 3

I don't find the "box" analogy to be very helpful. Just understand that, in classical logic:

(1) If you assume only that proposition P is true and you are subsequently able to prove that proposition Q is true, then you can conclude P implies Q. Having done so, you can no longer assume that P is true. That is the standard practice in formal proofs.

(2) If you assume only that proposition P is true and are subsequently able to prove that proposition Q is true and that it is false (an contradiction), then you can conclude P is false.

Answer 4

How can an assumption only have scope inside the box, but once you finish what you want to prove it is no more part of the assumption box and is accessible universally in the proof?

Assumptions are raised and discharged.

When you raise an assumption, you open a box (rather, a subproof).   Until you discharge the assumption (close the box) every statement derived is made in the context (aka scope) of that assumption -- they are statements that are asserted to be true if the assumption is true.   If you are using the Fitch system for natural deduction, this us usually highlighted by underlining the assumption to distinguish it from derivations made in its context.

The '$\to$ introduction' rule is one of the rules used to discharge an assumption.   The conditional statement that results is not inside the box -- after all, it is itself basically stating "if this assumption is true, then this conclusion is true too."

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$ $$\fitch{}{~\vdots\\\fitch{\lnot q\qquad \text{Assumption raised for the subproof.}}{~\vdots\qquad\quad\text{Derivations made in the context of the assumption}\\\lnot p\qquad\text{Conclusion reached within the context of the assumption}}\\\lnot q\to\lnot p\quad\text{Conditional statement deduced by the subproof}}$$

$$\fitch{}{~\vdots\\\fitch{\text{Assuming you are French}}{\text{Then your native country is in Europe}\\\text{Thus you are European}}\\\text{If you are French, then you are European}}$$