Is it admissible in a Fitch proof to use $\to$ introduction that "cuts across" subproofs and doesn't discharge them?

138 Views Asked by At

There is a certain on-line theorem prover the produces Fitch proofs that occasionally look like this:

enter image description here

It uses $\to$ introduction that doesn't seem legit in that it doesn't seem to discharge a whole sub-proof. At least one other on-line Fitch proof checker rejects such proofs.

enter image description here

The latter only accepts "proper" proofs of that discharge full sub-proofs by $\to$ introduction.

(Full proof of the same theorem in the latter -- I'm not inlining it here, as it would a bit distracting; also I used one derived rule [DeM] to cut some "cruft".)

Basically: is such a "trick" of $\to$ introduction that doesn't discharge a full sub-proof admissible/sound in some cases, or is the first software just buggy?

1

There are 1 best solutions below

0
On BEST ANSWER

Summary: You question the validity of this conditional introduction in the proof structure:

$$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{~~\vdots\\~~5.~~\lnot(p\to q)\\\fitch{~~6.~~q}{\fitch{~~7.~~\lnot p}{\fitch{~~8.~~p}{}\\~~9.~~p\to q\qquad{\to}\mathsf I~8{-}6\qquad?\\10.~~\bot}\\11.~~\lnot\lnot p\\12.~~ p}\\13.~~q\to p}$$

Indeed, it is actually valid: Since $q$ is derivable under the assumption of $p$ because it has been derived in an accessible lower context, then you may deduce $p\to q$ after closing the subproof.

The 'trick' is just ensuring that the conclusion of the subproof is where the software expects to find it.   Your first checker accepts that line 6 is accessible in the context starting at line 8.   The open logic proof checker requires the conclusion to be stated inside that context.

When a proof checker is finicky about this, simply use reiteration to explicitly restate that $q$ in the raised context.

$$\fitch{}{~~\vdots\\~~5.~~\lnot(p\to q)\\\fitch{~~6.~~q}{\fitch{~~7.~~\lnot p}{\fitch{~~8.~~p}{~~8.1.~~q\qquad\text{Reiteration}~6}\\~~9.~~p\to q\qquad{\to}\mathsf I~8{-}8.1\\10.~~\bot}\\11.~~\lnot\lnot p\\12.~~p}\\13.~~q\to p}$$