Co-Proofs

Presumably the result of a coproof is a cotheorem. Which I mention only because, as everybody knows, a comathematician is a device for turning cotheorems into ffee.

A piece of writing advice: even if Too Like The Lightning gave you the idea, The questions the readers have are "what does this idea mean?", "what are some examples?", and "how can I use it?", not "where did the author come up with this idea?" Too Like the Lightning is not illuminating about any of the former questions (i.e. you don't use it as a source of vivid examples), but it takes up nearly half your post.

As suggested by @Mateusz Bagiński [LW · GW] it is tempting to suggest that the proper reading of a coproof $c$ of $A$ should be a proof of the double negation of$A$ , i.e. $c$ is a proof $⊢\neg \neg A$.

The absence of evidence against the negation of $A$ is weaker than a proof $⊢\neg \neg A$ however. The former allows for new evidence to still appear while the latter categorically rejects this possibility on pain of contradiction. 

Coproofs as countermodels

How could absence of evidence be interpreted logically? One way is to interpret it as the provision of a countermodel. That is - a coproof $c$ of $A$ would be a model $m$ such that $m\models \neg A$. 

Currently, the countermodel $m$ prevents a proof of $A$ and the more countermodels we find the more we might hypothesize that in all models $n,n\models \neg A$ and therefore not $A$. On the other hand, we may find new evidence in the future that expands our knowledge database and excludes the would-be countermodel $m$. This would open the way of a proof of $A$ in our new context. 

Coproofs as sets of countermodels

We can go further by defining some natural (probability) distribution on the space of models $M$. 
This is generically a tricky business but given a finite signature of propositional letters $\Sigma =A_1,...,A_k$ over a classical base logic the space of models is given by "ultrafilters/models/truth assignments" $u\in 2^{\Sigma }=M$ which assign $ttrue$ or $ffalse$ to the basic propsitional letters and are extended to compound propositions in the usual manner (i.e. $u(A\wedge B)=u\left(A\right)\wedge u\left(B\right)$ etc).

A subset $U\subset M$ of models can now be interpreted as a coproof of $A$ if for all $u\in U,u\models \neg A$. 

Probability distributions on propositions and distributions on models 

We might want to generalize subsets of models to (generalized) distributions of models. Any distribution $p$ on the set of models $M$ now induces a distribution on the set of propositions. 

In the simple case above we could also make an invocation of the principle of indifference to define a natural uniform distributions $o$ on $M=2^{\Sigma }$. This would assigns a proposition $A$ the ratio $o\left(A\right)=\frac{|\{u\in M|u\models A\}|}{|\{u\in M|u\models \neg A\}|}$. 

Rk. Note that similar ideas appear in the van Horn-Cox theorem.

I don't like use of "proof" to talk about evidence, especially when it's often weak evidence. Why not go with "absence of counterevidence is counterevidence of absence"? Ok, confusing multiple negatives. "Absence of negative evidence makes positive evidence more plausable"? Not great either.

Maybe just forego the whole thing: "absence doesn't prove anything".

Two opposing attributes of data that cause some change in belief:

Positive Evidence / Lack of evidence

Probability-increasing / Probability-decreasing

Then cross the two to make:

Positive Evidence + Probability-increase = Proof

Lack of Evidence + Probability-increase = Co-proof

Positive Evidence + probability-decrease = Disproof/Counterproof (?)

Lack of Evidence + probability-decrease = Co-disproof? (Probably not)

?

Bayesians can do Popperian falsification -- to falsify a hypothesis $H$, all you have to do is find a hypothesis $H^{\prime }$ such that

as discussed in the blog post Closed Worlds and Bayesian Inference.

This would benefit from a diagram or a table.

I think a proof of not-not-X^[1] is more apt to be called "a co-proof of X" (which implies X if you [locally] assume the law of the excluded middle).

While I agree that "co-proofs" as you've described them are interesting, I'm not sure on how useful they are as a concept. While a lack of counter-evidence certainly helps when we want to argue in favor of a hypothesis, if there isn't enough evidence to bring that hypothesis to our attention in the first place, then we're privileging that hypothesis [LW · GW].

To speak to the example you give, while it is true that for any given person, not having an alibi is a co-proof of their involvement in a crime, there are likely vast numbers of people who don't have alibis, so absent additional proof that lets us pick from among those without alibis, the co-proof doesn't really get us anywhere by itself.