Subproof in Fitch style system

Question

When using a Fitch style system for proving various theorems, why are we allowed to assume anything we want in the assumption of a subproof in order to derive some desired result? It seems like there should be some restriction on what you can and cannot assume within a proof. Why is this process logically valid?

Answer 1

In a subproof we assume a formula $\varphi$ whatever (we have no restrictions) and we derive a new formula $\psi$; the "goal" of the subproof is to derive $\psi$ "under assumption" of $\varphi$.

Then we usually apply the $\rightarrow$-introduction rule (or conditional proof) and we derive $\varphi \rightarrow \psi$, "discharging" the assumption $\varphi$.

The $\rightarrow$-introduction rule can be formally stated as :

If we have derived $ψ$ from $\Gamma \cup \{ φ \}$ (i.e. : $Γ \cup \{ φ \} \vdash ψ$), then we can derive $(φ → ψ)$ from $\Gamma$ (i.e. : $\Gamma \vdash φ → ψ$), and we say that we have "discharged" the assumption $φ$ form the set of "active" assumptions.

In conclusion, the subproof gives us a derivation of the conditional statement : $φ → ψ$.

Thus, what is the justification of the subproof "mechanism" ? It is the soundness of the above rule.

In general [see : Neil Tennant, Natural logic (1978), page 71] :

The justification of the classical rules of inference consists in a demonstration that they are truth preserving: given any classical proof, if all its undischarged assumptions are true then its conclusion is true also; that is, the conclusion is a logical consequence of the undischarged assumptions.

We introduce the symbol :

$\Gamma \vDash \varphi$

to say that the formula $\varphi$ ia a logical consequence of the set $\Gamma$ of formulae.

Thus, according to the "strategy" above we are justified in using a proof system by the :

Soundness Theorem : If $\Gamma \vdash \varphi$, then $\Gamma \vDash \varphi$.

Having done this, we have a proof that all its rules are sound, i.e. truth-preserving, $\rightarrow$-introduction included.

Assuming the classical semantics with its truth-functional definition of the logical connectives, we have that the situation described is as follows :

We have a derivation - according to the rules of the system - of $\psi$ from the set of assumptions : $Γ \cup \{ \varphi \}$; i.e. we have :

$Γ \cup \{ \varphi \} \vdash \psi$

and the system is sound; thus $\psi$ is a logical consequence of $Γ \cup \{ \varphi \}$.

Let $\mathcal I$ be any interpretation that is a model of $Γ$ and $\varphi$, i.e. such that $\varphi$ is satisfied by $\mathcal I$ and also, for every formula $\gamma \in \Gamma$, $\gamma$ is satisfied by $\mathcal I$.

Thus, $\mathcal I$ is a model of $Γ$, and we must show that it is also a model of $\varphi → \psi$.

If it is not, then by the truth table for →, we have $\mathcal I(\varphi) = T$ and $\mathcal I(\psi) = F$.

But this is impossible, since $\mathcal I$ is now a model of $Γ \cup \{ \varphi \}$ in which $\psi$ is false, contradicting the fact that $\psi$ is a logical consequence of $Γ \cup \{ \varphi \}$.

---

Note

See also Peter Smith'answer in this post and the useful link in the comment.

Answer 2

"When using a Fitch style system for proving various theorems, why are we allowed to assume anything we want in the assumption of a subproof in order to derive some desired result? "

Because that assumption has scope. You haven't claimed that assumption as a theorem (though you can use theorems as assumptions). You only end up seeing what follows from that assumptions before you discharge the assumption.

The restriction lies in that the assumption has to have some sort of scope. The system won't end up as inconsistent, because you're not claiming that contradictions can't occur within the scope of some assumption or hypothesis. In fact, contradictions can and often enough do occur under the scope of an assumption in such proofs. And even more than that, contradictions can serve as the assumption/hypothesis that you make.

For instance (in Polish notation) one can have the following proof that NCpp $\vdash$ Cpp:

assumption   1 | NCpp
hypothesis   2 || p
C-in    1-2  3 | Cpp

We do have a contradiction here. In fact, we immediately have a contradiction by making the assumption in the first place. But, we haven't claimed that such a contradiction actually gives us any sort of theorem. The contradictory assumption has scope to it.

Or as another example, you can prove the law of the excluded middle ApNp in the following manner:

hypothesis   1 | NApNp
hypothesis   2 || NNp
hypothesis   3 ||| Np
2, 3 K-in    4 ||| KNpNNp
3-4 N-out    5 || p
5 A-in left  6 || ApNp
1, 6 K-in    7 || KApNpNApNp
2-7 N-out    8 | Np
8 A-in right 9 | ApNp
1, 9 K-in   10 | KApNpNApNp
1-10 N-out  11 ApNp

Again, we assumed a contradiction (the negation of a tautology). Then we showed that we could derive a contradiction of the form K$\alpha$N$\alpha$. And since the system I've used here allows us to discharge a hypothesis which is a negation when we derive a contradiction of the form K$\alpha$N$\alpha$ under the same scope as that hypothesis, we can get the theorem ApNp here.

Why is it valid? Well, no truth gets imputed to the assumptions made. Arguments end up as valid if their assumptions or hypotheses are false or unknown.