∞ is a free variable

[Skepdick]

In Programming Language Theory there exists the concept/distinction between bound and unbound variables.

In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a variable may be said to be either free or bound. A free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not a parameter of this or any container expression. Some older books use the terms real variable and apparent variable for free variable and bound variable, respectively. The idea is related to a placeholder (a symbol that will later be replaced by some value), or a wildcard character that stands for an unspecified symbol.

In colloquial English this could trivially be understood as the distinction between defined and undefined terms.

The symbol "x" is said to be unbound by default, until another symbol; or an expression is bound to it. It represents a free variable.
Unless, and until bound to something free variables represent an unbounded entity. Something without limits, lacking value or quantification.

But that is exactly what the symbol "∞" represents!

If two symbols represent the same concept (an unbound quantity; or value) it follows by the identity axiom that the two symbols are synonymous and interchangeable.

X is identical to ∞ (x ≡ ∞)

∞ to Mathematicians, is like Truth to Philosophers; or like God to theists.

It means whatever you want it to mean.

“When I use a word,’ Humpty Dumpty said in rather a scornful tone, ‘it means just what I choose it to mean — neither more nor less.’

’The question is,’ said Alice, ‘whether you can make words mean so many different things.’

’The question is,’ said Humpty Dumpty, ‘which is to be master — that’s all.”

[Impenitent]

strings are more free?

if there are a finite number of memory spaces created (as huge a number as that is) within all the connected computing devices, how could a number that is infinite actually fit?

-Imp

[Skepdick]

strings are more free?

if there are a finite number of memory spaces created (as huge a number as that is) within all the connected computing devices, how could a number that is infinite actually fit?

-Imp

Suppose there is a finite number of memory spaces.
Suppose there's a single address even.
Suppose we call this address "∞"

How much can you fit in it?

As much as you want, apparently.

[Impenitent]

even if each bit of memory represented one number in the infinite chain, there are a finite number of bits

-Imp

[Skepdick]

even if each bit of memory represented one number in the infinite chain, there are a finite number of bits

-Imp

I only need 1 bit. It can represent anything. Say - all numbers.

If you don't like that representation, it's probably because you care about something other than representing stuff...

Coincidentally "the ability to represent anything" is one of the defining features of free variables. Like ∞.

[ayylien]

you're conflating difference senses of bound. bounded variable (as opposed to free) in logic just means that it is not in the scope of a quantifier. It has no notion of quantity, or limitless, or infinity. We say a variable is unbounded just in case that it is not in the scope of a quantifier.

[Magnus Anderson]

It means whatever you want it to mean.

Not quite. The word "infinity" has a very precise meaning.

[Skepdick]

It means whatever you want it to mean.

Not quite. The word "infinity" has a very precise meaning.

No, it doesn't. Go ahead and give me the precise criteria for preciseness.

[Skepdick]

you're conflating difference senses of bound. bounded variable (as opposed to free) in logic just means that it is not in the scope of a quantifier. It has no notion of quantity, or limitless, or infinity. We say a variable is unbounded just in case that it is not in the scope of a quantifier.

I have no idea what you are trying to say. If you have a symbol that can't be evaluated in any scope - would you call that "bound" or "unbound"?

If the symbols "∃" and "∀" aren't in any scope - what would you call them?

Code: Select all

In [1]: eval("∃")
SyntaxError: invalid character '∃' (U+2203)
In [2]: eval("∀")
SyntaxError: invalid character '∀' (U+2200)

[wtf]

Unless, and until bound to something free variables represent an unbounded entity. Something without limits, lacking value or quantification.

But that is exactly what the symbol "∞" represents!

(My bolded emphasis)

Hey Skeppers. As someone noted, it does seem as if you have conflated the concept of a bound variable in logic, with a BOUNDED quantity in analysis. This is of course wrong.

In any event he symbol ∞ has a very specific meaning in math any time it's used. It can refer to

* The negative and positive points at infinity in the extended real numbers; or

* The point at infinity at the north pole of the Riemann sphere.

* The point at infinity in projective geometry.

In each case, the symbol has a very specific meaning.

In NO CASE does it ever refer to a free variable. It never has that meaning. It can't be freely substituted with something else.

It's possible that you might be thinking of its casual use in popular discussions, where it has a rather vague meaning and not the precise technical meanings given to it in math.

But in math, it has the specific technical meanings I mentioned. In fact in set theory, the mathematical theory of the infinite, the lemniscate symbol is never used. Rather, there are specific symbols for various ordinal and cardinal numbers.

But mostly, when you say that a free variable in logic is not bound, and is therefore not BOUNDED, you are making an error, confusing a bound variable with a bounded quantity. The meanings and contexts are entirely unrelated.

All you've done is engage in a little misleading wordplay.

[Skepdick]

Unless, and until bound to something free variables represent an unbounded entity. Something without limits, lacking value or quantification.

But that is exactly what the symbol "∞" represents!

(My bolded emphasis)

Hey Skeppers. As someone noted, it does seem as if you have conflated the concept of a bound variable in logic, with a BOUNDED quantity in analysis. This is of course wrong.

I am not doing what you are accusing me of doing. Let me try again with more precision (and also because whatever I was thinking at the time of writing that post is now *POOF* gone from my head).

An unbound variable is simply a variable that has not yet been bound to anything meaningful, yet it has the potential to be bound to something meaningful in future.
A free variable is an unbound variable that has no restrictions imposed upon it as to what it can and can't be bound to.
A free variable can be bound to ANY object. Without exception. Including itself.
A non-free variable has restrictions imposed upon what objects it can and can't be bound to.

If you want - a free variable is an untyped variable.
A non-free variable is a typed variable.

Can't bind the integer 2 to a variable of type vector.
Can't bind the set {} to a variable of type monoid.

In any event he symbol ∞ has a very specific meaning in math any time it's used. It can refer to

* The negative and positive points at infinity in the extended real numbers; or

* The point at infinity at the north pole of the Riemann sphere.

* The point at infinity in projective geometry.

In each case, the symbol has a very specific meaning.

In NO CASE does it ever refer to a free variable. It never has that meaning. It can't be freely substituted with something else.

Q.E.D you've given 3 different bindings for the symbol "∞". And on top of that every one of your bindings is recursive e.g it uses the English representation "infinity" for the symbol "∞". You are binding the symbol "∞" to expressions including itself which amounts to the "letrec" binding operator (as distinct from "let")

Every conception/definition of it is a "point". As in fixed point computations...

f (fix f) = fix f
∞ (fix ∞) = fix ∞

Infinity is its own fixed point.

It's possible that you might be thinking of its casual use in popular discussions, where it has a rather vague meaning and not the precise technical meanings given to it in math.

No, I am thinking geometrically and precisely of the Lambda cube/Calculus of Construction. Which is a way of formalizing the restrictions imposed upon variable-binding.

x-axis (→) : types that can bind terms, corresponding to dependent types.
y-axis (↑): terms that can bind types, corresponding to polymorphism.
z-axis (↗): types that can bind types, corresponding to (binding) type operators.

But in math, it has the specific technical meanings I mentioned. In fact in set theory, the mathematical theory of the infinite, the lemniscate symbol is never used. Rather, there are specific symbols for various ordinal and cardinal numbers.

OK... So give me the typing rules for a variable "x" such that you CAN'T bind a finite set to "x", but you can bind an infinite sets to it.

But mostly, when you say that a free variable in logic is not bound, and is therefore not BOUNDED, you are making an error, confusing a bound variable with a bounded quantity. The meanings and contexts are entirely unrelated.

All you've done is engage in a little misleading wordplay.

All you've done is misunderstood my meaning.

The process of binding/bounding (typing) an unbound/free (untyped) variable IS quantization. It's precisely the process of mapping input values from some large set to output values in some smaller set.

You want a concrete example? Sure...Lets define the symbol "N" as in the natural numbers.

Start with a continuous, monotonically increasing function. such as the Real number line. [0,∞) or whatever.
Discretize it using the floor function or some such (I can't be bothered to be precise here).
Big infinity (R) mapped to small infinity (N) is a surjective function Q: R -> N e.g a quantizer.

The reason you don't use the lemniscate symbol is precisely because you assume it implicitly in the Metamathematics of your Mathematics.

[wtf]

An unbound variable is simply a variable that has not yet been bound to anything meaningful, yet it has the potential to be bound to something meaningful in future.
A free variable is an unbound variable that has no restrictions imposed upon it as to what it can and can't be bound to.

Let me stop here at the first thing I don't understand.

Here's the Wiki page on free and bound variables. A bound variable is a variable that's in the scope of a quantifier. A free variable is a variable that's not bound.

I have never heard of a distinction between a free and unbound variable. According to my understanding, backed up by Wiki, they are synonymous.

Where did you get your definition that "A free variable is an unbound variable that has no restrictions imposed upon it as to what it can and can't be bound to."?

In any event, when I say that lim(x ->0) 1/x = infinity, the infinity symbol refers specifically to the infinity of the extended reals. It does not range over anything and it can not be substituted for by anything at all. It's a very specific symbol with exactly one referent, namely the conceptual rightmost point on the extended real number line.

ps -- Here's the Wiki link.

https://en.wikipedia.org/wiki/Free_vari ... _variables

[Skepdick]

Here's the Wiki page on free and bound variables. A bound variable is a variable that's in the scope of a quantifier. A free variable is a variable that's not bound.

OK... Do you see that a choice exists there? A choice to keep those two things as categorically distinct semantic properties.

Lexical scoping is one thing. Binding is another.

A bound variable can be in; or out of scope of a quantifier.
An unbound variable can also bein; or out of scope of a quantifier.

I am also introducing a notion of "degrees of freedom" with respect to binding.
In; or out of scope of a quantifier - a variable is "absolutely free" when it's untyped - e.g it can bind to anything available for binding-to.

Restricting the "binding freedom" of a variable is the same as imposing a type on a variable.

If you want it in more logical/formal sense free implies unbound.
unbound does NOT imply free.

x ∈ R is unbound. It has no specific value in R. x is NOT free.

I have never heard of a distinction between a free and unbound variable. According to my understanding, backed up by Wiki, they are synonymous.

They can be. When you are being imprecise. I am talking about degrees of unboundness and degrees of freedom with respect to bindings.

An untyped variable can represent anything.
A typed variable can't.

e.g x can be pi. x∈N can't be pi.

Where did you get your definition that "A free variable is an unbound variable that has no restrictions imposed upon it as to what it can and can't be bound to."?

From my intuition. And from type theory. The type of a variable imposes limits on what it can and can't be bound with.

There may be a more common definition about the same thing I am talking about. I am an autodidact - so I wouldn't know.

In any event, when I say that lim(x ->0) 1/x = infinity, the infinity symbol refers specifically to the infinity of the extended reals. It does not range over anything and it can not be substituted for by anything at all. It's a very specific symbol with exactly one referent, namely the conceptual rightmost point on the extended real number line.

Specific how? You've imposed no binding limits on "x". It could be anything,

As far as I can tell it could be x -> 0 in N*
Or X -> 0 in R*
Or X -> 0 in any domain really.

Also, why can't it be substituted ?!?

Surely I can substitute infinity (or any of its representations) for the expression "lim(x ->0) 1/x" ?!?

[wtf]

OK... Do you see that a choice exists there? A choice to keep those two things as categorically distinct semantic properties.

Lexical scoping is one thing. Binding is another.

A bound variable can be in; or out of scope of a quantifier.
An unbound variable can also bein; or out of scope of a quantifier.

Well nevermind all that ... the essential point is that the infinity symbol ∞ as it is used in math is a CONSTANT, not a variable. If you had titled this thread, "5 is a free variable," your conceptual error would be more clear.

∞ does not stand for anything. It's not a variable that ranges over a collection of possible values. It's a particular constant; whether it's the extended reals or the Riemann sphere or whatever. It's not a free variable, it's not a bound variable. It's not a variable at all. It's a constant.

I am also introducing a notion of "degrees of freedom" with respect to binding.
In; or out of scope of a quantifier - a variable is "absolutely free" when it's untyped - e.g it can bind to anything.

Like 5? What can bind to 5? Likewise, what can bind to the infinity symbol?

Restricting the "binding freedom" of a variable is the same as imposing a type on a variable.

Yes but the infinity symbol is not a variable. And you haven't given an example to support your claim that it is.

If you want it in more logical/formal sense free implies unbound.
unbound does NOT imply free.

You are making a distinction that's not found in the literature.

They can be. When you are being imprecise. I am talking about degrees of unboundness and degrees of freedom with respect to bindings.

This is your concept, not found in the standard literature.

But even granting (for sake of discussion) that you are on to something; it can not apply to the infinity symbol, which in any mathematical context is a constant and not a variable.

An untyped variable can represent anything.
A typed variable can't.

I won't argue your conflation of CS or type theory concepts with the basic logical definitions.

The main point is that the infinity symbol is not a variable.

From my intuition. And from type theory. The type of a variable imposes limits on what it can and can't be bound with.

Ok. So these are original ideas of yours. Nothing wrong with that. We might even have a conversation about it sometime. But it doesn't bear on the infinity symbol, which in mathematical contexts is a constant and not a variable. Nothing binds to it.

There may be a more common definition about the same thing I am talking about. I am an autodidact - so I wouldn't know.

An autodidact is one who learns standard material on their own.

In this case you are making up your own material. You may be a researcher, or a genius, or a crank. It doesn't matter here. Because whatever your ideas on variables may be, the infinity symbol is not a variable. Nothing binds to it, any more than when we write 2 + 3 = 5, something binds to 5. No. 5 is a constant. It is not a variable. Likewise the infinity symbol is a constant. It doesn't bind to anything, it doesn't range over a set of values.

In any event, when I say that lim(x ->0) 1/x = infinity, the infinity symbol refers specifically to the infinity of the extended reals. It does not range over anything and it can not be substituted for by anything at all. It's a very specific symbol with exactly one referent, namely the conceptual rightmost point on the extended real number line.

Specific how? You've imposed no binding limits on "x". It could be anything,

As far as I can tell it could be x -> 0 in N*
Or X -> 0 in R*
Or X -> 0 in any domain really.

We aren't talking about x. We're talking about the infinity symbol. It's a constant in this context, denoting the infinity of the extended real numbers. Infinity isn't a free or bound variable here. It's a constant.

So the summary here is that you may or may not have some interesting ideas about the "degree of boundedness" of a bound variable. But regardless, those ideas don't apply to the infinity symbol, because in mathematical contexts, the infinity symbol is not a variable. It's a constant. It's a particular point in the extended real numbers, just like 5 is a particular point in the real numbers.

[Skepdick]

Well nevermind all that ... the essential point is that the infinity symbol ∞ as it is used in math is a CONSTANT, not a variable.

Distinction without relevance. There's practically no difference between a constant and an immutable variable.

Both require binding before being used in any formula/expression.

This example (using Rust) declares the term "A" as a constant with type "i32" and value "10".

Code: Select all

const A: i32 = 10;

And here you have a syntax error because the binding operator declares neither a type signature nor a value for the symbol ""∞"

Code: Select all

const ∞: ??? = ???;

If you had titled this thread, "5 is a free variable," your conceptual error would be more clear.

What's an "error" in Mathematics? The concept is not well defined.

If the symbol "5" has no binding then yes - it's a free variable.

Show me its binding.

∞ does not stand for anything.

Q.E.D!

In the example above the CONSTANT "A" stands for the 32 bit integer "10".
Also in the example above the CONSTANT "∞" doesn't stand for anything.

Because it's NOT bound to anything.

Yes but the infinity symbol is not a variable. And you haven't given an example to support your claim that it is.

Burden of proof is not on me. It's on you.

Show me the binding for the term ""∞" (which you claim to be a CONSTANT).

Yes but the infinity symbol is not a variable. And you haven't given an example to support your claim that it is.

That's just a conceptual error on your part. I don't care if it's a variable or a constant. I only care if it's bound or unbound.

You insist that it's NOT a free variable. Fine! Show me its binding.

I won't argue your conflation of CS or type theory concepts with the basic logical definitions.

The main point is that the infinity symbol is not a variable.

I am using the exact definitions you claim to be using.

A symbol that is NOT bound is said to be free.
A symbol that is free is said to be unboundbound.

What's the symbol "∞" bound to?

A symbol that is NOT in the scope of a quantifier is a free symbol.
Which quantifier is the symbol "∞" in the scope of?

If it's not bound to anything then it's unbounded; and by your own definition - it's free.

We aren't talking about x. We're talking about the infinity symbol. It's a constant in this context, denoting the infinity of the extended real numbers. Infinity isn't a free or bound variable here. It's a constant.

Constant. Global (unscoped) immutable variable. Potato/potatoh. This is a question of binding.

Finish binding this symbol:

Code: Select all

const ∞: ??? = ???