--- Day changed Wed Nov 04 2015
lpaste“{AS}” pasted “Strengthening.agda” at http://lpaste.net/14456204/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 logic04/11 10:15
{AS}or ignore the latter statement04/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 logic04/11 14:21
augurwell. let me rephrase that, because it depends on how you relate proof relevance to proof irrelevance04/11 14:23
augurif 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 important04/11 14:24
augureg if B is empty, then it holds, even tho P x doesnt hold of any x at all04/11 14:25
auguron 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 = B04/11 14:25
augurA -> B -> B   is obviously true, but   A -> B is not04/11 14:25
augurso it cant be true that for all A, B, and C/P this holds04/11 14:26
{AS}augur: but P doesn't depend on y04/11 15:14
augurit doesnt need to depend on y, just B04/11 15:14
{AS}Ah04/11 15:14
{AS}so something like if B was Ø 04/11 15:15
augurso as i said, if you pick P = \_ -> B, or C = B, then  (x : A) -> (y : B) -> P x   is provable04/11 15:15
{AS}Ah, thanks for the explanation04/11 15:15
augurbecause its  (x : A) -> (y : B) -> B04/11 15:15
{AS}maybe I should be more explicit I guess :)04/11 15:15
augurbut (x : A) -> P x  wont be04/11 15:16
augurbut yeah, ultimately it has something to do with the possibility of B being empty04/11 15:16
augurwell, not ultimately, rather04/11 15:16
augurbut: in some cases, the emptiness of B makes one provable but not the other04/11 15:17
{AS}augur: Thanks :)04/11 15:17
augurand also alternatively, the possibility that consequent might in fact be one of the antecedent, but might not be provable without that antecedent04/11 15:17
{AS}augur: what if A = B?04/11 15:18
augurthen in those cases it will be provable, but thats irrelevant04/11 15:18
augurif ANY case is false, then the entailment is false04/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 example04/11 15:18
auguralso yeah, strengthening is not what you wrote, but rather04/11 15:19
augurits   A -> A -> B   entails   A -> B04/11 15:19
augurand thats easy to prove!04/11 15:19
augur\f x -> f x x04/11 15:19
{AS}Yeah :)04/11 15:19
augurstrengthening is about extra proofs not being necessary04/11 15:19
augurweakening is about irrelevant proofs not being necessary04/11 15:19
{AS}augur: I thought that y : B was an extra proof in this case04/11 15:20
{AS}perhaps I should have added the side condition explicitly04/11 15:20
{AS}that y or B are not free in P or something like that04/11 15:20
augurno, the extra-ness in question is in relation to existing ones04/11 15:20
augurlike, if i have x : A, then y : A is an extra A04/11 15:20
augurin general, strengthening (with proof terms) is written like this:04/11 15:21
augurG, x : A, y : A !- M : B   ===>   G, x : A !- [x/y]M : B04/11 15:21
auguror w/o proof terms:   G, A, A !- B   ===>   G, A !- B04/11 15:22
{AS}Aha04/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
augura falsehoold :)04/11 15:25
{AS}augur: Aren't they true when y and B are not free in P?04/11 15:26
augurwell, if y and B dont appear in P x, i suppose its true actually?04/11 15:26
{AS}That is what I am guessing04/11 15:26
augurbut its a metatheorem of some sort. its a kind of anti-weakening04/11 15:26
{AS}That is why I called it strengthening :)04/11 15:27
augurit 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 anywhere04/11 15:27
{AS}A ha04/11 15:27
augurstrengthening has an established meaning tho :P04/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 is04/11 15:28
augurthat seems like a roundabout way to do it, i think04/11 15:29
augurat the meta-level you're better off just keeping track of the fact that P has such-and-such free vars04/11 15:29
{AS}OK04/11 15:29
{AS}I have to go, but thanks for the discussion04/11 15:30

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