As suggested by @Mateusz Bagiński it is tempting to suggest that the proper reading of a coproof c of A should be a proof of the double negation ofA , i.e.c is a proof ⊢¬¬A.
The absence of evidence against the negation of A is weaker than a proof ⊢¬¬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⊨¬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⊨¬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 Σ=A1,...,Ak over a classical base logic the space of models is given by “ultrafilters/models/truth assignments” u∈2Σ=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∧B)=u(A)∧u(B) etc).
A subset U⊂M of models can now be interpreted as a coproof of A if for all u∈U,u⊨¬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Σ. This would assigns a proposition A the ratio o(A)=|{u∈M|u⊨A}||{u∈M|u⊨¬A}|.
Rk. Note that similar ideas appear in the van Horn-Cox theorem.
As suggested by @Mateusz Bagiński it is tempting to suggest that the proper reading of a coproof c of A should be a proof of the double negation ofA , i.e.c is a proof ⊢¬¬A.
The absence of evidence against the negation of A is weaker than a proof ⊢¬¬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⊨¬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⊨¬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 Σ=A1,...,Ak over a classical base logic the space of models is given by “ultrafilters/models/truth assignments” u∈2Σ=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∧B)=u(A)∧u(B) etc).
A subset U⊂M of models can now be interpreted as a coproof of A if for all u∈U,u⊨¬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Σ. This would assigns a proposition A the ratio o(A)=|{u∈M|u⊨A}||{u∈M|u⊨¬A}|.
Rk. Note that similar ideas appear in the van Horn-Cox theorem.