An odd idea from a few days ago:

I watched this video a while back, this is Richard Feynman giving a lecture about discovering laws in physics -

He is talking about laws in physics. (the underlying Philosophy of Science that Feynman describes here is due to Karl Popper)

What Feynman is describing seems fundamentally different from what we do in the formal sciences like math/logic/cs. In the later we usually choose an axiom set that we believe to be right, based on our aesthetics, and then go on to prove other things that are right wrt our axioms.  Only things that are provable are taken to right and things that are right are irrefutably so. The system is inconsistent if we deduce False from the rules that we have. Inconsistent systems are not interesting. All formal methods work like this, in spirit - they keep track of what is right.

In what Feynman is describing, they don’t have a formal notion of right. They have a notion of what is wrong and as long as something cannot be constructively (by experiment) shown to be wrong, they can temporarily accept it to be not-wrong. If you look at this as a formal system, this is one where “what is not wrong yet” is known instead of what is right. Something is not wrong because 1) We don’t know a proof by which we can construct F from it or 2) Given our current inference rules there is no proof for it. But, we may add a new inference rule to the system in the future which may invalidate the belief that something is not wrong. It’s a feels like the opposite of what we do with logics.

Imagine a formal system or a model of computation based on notion like this. We are, in a fundamental sense, giving up the notion of consistency and completeness when we do this. I wonder if there exists a computational model that corresponds to such a “co-logic” of the sort they use in the *real* sciences. Such a system, in spirit, might be able to deal with partially correct data, incorrect assumptions etc. in a natural way. Absolutely correct data (or properties about the data) would be the exception.

(I wonder what this implies for the incompleteness theorem and such. I have been told that the "co-logic" I refer to here is actually co-induction. I see some similarities there, but I am not sure if its exactly that. )

A Tutorial on (Co)Algebras and (Co)Induction - Jacobs, Rutten

A Tutorial on Co-induction and Functional Programming