Advertising
- contraction in LK, free variable
- 2012 year 6 month 9 day Saturday 11:37:08 MDT
- irc://irc.freenode.net/##logic
- Day changed to 26 May 2012
- 18:53 < dgpratt> there is something about this that I find troubling: http://i.imgur.com/wqL8a.png
- 18:54 < neophyte> sometimes i hate the responses people give to math questions on reddit.
- 18:54 < dgpratt> namely what happens with
- 18:54 < dgpratt> (r)
- 19:32 < matthewt> http://www.ee.surrey.ac.uk/Projects/Labview/minimisation/graphics/karintro1.gif aren't b and c mixed up on the second diagram
- 19:34 < Saizan> matthewt: yep, or they have some weird way to label the sides
- 19:35 < matthewt> okay thanks
- 19:35 < ski> dgpratt : it assumes non-empty domain -- otherwise i think it's fine
- 19:36 < ski> dgpratt : the `forall'-right application is ok since `x' isn't mentioned (freely) in any other assumption or conclusion
- 19:37 < ski> i think i've figured out how the proof works, computationally, as well
- 19:39 < ski> `x' is really a locally assumed constant here (dicharged by the `forall'-right rule). the only globally assumed inhabitant is `y'
- 19:51 < Saizan> maybe we should make a version of the sequent calculus where the antecedent keeps track of local variables too
- 19:53 < matthewt> sorry for the ignorance dgpratt, but what you pasted is an example of 'resolution' isn't it? in FOL?
- 19:55 < ski> Saizan : i've seen something like `Gamma |-_Chi Delta' used, with `Chi' a typing environment
- 19:56 < Saizan> ski: ah, probably better
- 19:56 < Saizan> matthewt: it's a sequent calculus proof
- 19:57 < ski> in LK, i think
- 19:57 < matthewt> oh, okay
- 19:57 < ski> Saizan : it fits nicer with the categorical view of the rules
- 19:59 < matthewt> Saizan: is it related to resolution somehow?
- 20:03 < ski> <http://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK>
- 20:04 < ski> i think the cut rule is related to resolution
- 20:51 < dgpratt> ski: ok, thanks, I shall take your word for it :)
- 20:54 < dgpratt> sometimes when trying to understand these things, I try to substitute 'real' things into the statement(s)
- 20:55 < dgpratt> as this case demonstrates, I am finding that strategy has limited use
- 20:56 < dgpratt> I suppose it's probably because I know too much about the 'real' things
- 21:36 < ski> dgpratt : i think one "problem" with the derivation is that it is inherently classical (nonconstructive)
- 21:39 < ski> dgpratt : should i explain my informal computational understanding of it ?
- 23:01 < dgpratt> ski: I can't promise I'll fully comprehend it, but I'd appreciate any effort to explain it, yes
- 23:04 < ski> well, first, the top three sequents have both `x' and `y' as free variables
- 23:04 < ski> the rest of the them (*including* the last two ones) has only `y' as free variable
- 23:05 < ski> so, the final sequent is claiming that given an `y' in the domain, `exists x. (P(x) -> (forall y. P(y)))' is true
- 23:05 < ski> (it is not true if the domain is empty)
- 23:06 < ski> so, the reasoning is more or less as :
- 23:07 < ski> assume that someone in a computer game is claiming to have proven the final sequent (we assume the domain is non-empty for this argument)
- 23:07 < ski> so, they're claiming there is an `x' in the domain, and they are claiming a certain implication holds
- 23:08 < ski> but you're a skeptical fellow, you don't just trust the word of this other one, you want to test it
- 23:08 < ski> so, you need to try to manufacture a proof of `P(x)'
- 23:08 < ski> (where `P' is some pre-agreed predicate)
- 23:09 < ski> but you don't know what `x' is
- 23:09 < ski> maybe you fail at this first step, because you can't find a proof of `P(x)'
- 23:09 < ski> (and if `P(x)' *is* false, then the implication is trivially/vacuously true, so then the proof was sound)
- 23:10 < ski> but maybe you can figure out a proof of `P(x)' -- e.g. if you happen to know that `forall x. P(x)' is true
- 23:10 < ski> (then `P(x)' must be true for the mysterious `x' which you don't know yet)
- 23:10 < ski> so far, so good
- 23:11 < ski> you've produced a proof of `P(x)', and now it's time for your opponent to actually show the consequent `forall y. P(y)' of the implication
- 23:12 < ski> and this is true if `P(y)' is true for every `y' in the domain
- 23:12 < ski> so at this point you can attempt to poke a hole in your opponents reasoning, by finding an `y' where `P(y)' is false
- 23:13 < ski> let's say that you pick a specific element `y0' that you wonder if your opponent can prove `P(y0)' for
- 23:13 < ski> now, the fun happens :
- 23:14 < ski> at this point, your opponent quits the current game, and *loads* a previous game position, namely just before s/he told you that there is an `x' such that ...
- 23:14 < ski> so we're back at an earlier stage in the argument now
- 23:14 < ski> you have just been told there is an `x' such that the implication holds
- 23:15 < ski> and your task now (as before) it so try to disprove the implication, by proving the antecedent and disproving the consequent
- 23:15 < ski> and, as before, if you fail in proving the antecedent `P(x)', then your opponent wins by default
- 23:16 < ski> so, assume instead (as before) that you manage to prove `P(x)'
- 23:16 < ski> but the difference from before is that the secret `x' here is actually the `y0' that *you* chose in a "parallel universe"
- 23:16 < ski> so, you've actually proved `P(y0)' yourself !
- 23:17 < ski> at this point, your opponent quits the game again, and loads the position that was just after you had chosen `y0' (when you attempted to disprove `forall y. P(y)')
- 23:18 < ski> and this time, your opponent has a proof of `P(y0)' (which you in fact computed in the other "parallel universe")
- 23:18 < ski> so, for your specific choice of `y0', your opponent has proven `P(y0)'
- 23:18 < ski> if you want to, you could at this point load the position in the game just before you chose `y0'
- 23:18 < ski> and you could choose say `y1' instead
- 23:19 < ski> but then, by the same procedure as above, your opponent will still end up with a proof of `P(y1)'
- 23:19 < ski> and that's it !
- 23:19 < ski> dgpratt : how's that for an informal computational description ? :)
- 23:21 < ski> (btw, note that in the sequent `|- exists x. P(x) -> (forall y. P(y)) , exists x. P(x) -> (forall y. P(y))' the latter conclusion corresponds to the first parallel universe above, and the former conclusion corresponds to the second parallel universe)
- 23:22 < Saizan> these universes are more braided than parallel :)
- 23:24 < ski> yeah, the "parallel universe" was only meant as an analogy :)
- 23:30 < ski> (btw, note that the opponent didn't use your initial proof of `P(y)' : this corresponds to it being eliminated by left-weakening at the top :: similarly in the second universe, your opponent just ignored your pending wait for a proof of `forall y. P(y)' : this corresponds to the right-weakening of it at the top)
- Day changed to 27 May 2012
- 02:58 < dgpratt> ski: holy crap! nice explanation :)
- 03:04 < ski> dgpratt : (: any comments ?
- 03:14 < dgpratt> it certainly makes sense as a stand-alone explanation, but I'm still working on connecting it to the initial derivation
- 03:23 < dgpratt> ski: holy crap again!...maybe
- 03:23 < dgpratt> ok, I can't quite put this together yet, but my mind is trying to make a connection between this and how existential quantification works in Haskell
- 03:24 < dgpratt> (another subject of which I have a rather limited understand)
- 03:26 -!- augur [~augur@208.58.5.87] has joined ##logic
- 03:27 < ski> the thread of action in the explanation above starts tracing from the bottom sequent in the derivation, up through the right conclusion, throught the `forall y.' part which is opened by the `forall'-right rule as `x', up to the `exists'-right rule above which hides `x' as `x0' (later renamed `x' again), down through that other conclusion back to the bottom sequent
- 03:28 < ski> there we await the player to prove `P(x)' which we trace back up that conclusion up to the `P(x)' assumption, which is transferred over to an `P(x)' conclusion at the top
- 03:29 < dgpratt> ski: makes sense
- 03:29 < ski> and then we follow that down again the latter conclusion, as it gets `forall y0.', &c. added in front of it
- 03:29 < ski> eventually proving the `P(y)' part of the latter conclusion
- 03:29 < ski> (which by right-contraction is the single conclusion of the final sequent)
- 03:30 < ski> i saw you were doubtful of the `forall'-right rule before
- 03:30 < ski> but this isn't really that different from the following
- 03:31 < ski> ------------ id
- 03:32 < ski> P(x) |- P(x)
- 03:32 < ski> ---------------------- |- exists
- 03:32 < ski> P(x) |- exists y. P(y)
- 03:33 < ski> ------------------------- |- ->
- 03:33 < dgpratt> the fact that the forall-right rule requires a "fresh" x makes it easier to....accept
- 03:33 < ski> |- P(x) -> exists y. P(y)
- 03:33 < ski> ----------------------------------- |- forall
- 03:33 < ski> |- forall x. P(x) -> exists y. P(y)
- 03:33 < ski> here, in some sense, the `x' and the `y' is "the same"
- 03:34 < ski> but the point is that we've hidden one of the `x's behind the bound variable `y' when we make the `|- forall' step
- 03:34 < ski> so that `y' doesn't occur in any premise nor in any other conclusion before applying this rule
- 03:35 < ski> the same behaviour is perhaps even clearer with `exists'-elimination
- 03:36 < ski> Gamma |- exists x. Phi[x] Gamma , Phi[x] |- Psi
- 03:37 < ski> ------------------------------------------------- exists-E
- 03:37 < ski> Gamma |- Psi
- 03:37 < ski> here the *formula* `Psi' doesn't depend on `x' (nor does the other premises in `Gamma') -- but the *proof* may still depend on `x'
- 03:38 < ski> anyway, in a sequence `Gamma |- Phi , Psi', this `Phi , Psi' is more or less the same as `Phi \/ Psi'
- 03:38 < ski> so one could consider doing steps
- 03:38 < copumpkin> ski: you need a whiteboard :)
- 03:39 < ski> P(y) |- P(x) -> forall y0. P(y0) , P(x)
- 03:39 < ski> P(y) |- exists x0. P(x0) -> forall y0. P(y0) , P(x)
- 03:40 < dgpratt> ski: this is all good stuff and thus I am reluctant to slow you down, but I think my information-absorption potential has been exceeded for the day :)
- 03:40 < ski> P(y) |- (exists x0. P(x0) -> forall y0. P(y0)) \/ P(x)
- 03:40 < ski> P(y) |- forall y0. (exists x0. P(x0) -> forall y0. P(y0)) \/ P(y0)
- 03:40 < ski> then we use a distributive law
- 03:40 < dgpratt> I'll definitely be reading and re-reading all this, but I hope you won
- 03:40 < ski> P(y) |- (exists x0. P(x0) -> forall y0. P(y0)) \/ (forall y0. P(y0))
- 03:40 < ski> P(y) |- exists x0. P(x0) -> forall y0. P(y0) , forall y0. P(y0)
- 03:41 < dgpratt> err...I hope you won't expect me to make any salient comments on all this for the time being :)
- 03:41 < ski> in the step `.. |- forall y0. (exists x0. ..x0..) \/ P(y0)', the situation isn't very different from with `forall x. P(x) -> exists y. P(x)' in my example above
- 03:42 < ski> (meaning `forall x. (P(x) -> (exists y. P(x)))' if it wasn't clear)
- 03:42 < ski> copumpkin :)
- 03:42 < ski> dgpratt : ok, well i'm done :)
- 03:43 < ski> (the point was mostly to try to show how the situation with `exists'-right and `forall'-right in your given derivation isn't really that much different from my situation with `|- exists' and `|- forall' above)
- 03:46 < ski> (note how classically, `foo -> bar' is the same as `not foo \/ bar', which should perhaps make the analogy clearer)
- Day changed to 31 May 2012
- 16:48 < dgpratt> ski: I have a question for you if you're able
- 16:49 * ski . o ( "to be able to disable, is that stable ?" )
- 16:50 < dgpratt> hmm...I'll interpret that as an affirmative
- 16:51 < dgpratt> every time I think I understand the concept of free and bound variables, I encounter something that tells me I don't
- 16:51 < dgpratt> case in point, from our conversation the other day:
- 16:51 < dgpratt> <ski> well, first, the top three sequents have both `x' and `y' as free variables
- 16:51 < dgpratt> <ski> the rest of the them (*including* the last two ones) has only `y' as free variable
- 16:52 < ski> hehe, yes, this is a somewhat unusual concept of free variable
- 16:52 < ski> but, you need something like this, if you want to allow empty domains
- 16:52 < ski> (and doing this is very natural in categorical semantics)
- 16:52 < dgpratt> this is in reference to http://i.imgur.com/wqL8a.png
- 16:53 < ski> "The Image you are requesting does not exist or is no longer available"
- 16:55 < ski> oh, right, i just realized i still have the picture open
- 16:55 < dgpratt> so...how does one distinguish between free and bound vars in the sequent calcululs? and...
- 16:56 < dgpratt> ...what are the implications as such?
- 16:57 < dgpratt> by the way, I was trying to think about this in terms of Haskell's type quantification and something occurred to me that kind of made sense, but I'm not sure it's the right intuition...
- 16:58 < dgpratt> I was thinking about a function with a type like this:
- 16:58 < dgpratt> f :: forall a b. (forall c. c -> a) -> b -> a
- 16:59 < dolio> Things are a little clearer in something like Haskell (type theory) because variables have to go in the context to specify their type.
- 16:59 < dolio> But that's often not done in logic because there's only one domain of discourse for the variables to range over.
- 16:59 < dgpratt> now as I understand it c is (in essence) an existentially quantified type var...
- 16:59 < dolio> (At least, in many logics.)
- 17:01 < dgpratt> but the implication is that in order to pass something in for that first input of 'f', I need a function that accepts a universally quantified type...right?
- 17:01 < dolio> It is existentially quantified in the sense that forall c. c -> T is equivalent to (exists c. c) -> T if c is not free in T.
- 17:03 < dolio> You can fiddle around with that type...
- 17:04 < dolio> forall a b. (forall c. c -> a) -> b -> a ~ forall b. b -> (forall a. (forall c. c -> a) -> a) ~ (exists b. b) -> (forall a. ((exists c. c) -> a) -> a) ~ (exists b. b) -> (exists c. c)
- 17:04 < dolio> Because forall a. (T -> a) -> a is isomorphic to T if a is not free in T.
- 17:05 < dgpratt> dolio: interesting; I shall have to ponder that some
- 17:10 * ski was busy transcribing the proof in question, for easy reference
- 17:10 < ski> here it comes :
- 17:10 < ski> ----------------------------------------------------------------------------------- (axiom)
- 17:10 < ski> P(x) |- P(x )
- 17:10 < ski> ----------------------------------------------------------------------------------- (weakening-l,weakening-r)
- 17:10 < ski> P(x), P(y) |- forall y0. P(y0) , P(x )
- 17:10 < ski> ----------------------------------------------------------------------------------- (->-r)
- 17:10 < ski> P(y) |- P(x ) -> (forall y0. P(y0)), P(x )
- 17:11 < ski> ----------------------------------------------------------------------------- (exists-r)
- 17:11 < ski> P(y) |- exists x0. P(x0) -> (forall y0. P(y0)), P(x )
- 17:11 < ski> ----------------------------------------------------------------------------- (forall-r)
- 17:11 < ski> P(y) |- exists x . P(x ) -> (forall y0. P(y0)), forall y0. P(y0)
- 17:11 < ski> ------------------------------------------------------------------------------ (->-r)
- 17:11 < ski> |- exists x . P(x ) -> (forall y0. P(y0)), P(y ) -> (forall y0. P(y0))
- 17:11 < ski> ------------------------------------------------------------------------- (exists-r)
- 17:12 < ski> |- exists x . P(x ) -> (forall y . P(y )), exists x . P(x ) -> (forall y . P(y ))
- 17:12 < ski> ------------------------------------------------------------------------- (contraction-r)
- 17:12 < ski> |- exists x . P(x ) -> (forall y . P(y ))
- 17:12 < ski> (ok, a little damaged, but i hope it will do)
- 17:13 < ski> dgpratt : to answer your question, the classical definition of a free variable means the variable must occur at least once (and "freely")
- 17:13 < ski> however, it's often nicer to keep track of exactly which variables are *allowed* to occur in an expression/formula
- 17:14 < ski> e.g. in math, `x - x' can be expressed as `0'
- 17:14 < ski> we'd like to say that when we state `x - x = 0', then both sub-expressions here have the same set of free variables
- 17:14 < ski> so, here we're distinguishing between the variables that actually *occur* (freely) and those that *may* occur
- 17:15 < ski> the former must be a subset of the latter
- 17:15 < dolio> Man, LK is weird.
- 17:15 < ski> (this is a bit similar to specifying a codomain of a function as a set which only need to *contain* every possibly result-value of the function)
- 17:16 < ski> (dolio : you say my computational interpretation of this proof some days ago ? :)
- 17:16 < dgpratt> ski: oh, I think I see -- but I've been burned on that before :)
- 17:16 < ski> in most common accounts of (single-sorted) logic, this is a correct inference :
- 17:16 < dolio> ski: No, but I have a vague idea of how it'd go.
- 17:17 < dolio> Those uses of ->-r feel wrong to me, though. :)
- 17:19 < dolio> Presumably your interpretation is that it's setting up communicating processes of a sort, though?
- 17:20 < ski> ----------------------
- 17:21 < ski> P(x) |- P(x)
- 17:21 < ski> -------------------------------- exists
- 17:21 < ski> P(x) |- exists x. P(x)
- 17:21 < ski> forall --------------------------------
- 17:21 < ski> forall x. P(x) |- exists x. P(x)
- 17:21 < ski> so, e.g. from `forall x. x = x' we can conclude `exists x. x = x'
- 17:21 < ski> iow, the domain is non-empty
- 17:22 < ski> (or, if every invisible unicorn is pink, then there exists an invisible unicorn, which is pink)
- 17:23 < dolio> No.
- 17:23 < dolio> If everything is an invisible pink unicorn, then there exists an invisible pink unicorn.
- 17:23 < ski> (the domain here is the set of all invisible unicorns)
- 17:24 < dolio> I guess that works, too.
- 17:24 < ski> dgpratt : so, what we're going to do instead is to explicitly mention the variables which are *allowed* to occur in the premises and conclusions
- 17:24 < dolio> Presumably you wouldn't be able to prove that all invisible unicorns are pink, I guess.
- 17:24 < ski> and we're going to say that in `Gamma |- Delta', we have a single set of variables which are allowed to occur
- 17:24 < ski> the "free variables"
- 17:25 < ski> dolio : hm, i suppose i'd better permute `unicorn' and `pink'
- 17:25 < ski> (so that we have the domain of all invisible pink stuff)
- 17:26 < ski> (so that we can conclude that having such a thing is a contradiction in terms)
- 17:26 < ski> anyway
- 17:26 < ski> we're going to write `Gamma |-_{Chi} Delta', where `Chi' is the set of free variables, for this sequent
- 17:26 < ski> so, we get
- 17:27 < ski> --------------------------
- 17:27 < dolio> Well, if your domain of discourse is invisible pink stuff, the domain is empty, so the logic is letting you do unsound things. :)
- 17:27 < ski> P(x) |-_{x} P(x)
- 17:27 < ski> ---------------------- exists
- 17:27 < ski> P(x) |-_{x} exists x. P(x)
- 17:27 < ski> forall ------------------------------------
- 17:27 < ski> forall x. P(x) |-_{x} exists x. P(x)
- 17:28 < ski> dp the point to note is that we *still* have `x' as a free variable in the final sequent
- 17:28 < dgpratt> ski: noted
- 17:29 < ski> so, this really reads something like : provided that we have an individual `x' in the domain, then if for every `x', `P(x)' holds, then there exists an `x' such that `P(x)' holds
- 17:29 < ski> you can get rid of variables by using a substitution
- 17:30 < ski> e.g. going from `P(x,y) |-_{x,y} Q(s(x))' to `P(s(y),y) |-_{y} Q(s(s(y)))'
- 17:31 < ski> and you can do that in the above little proof, thus getting rid of the free (but non-occuring) variable `x'
- 17:31 < dgpratt> ski: hmm
- 17:31 < ski> but then you instead get all the variables which freely occured in the term you substituted for `x'
- 17:32 < ski> so, the only way to end up with an empty set of free variables is to have a *closed* term to substitute for `x'
- 17:32 < ski> e.g. if you're working in a signature where you have a constant `z' :)
- 17:33 < ski> dgpratt : in your more complicated proof a bit up, the same thing happens with `y'
- 17:33 < ski> but not with `x'
- 17:33 < ski> only `y' is a free variable in the last sequent
- 17:36 < dgpratt> ski: ok, I'm gonna save this chat log and re-read it 10 or so times until it sinks in :)
- 17:36 < ski> this is because the right-rule for `forall' "discharges" the assumption of `x' being an individual in the domain
- 17:37 < ski> the right-rule for `exists' only takes something that exists, and hides it in the formula
- 17:38 < ski> you are still implicitly depending on it existing (and specifically, of the variables occuring in it existing)
- 17:38 < ski> similarly for the left-rule for `forall', here you have a general assumption, and instantiate to an already existing thing
- 17:39 < ski> but not so in right-rule for `forall', since here the variable is actually a hypothetical/arbitrary element, which need not correspond to *any* actual elements (i.e. the number of elements in the domain can be zero)
- 17:40 < ski> and similarly for the left-rule for `exists', here you're not already assuming the existence of the things, because the existential *itself* encodes the assumption of the thing existing
- 17:41 < dgpratt> ski: ok, that makes sense at an elementary level
- 17:41 < ski> i.e. you don't need to keep track of the thing as one (or depending on some) variable(s) -- because simply by assuming the existential formula do you *implicitly* assume the existence of the thing
- 17:42 < ski> the left-rule merely takes the step from this existence being implicit, to it being explicit (or in the other direction, depending on whether you read the derivation from the conclusion up, or from the axioms down)
- 17:43 < ski> dgpratt : mayhaps you'd like to add free-variable-sets to all of the basic rules, to better understand how they get propagated ?
- 17:44 < ski> dolio : yes, which was the point, of course :)
- 17:44 < dolio> Ah.
- 17:45 < dgpratt> I think so...but not presently :) I'm still trying to absorb all you've said so far :)
- 17:45 < ski> (well, i suppose a greater point was to show that to be able to talk about domains that we don't know yet whether they're empty or not, we need to allow for the possibility of empty domains -- and the above is a nice way to do this)
advertising
Update the Post
Either update this post and resubmit it with changes, or make a new post.
You may also comment on this post.
Please note that information posted here will expire by default in one month. If you do not want it to expire, please set the expiry time above. If it is set to expire, web search engines will not be allowed to index it prior to it expiring. Items that are not marked to expire will be indexable by search engines. Be careful with your passwords. All illegal activities will be reported and any information will be handed over to the authorities, so be good.