Even more loosely: Two facts are non-independent if having a proof of A helps you write a proof of B.
Wouldn’t that be only positive dependence rather than general (non-in)dependence? What about negative dependence? Negative dependence in probabilistic terms: P(A)×P(B)>P(A&B).
It’s impossible for having a proof of A to make it harder to prove B.
Proof(A&B) should not be longer than Proof(A) and Proof(B) put together, since proving A and B separately also proves A&B. (Except maybe you waste a few tokens of syntax to say “therefore A&B” or something.)
Wouldn’t that be only positive dependence rather than general (non-in)dependence? What about negative dependence? Negative dependence in probabilistic terms: P(A)×P(B)>P(A&B).
It’s impossible for having a proof of A to make it harder to prove B.
Proof(A&B) should not be longer than Proof(A) and Proof(B) put together, since proving A and B separately also proves A&B. (Except maybe you waste a few tokens of syntax to say “therefore A&B” or something.)