4 ms·
You can think of "A => B" as stating "there is a way of transforming proofs of A into proofs of B". If "A" is false, then there are no proofs of "A", and thus t
by ihm 9y ago
You can think of "A => B" as stating "there is a way of transforming proofs of A into proofs of B". If "A" is false, then there are no proofs of "A", and thus there is trivially a way of transforming proofs of "A" of "B" (since you will never be confronted with a proof of "A"). So a false statement implies anything.
If "B" is true, then there is some proof p of "B". Now here is a way of transforming a proof of "A" into a proof of "B": given a proof q of "A", just return that one proof p. So anything implies a true statement.
- dvt 9y agoThis is actually the best way to understand it. But without some background (Proof Theory 101, The Deductive Theorem, Metalogic 101), I'm sure this sounds like gibberish :) NB: Although you muddy the waters a bit. "A => B" is literally "A proves B". And to see why an inconsistent set implies anything at all, we just need to look at the Principle of Explosion[1] -- which is probably less contentious than material implication. [1] https://en.wikipedia.org/wiki/Principle_of_explosion https://en.wikipedia.org/wiki/Principle_of_explosion
- dvt 9y agoSmall clarification (I wrote my parent post super late last night). Via the Deduction Theorem, we have: ⊢ A -> B => A ⊢ B That's what I mean by "A proves B"
- setr 9y agoI just think of it as P->Q only says something about Q when P is true; no information is given about Q when P is false, so Q can be whatever it wants in that case. And since any value of Q is acceptable, then the statememt holds regardless of Q's value (when P is false). We only have the chance to return false when P is true, because thats the only time P says something about Q (that its true)
- evincarofautumn 9y agoThat’s how I understand it now after a bunch of exposure to type theory and internalising Curry–Howard. But as a programmer my earliest practical way of thinking of it was “How would I use an ‘implies’ operator in programming?” Things like these: (a => b) == (a ? b : true) == !a || b if (a) assert(b); // == assert(a => b); #if !defined(_MSC_VER) || defined(_NATIVE_WCHAR_T_DEFINED) // == #if defined(_MSC_VER) => defined(_NATIVE_WCHAR_T_DEFINED) if (!p || !p->buffer) return 0; // == if (p => !p->buffer) return 0; That is, just talking about truth values, the results of proofs rather than the proofs themselves.
- adrianratnapala 9y agoThis is interesting because, I'm trying to get to grips with where the abstract and the practical meet. But I'm not sure all of your example fit. Your first example if(a) assert(b); really does fit the intuitive idea of implication. The other two just look like cases that happen to have the same boolean structure as implication, but that's not their meaning. For example if(!p || !p->buffer) return 0; Means (roughly) "check if p's buffer exists, which of course requires that p also exists". So there is a kind of implication here, but it goes in the direction p->buffer => p Which is not what you are talking about.
- evincarofautumn 9y agoThe “#if” example seems clear enough to me. We always want to use wchar_t, but if we’re using MSVC, then only if it’s available. The “buffer” example isn’t great, I agree. I just pulled these from random sources in my projects directory by grepping for “not…or”.
- adrianratnapala 9y agoYour "#if" logic sounds perfectly reasonable, but what does it have to do with implication? Except that the boolean test just happens to have the same truth table.