Is there a logic of sufficiency? Or goals?

Question

This question has been substantially rewritten. Thank you to Peter Smith for pointing out some issues in the original. I hope this version is less ambiguous.

---

In classical logic, one may argue as follows.

Assume $\alpha$ and $\neg \beta$.

---

...

$\gamma \wedge \neg \gamma$ [Where $\gamma$ represents some well-formed formula].

$\therefore \alpha \rightarrow \beta$.

Although this is a very powerful method of proof, one drawback is that it undermines visualizability. For instance, suppose we're trying to prove that a relation $<$ is transitive. We may argue according to the above blueprint as follows.

Assume $(x<y \;\wedge\; y<z)$ and $\neg(x < z)$.

---

...

$\gamma,$ and not $\gamma$.

$\therefore (x<y \;\wedge\; y<z) \;\rightarrow\; x < z$.

The problem is, its impossible to visualize the situation entailed by our assumptions (that's proof by contradiction for you). So a better way of structuring such the argument would probably leverage the notion of sufficiency, basically the idea that we have a goal statement. Here's an example.

Assume $(x<y \;\wedge\; y<z),$ and assume our goal is $(x < z)$. [In other words, it suffices to show $(x<z)$.]

---

...

$\gamma,$ and it is suffices to show $\gamma$.

$\therefore (x<y \;\wedge\; y<z) \;\rightarrow\; x < z$.

We got the same conclusion in the end; but, notice that this time around, we're perfectly capable of visualizing the situation entailed by our assumptions. So this proof is, in some sense, better than the previous one. This begs the question: can goal statements be formalized? In other words, is there a logic of sufficiency?

Reference request. Is there such a thing as 'sufficiency logic' or 'goal logic' which formalizes the above argument?

---

Discussion.

To mean that 'it is our goal to prove $\beta$', or equivalently 'it suffices to prove $\beta$', lets write $-\beta$. Then the general form of the argument I'd like formalized is as follows.

Assume $\alpha$ and $-\beta$.

---

...

$\gamma,$ $-\gamma$

$\therefore \alpha \rightarrow \beta$.

Now the problem with trying to formalize this argument is that the concept of sufficiency has no semantics. For instance, with respect to any given model, a sentence $\beta$ may be true or false, but the statement 'our goal is to show $\beta$' is neither. So $-\beta$ has no truthvalue. Nonetheless, it clearly has inference rules. For instance, the following pattern of argumentation probably wouldn't raise any eyebrows:

Since

• $\alpha \rightarrow \beta$ and

• it is our goal to prove $\beta$

thus

• it suffices to prove $\alpha$.

If we accept this pattern of argumentation, then this suggests an inference rule for the sufficiency operator. Namely $$\alpha \rightarrow \beta, -\beta \vdash -\alpha.$$

Here's another pattern of argumentation probably wouldn't raise any eyebrows.

Since

• it is our goal to prove $\alpha \vee \beta$

thus

• it suffices to prove $\beta$.

This suggests the inference rule

$$-(\alpha \vee \beta) \vdash -\alpha$$

Notice that, if we substituted negation for the occurrences of the sufficiency operator in the two inference rules described so far, we'd get admissible inference rules of classical logic. Namely

$$\alpha \rightarrow \beta, \neg\beta \vdash \neg\alpha,\qquad \neg(\alpha \vee \beta) \vdash \neg\beta$$

This suggests that sufficiency is somewhat similar to negation. Indeed, if we tried to construct a truth-table for it, we'd probably just come up with the truthtable for negation! However, as I've tried to emphasize, the suffiency operator is not truth-functional, and formulae of the form $-\beta$ have no semantics.

This means, for example, that $\alpha \vee (-\beta)$ probably isn't a well-formed formula, because $\vee$ expects truth-values for inputs, but $-\beta$ has no truthvalue. So while $-(\alpha \vee \beta)$ is well-formed, probably $\alpha \vee (-\beta)$ is not. Similarly, I suppose that $-(-\beta)$ is ill-formed. So there cannot be double sufficiency elimination or anything like that!

Answer 1

"It suffices to show ..." is surely some kind of modality. Let's write $\bigcirc$ for it. What rules of inference should we use for $\bigcirc$? To answer that question we need to specify the conditions for soundness. I think this is what is intended:

The sequent $\Gamma \vdash \bigcirc \varphi$ is valid if and only if there exists $\psi$ such that both $\Gamma, \varphi \vdash \psi$ and $\Gamma \vdash \bigcirc \psi$ are valid.

The above criterion is inductive, so we should introduce a base case:

The sequent $\Gamma \vdash \bigcirc \varphi$ is valid if $\bigcirc \varphi$ appears in $\Gamma$.

Also, if we believe ex falso quodlibet, then we should also add $\bigcirc \bot$ as an axiom, to deal with the case where no formulae of the form $\bigcirc \varphi$ appears on the LHS of $\vdash$.

Unfortunately, the above is not enough to guarantee that $\bigcirc$ does what it should. For instance, if we add the axiom $\bigcirc \top$, then $\Gamma \vdash \bigcirc \varphi$ for all $\varphi$! (Take $\psi = \top$ in the first condition.) More generally, for any fixed $\chi$, taking $\bigcirc \varphi \equiv (\varphi \to \chi)$ and assuming $\bigcirc \chi$ as an axiom yields a unary operator $\bigcirc$ that satisfies the above conditions.

In particular, $\bigcirc \varphi \equiv (\varphi \to \bot) \equiv \lnot \varphi$ works if we accept $\bigcirc \bot$ as an axiom. In some sense this is not surprising. For the fragment of intuitionistic propositional logic with $\bot$ and $\lor$, if we want to prove $\varphi$, then it suffices to prove any $\psi$ which is below $\varphi$ in the associated Lindenbaum–Tarski algebra, but these are precisely the $\psi$ which become falsehoods when $\varphi \mathrel{\dashv \vdash} \bot$ is added as an axiom. This is not true for larger fragments of intuitionistic propositional logic because of interactions with the other logical connectives, but I think this observation still has some explanatory power.

Answer 2

1. 'Suffices to prove' what? There is surely no absolute notion here: what suffices in a context is entirely context relative. So what, more carefully, is the notion in play here?

2. And however you slice the pie, is 'it suffices to prove that it suffices to prove A' equivalent to 'A'? Surely not! Hence 'it suffices to prove that' doesn't behave formally like [classical] negation.