What is free/bind variable?
in [Logic]
|
From: Tegiri Nenashi on 31 Mar 2010 20:09 I mean is it purely syntactic construction? Consider a function of one variable x->f(x). The "x" in any formula involving f is defined as free or bind depending on the larger context, e.g. if there is a quantifier in front, etc. Then, when asked "how many free variables are in the formulas "f(x)" and "^x.f(x)" one would answer 1 and 0, correspondingly. (Not sure if the notation for "^" quantifier is standard; the justification is in the Barendregt paper: "The impact of the lambda calculus in logic and computer science".) However, consider the same function x->f(x) represented as a predicate p(x,y). It has two free variables! Somehow when we view p(x,y) in the context of an additional constraint "A x_1 x_2 y: p(x_1,y) & p(x_2,y) - > x_1=x_2" the list of free variables collapses! Analogous situation arise when a predicate (or function) doesn't depend on some variables; these variables are not free (and, therefore, bound)?
From: William Elliot on 1 Apr 2010 05:29 On Wed, 31 Mar 2010, Tegiri Nenashi wrote: > I mean is it purely syntactic construction? To what are you referring? > Consider a function of one variable x->f(x). The "x" in any formula > involving f is defined as free or bind depending on the larger context, > e.g. if there is a quantifier in front, etc. Then, when asked "how many > free variables are in the formulas "f(x)" and "^x.f(x)" one would answer > 1 and 0, correspondingly. (Not sure if the notation for "^" quantifier > is standard; the justification is in the Barendregt paper: "The impact > of the lambda calculus in logic and computer science".) > > However, consider the same function x->f(x) represented as a predicate > p(x,y). It has two free variables! Somehow when we view p(x,y) in the > context of an additional constraint "A x_1 x_2 y: p(x_1,y) & p(x_2,y) - >> x_1=x_2" the list of free variables collapses! Analogous situation > arise when a predicate (or function) doesn't depend on some variables; > these variables are not free (and, therefore, bound)? > When p is a two place binary constant or variable, then the atomic formula p(x,y) has one free occurrence of x and one free occurrence of y as does the wwf p(x,y) -> p(x,y) The wwf Ax.p(x,y) has one bounded occurrence of x and one free occurrence of y. The wwf Ax.Ay.p(x,y) has one bounded occurrence of x and one bounded occurrence of y. The atomic formula p(x,x) has two free occurrence of x. The wwf Ax.p(x,x) has two bound occurrences of x. The wwf Ax.p(x.x) -> p(y,y) has two bound occurrences of x and two free occurrences of y. The wwf Ax.p(x.x) -> p(x,x) has two bound and two free occurrences of x. Let f be a two place function constant or variable. The term f(x,y) has one free occurrence of x and one free occurrence of y.
From: Frederick Williams on 1 Apr 2010 08:19 William Elliot wrote: > > On Wed, 31 Mar 2010, Tegiri Nenashi wrote: > > > I mean is it purely syntactic construction? > > To what are you referring? > > > Consider a function of one variable x->f(x). The "x" in any formula > > involving f is defined as free or bind depending on the larger context, > > e.g. if there is a quantifier in front, etc. Then, when asked "how many > > free variables are in the formulas "f(x)" and "^x.f(x)" one would answer > > 1 and 0, correspondingly. (Not sure if the notation for "^" quantifier > > is standard; the justification is in the Barendregt paper: "The impact > > of the lambda calculus in logic and computer science".) > > > > However, consider the same function x->f(x) represented as a predicate > > p(x,y). It has two free variables! Somehow when we view p(x,y) in the > > context of an additional constraint "A x_1 x_2 y: p(x_1,y) & p(x_2,y) - > >> x_1=x_2" the list of free variables collapses! Analogous situation > > arise when a predicate (or function) doesn't depend on some variables; > > these variables are not free (and, therefore, bound)? > > > When p is a two place binary constant or variable, then the atomic > formula p(x,y) has one free occurrence of x and one free occurrence of y > as does the wwf p(x,y) -> p(x,y) > > The wwf Ax.p(x,y) has one bounded occurrence of x Some would say two. > and one free occurrence of y. > > The wwf Ax.Ay.p(x,y) has one bounded occurrence of x > and one bounded occurrence of y. Some would say two of each. > The atomic formula p(x,x) has two free occurrence of x. > The wwf Ax.p(x,x) has two bound occurrences of x. Three. > The wwf Ax.p(x.x) -> p(y,y) has two bound occurrences of x Three. > and two free > occurrences of y. > The wwf Ax.p(x.x) -> p(x,x) has two bound Three. > and two free occurrences of x. > > Let f be a two place function constant or variable. > The term f(x,y) has one free occurrence of x and one free occurrence of y. -- I can't go on, I'll go on.
From: Frederick Williams on 1 Apr 2010 08:21 Tegiri Nenashi wrote: > > I mean is it purely syntactic construction? Yes. When used of variables in an expression in a formal language, "free" and "bound" have syntactic definitions which ONLY make sense in the context of the language under discussion -- I can't go on, I'll go on.
From: Frederick Williams on 1 Apr 2010 08:26 Tegiri Nenashi wrote: > > [...] (Not sure if the notation for "^" quantifier is > standard; the justification is in the Barendregt paper: "The impact of > the lambda calculus in logic and computer science".) /\ is fine: it's a bit bigger than the /\ of conjunction but ASCII cannot discriminate. So how about /\ for the quantifier and ^ for conjunction? I like U for universal--and so did Hintikka. -- I can't go on, I'll go on.
|
Next
|
Last
Pages: 1 2 Prev: EINSTEINERCISING MAKES YOU GO BLIND Next: [GR] > The Number 401 - Aleph + Tav |