[SuchAnonMuchWow]

Mathematicians already explored exactly what you describe: this is the difference between classical logic and intuitionistic logic:

In classical logic statements can be true in and of themselves even if there as no proof of it, but in intuitionistic logic statements are true only if there is a proof of it: the proof is the cause for the statement to be true.

In intuitionistic logic, things are not as simple as "either there is a cow in the field, or there is none" because as you said, for the knowledge of "a cow is in the field" to be true, you need a proof of it. It brings lots of nuance, for example "there isn't no cow in the field" is a weaker knowledge than "there is a cow in the field".

[ndndjdjdn]

It is a fascinating topic. I spent a few hours on it once. I remember vaguely that the logic is very configurable and you had a lot of choices. Like you choose law of excluded middle or not I think, and things like that depending on your taste or problem. I might be wrong it was 8 years ago and I spent a couple of weeks reading about it.

Also no suprise the rabbit hole came from Haskell where those types (huh) are attracted to this more.foundational theory of computation.