∞ is a free variable

[wtf]

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

There is not much space for conversation if you think 5 is a variable.

In the mathematical expression f(x) = 5, 5 is a constant. Its value does not "range" over anything.

In a programming language with = as the assignment operator, in the assignment

x = 5

the 5 is a constant.

You are entitled to make up your own private theory in which its a variable, but in that case I can't argue with your private language.

It's true that in a programming language 5 stands for an internal bit representation of the number 5. But that's all it stands for. It doesn't range over anything.

If you were to later say

x = 6

then 6 (or its internal representation) would be loaded in to the memory area allocated to the variable x.

But if you set 5 = 6, that would generate an error. In fact I just tried it out in Python3.

Code: Select all

>>> 5 = 6
  File "<stdin>", line 1
SyntaxError: cannot assign to literal

You started out claiming that ∞ is a variable, and in defense of your claim you referenced your own personal theory of the "degree of boundedness" of a bound variable in logic. That is an interesting concept, but it's a side issue here.

The point is that ∞ is not a variable, it's a constant.

And now you seem to be claiming that 5 is a variable.

There's no conversation to be had if you are going to make up your own words for things. There is no textbook or paper or school of thought in math, logic, type theory, philosophy, or computer science in which 5 is a variable. 5 is a constant. It stands for the abstract, Platonic number 5 and nothing else. It is never used to range over any collection of values. Surely you know this, and I'm puzzled as to why you would claim otherwise.

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

The symbol ∞ stands for the largest element of the set of extended real numbers, as taught in single-variable calculus the world over.

In mathematics, the extended real number system is obtained from the real number system by adding two elements denoted +∞ and -∞ that are respectively greater and lower than every real number.

https://en.wikipedia.org/wiki/Extended_real_number_line

[mickthinks]

Skepdick—not even wrong.

[Skepdick]

There is not much space for conversation if you think 5 is a variable.

Your inability to participate in such a conversation doesn't mean there's no space for it. The space can be constructed.

Only there's no need - since the space (paradigm?) has been around for a few decades now.

In the mathematical expression f(x) = 5, 5 is a constant. Its value does not "range" over anything.

1. "f(x) = 5" is a malformed expression in the language I am using.

Code: Select all

❯ agda function-five.agda
Checking function-five 
function-five.agda:1,1-8
Missing type signature for left hand side f x
when scope checking the declaration
  f x = 5

2. Of course it ranges over something - a singleton.

Code: Select all

In [1]: eval("5")
Out[1]: 5

You know what doesn't range over anything? An unbound symbol.

Code: Select all

In [1]: eval("X")
NameError: name 'X' is not defined

If you want me to explain this to you in Category Theoretic terms - it's an object without an identity morphism. So it fails to form a category.

And now it ranges over something too.

Code: Select all

In [2]: class SelfReturning:
   ...:     def __init__(self, name):
   ...:         self.name = name
   ...:
   ...:     def __repr__(self):
   ...:         return self.name
   ...:
   ...: X = SelfReturning('X')
   
In [3]: eval("X")
Out[3]: X

No more NameError!

the 5 is a constant.

All I am hearing you say when you use the term "constant" is that its binding is immutable.

Fine.

But you are still not showing me its binding

Because it's bound to some mystical entity in the Platonic realm. Lol.

That sounds like a private language to me.

You are entitled to make up your own private theory in which its a variable, but in that case I can't argue with your private language.

My theory is so "private" it has a Wikipedia page, an entry on nLab, 18100 results on Google sholar, an open source implementation, and easilly accessible documentation.

I think you are using a private definition of "private theory" and "private language".

Where's the source code/documentation for the language in which the expression "f(x) = 5" is to be interpreted?

It's true that in a programming language 5 stands for an internal bit representation of the number 5.

It doesn't stand for anything of that sort. Both the binary and decimal encodings (which happen to be isomorphic) stand for whatever you are representing using your representation system.

But if you set 5 = 6, that would generate an error. In fact I just tried it out in Python3.

Code: Select all

>>> 5 = 6
  File "<stdin>", line 1
SyntaxError: cannot assign to literal

Then don't use a notation which treats it as a literal/primitive? Use the Lambda calculus and Church encodings.

Here's the important bit:

Terms that are usually considered primitive in other notations (such as integers, Booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding... In the untyped lambda calculus the only primitive data type is the function.

Numbers? What are those? All you get is functions!

And so...

In N 5 is bound to the expression λf.λx.f (f (f (f (f x))))
In N* 5 is bound to the expression λf.λx.f (f (f (f x)))

Please pay attention! Using this encoding 5:N != 5:N*
They litearly represent different Mathematical objects.

And just like that the symbol you call "5" ranges over TWO possible values/bindings.

So what does f(x) = 5 even mean?!?

Is it supposed to mean f(x) = 5:N; or is it supposed to mean f(x) = 5:N* ?

Also pay attention that in such a system 5 = 6 would be a perfectly meaningful informal Mathematical statement that could be formally interpreted as 5:N+ = 6:N

You started out claiming that ∞ is a variable, and in defense of your claim you referenced your own personal theory of the "degree of boundedness" of a bound variable in logic. That is an interesting concept, but it's a side issue here.

It's not a side issue. It's THE issue.

Show me the binding for the symbol "∞"

The point is that ∞ is not a variable, it's a constant.

No! It's a chicken.NO! A hamburger.

Variable. Constant! Potato/potatoh! An immutable binding functions as a constant.

Show me its binding!

There's no conversation to be had if you are going to make up your own words for things.

I am not making up any words. I am using precisely the formal definitions you claim to be using.

If it appears in the scope of a quantifier then the name/label 5 is bound. e.g it exists.
If it doesn't appear in the scope of a quantifier then the name/label 5 is unbound. e.g it doesn't exist.

You know... because...

In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists"

https://en.wikipedia.org/wiki/Dependent_type

There is no textbook or paper or school of thought in math, logic, type theory, philosophy, or computer science in which 5 is a variable. 5 is a constant.

Fine! We'll use the label "constant" instead of the label "variable". Sophist.

WHICH of these two constants is "5" ?

1. const 5 := λf.λx.f (f (f (f (f x))))
2. const 5 := λf.λx.f (f (f (f x)))

It stands for the abstract, Platonic number 5 and nothing else.

Which abstract Platonic number is that?

λf.λx.f (f (f (f (f x)))) as understoodin N

OR

λf.λx.f (f (f (f x))) as understood in N*

It is never used to range over any collection of values.

Contradiction. It ranges over a singleton.

Which one?

λf.λx.f (f (f (f (f x)))) or λf.λx.f (f (f (f x)))

Surely you know this, and I'm puzzled as to why you would claim otherwise.

Because in Dependent Type Theory ALL terms depend on values.

It just happens that you believe the value of 5 depends on itself.
And I believe its value depends on λf.λx.f (f (f (f (f x)))) or λf.λx.f (f (f (f x)))

The symbol ∞ stands for the largest element of the set of extended real numbers, as taught in single-variable calculus the world over.

I didn't ask you for its relation to other symbols.
I asked you for its binding.

[Skepdick]

Skepdick—not even wrong.

Why, thank you for the compliment.

I strive for all my work to be correct by construction. True engineering!

https://www.eschertech.com/products/cor ... uction.php

[Magnus Anderson]

It means whatever you want it to mean.

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

No, it doesn't.

Yes, it does.

Go ahead and give me the precise criteria for preciseness.

Go ahead and explain why I have to do that.

[Magnus Anderson]

Surely you know this, and I'm puzzled as to why you would claim otherwise.

You must not be particularly familiar with Skepdick's output on this forum

If there is one thing that defines him, it's word games.

[wtf]

You must not be particularly familiar with Skepdick's output on this forum

Triumph of hope over experience

[Skepdick]

Go ahead and explain why I have to do that.

So that we can evaluate the definition of "infinity" against your supposed criteria for preciseness?

[Skepdick]

If there is one thing that defines him, it's word games.

My, my! Another compliment.

Yes. I know how definability works. Wish I could say the same about you.

https://en.wikipedia.org/wiki/Definable_set

The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise. -- Edsger Dijkstra

[Skepdick]

Triumph of hope over experience

Amen! Here's to hoping you've come closer to understanding.

[Magnus Anderson]

My, my! Another compliment.

Yoi're lucky that they tolerate you. Any remotely serious board would have banned you long time ago.

[Magnus Anderson]

Go ahead and explain why I have to do that.

So that we can evaluate the definition of "infinity" against your supposed criteria for preciseness?

All you have to do is listen carefully.

The word "infinity" means "a number greater than every integer".

That's it.

So no, it does not mean anything you want it to mean. You can't use that symbol to represent inregers or cats, for example.

[Skepdick]

Go ahead and explain why I have to do that.

So that we can evaluate the definition of "infinity" against your supposed criteria for preciseness?

All you have to do is listen carefully.

The word "infinity" means "a number greater than every integer".

That’s it

Is that what you want it to mean?

OK, but Infinity is not a number.

So no, it does not mean anything you want it to mean. You can't use that symbol to represent inregers or cats, for example.

Yet you demonstrate why I am right…

[Skepdick]

My, my! Another compliment.

Yoi're lucky that they tolerate you. Any remotely serious board would have banned you long time ago.

I am a heretic in any Orthodoxy, and I have zero tolerance for your intolerance.

[Magnus Anderson]

I am a heretic in any Orthodoxy, and I have zero tolerance for your intolerance.

You are a thought and discussion cancer.