--- Day changed Wed Nov 04 2015 | ||

lpaste | “{AS}” pasted “Strengthening.agda” at http://lpaste.net/144562 | 04/11 10:11 |
---|---|---|

{AS} | Hi, is the above theorem not possible to prove in Agda? | 04/11 10:12 |

{AS} | I believe It is obviously true in classic logic, but I don't think it will break anything in intuitionistic logic | 04/11 10:15 |

{AS} | or ignore the latter statement | 04/11 10:16 |

{AS} | I can now see why this does not necessarily hold (since we may still dependent computationally on y) | 04/11 10:19 |

augur | {AS}: its not true in classical logic | 04/11 14:21 |

augur | well. let me rephrase that, because it depends on how you relate proof relevance to proof irrelevance | 04/11 14:23 |

augur | if you mean that "forall x in A, y in B. P x" entails "forall x in A, P x" is true in classical logic, this isn't true because the vacuity of quantifying over B might be important | 04/11 14:24 |

augur | eg if B is empty, then it holds, even tho P x doesnt hold of any x at all | 04/11 14:25 |

augur | on the other hand, since this can be read as implication, A -> B -> C doesnt entail A -> C because C might reference B, eg if C = B | 04/11 14:25 |

augur | A -> B -> B is obviously true, but A -> B is not | 04/11 14:25 |

augur | so it cant be true that for all A, B, and C/P this holds | 04/11 14:26 |

{AS} | augur: but P doesn't depend on y | 04/11 15:14 |

augur | it doesnt need to depend on y, just B | 04/11 15:14 |

{AS} | Ah | 04/11 15:14 |

{AS} | so something like if B was Ø | 04/11 15:15 |

augur | so as i said, if you pick P = \_ -> B, or C = B, then (x : A) -> (y : B) -> P x is provable | 04/11 15:15 |

{AS} | Ah, thanks for the explanation | 04/11 15:15 |

augur | because its (x : A) -> (y : B) -> B | 04/11 15:15 |

{AS} | maybe I should be more explicit I guess :) | 04/11 15:15 |

augur | but (x : A) -> P x wont be | 04/11 15:16 |

augur | but yeah, ultimately it has something to do with the possibility of B being empty | 04/11 15:16 |

augur | well, not ultimately, rather | 04/11 15:16 |

augur | but: in some cases, the emptiness of B makes one provable but not the other | 04/11 15:17 |

{AS} | augur: Thanks :) | 04/11 15:17 |

augur | and also alternatively, the possibility that consequent might in fact be one of the antecedent, but might not be provable without that antecedent | 04/11 15:17 |

{AS} | augur: what if A = B? | 04/11 15:18 |

augur | then in those cases it will be provable, but thats irrelevant | 04/11 15:18 |

augur | if ANY case is false, then the entailment is false | 04/11 15:18 |

{AS} | augur: Thanks (that is the case I have actually) | 04/11 15:18 |

{AS} | I was perhaps overly eagerly generalising my minimal example | 04/11 15:18 |

augur | also yeah, strengthening is not what you wrote, but rather | 04/11 15:19 |

augur | its A -> A -> B entails A -> B | 04/11 15:19 |

augur | and thats easy to prove! | 04/11 15:19 |

augur | \f x -> f x x | 04/11 15:19 |

{AS} | Yeah :) | 04/11 15:19 |

augur | strengthening is about extra proofs not being necessary | 04/11 15:19 |

augur | weakening is about irrelevant proofs not being necessary | 04/11 15:19 |

{AS} | augur: I thought that y : B was an extra proof in this case | 04/11 15:20 |

{AS} | perhaps I should have added the side condition explicitly | 04/11 15:20 |

{AS} | that y or B are not free in P or something like that | 04/11 15:20 |

augur | no, the extra-ness in question is in relation to existing ones | 04/11 15:20 |

augur | like, if i have x : A, then y : A is an extra A | 04/11 15:20 |

augur | in general, strengthening (with proof terms) is written like this: | 04/11 15:21 |

augur | G, x : A, y : A !- M : B ===> G, x : A !- [x/y]M : B | 04/11 15:21 |

augur | or w/o proof terms: G, A, A !- B ===> G, A !- B | 04/11 15:22 |

{AS} | Aha | 04/11 15:22 |

{AS} | what would the property be that G, x : A, y : B |- P x (y and B are not free in P) ==> G, x :A |- P x be called? | 04/11 15:23 |

augur | a falsehoold :) | 04/11 15:25 |

{AS} | augur: Aren't they true when y and B are not free in P? | 04/11 15:26 |

augur | well, if y and B dont appear in P x, i suppose its true actually? | 04/11 15:26 |

{AS} | That is what I am guessing | 04/11 15:26 |

augur | but its a metatheorem of some sort. its a kind of anti-weakening | 04/11 15:26 |

{AS} | That is why I called it strengthening :) | 04/11 15:27 |

augur | it wont be provable within the logic, because you'll need to do some kind of induction over proofs using the fact that y is not used to prove P x anywhere | 04/11 15:27 |

{AS} | A ha | 04/11 15:27 |

augur | strengthening has an established meaning tho :P | 04/11 15:27 |

{AS} | technically one could just show that forall z. [z/y]P = P ? | 04/11 15:28 |

{AS} | in the meta level that is | 04/11 15:28 |

augur | that seems like a roundabout way to do it, i think | 04/11 15:29 |

augur | at the meta-level you're better off just keeping track of the fact that P has such-and-such free vars | 04/11 15:29 |

{AS} | OK | 04/11 15:29 |

{AS} | I have to go, but thanks for the discussion | 04/11 15:30 |

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!