Torn between classical and constructive mathematics

[Skepdick]

The subset of numbers isn't countable unless you can construct that subset first..

The type for the cardinality of a subset of the natural numbers is a natural number. You do not need to construct that subset first.

That's not always true.

The subset is constructed using members which satisfy predicate p(). If p is undefined e.g halt(x)...how do you type-check it?

Code: Select all

{x | x ∈ S and p(x)}

How do you distinguish between an empty set (e.g NO element satisfied p()) and a non-existing set (e.g p() is undefined)?

It's not about the type of the elements. It is about the type of the cardinality.

If there's no object x, there is no cardinality(x) and there is no typeOf(cardinality(x)).

Your set has 6 elements, and 6 is a natural number. It does not matter of what type the elements are. If you add x, then the cardinality of that set will be 7 instead of 6. It is immaterial what x exactly is.

Nonsense. We aren't talking about the cardinality of sets. We are talking about the cardinality of subsets you can't construct.

There are programs that are guaranteed to halt, such as the empty program.

That's not true. The blank tape problem is equivalent to the halting problem.

So, you can always pick one program from the halting set and one program from the non-halting set. Hence, the axiom of choice is sustainable in that context.

More nonsense. You haven't constructed the halting and non-halting sets. All you have is the set of all programs.

Most elements in the powerset of a countable infinite set -- which is uncountable -- are ineffable.

That's nonsense under axiom of choice.

pick a random element of a powerset and tell me what it is. Why can't you?

They cannot be expressed in language.

Really? You don't know which element of a powerset you are thinking about?

So, most of the elements of such powerset cannot participate in that infinite datastream. Hence, the topos of realizability is not computationally closed.

How do you know if the elements are participating in the infinite datastream? Just wait a bit longer, we are still getting the digits of pi out...

It is trivially easy to produce ineffable objects in the topos, regardless of how carefully you copy programs/constructs into its "chroot".

Of course it's trivially easy. Let p be an ineffable object.

Now what? Tell me something about it. How does it relate to other objects? What properties does it have?

[godelian]

The subset is constructed using predicate p(). If p is undefined e.g halt(x)...how do you type-check it?

Code: Select all

[x for x in N if p(x)]

typeof cardinality([expression]) == "naturalNumber"
You do not need "expression" to determinate this. You also do not need to run the expression. It can be determined at compile time.

Code: Select all

typeof array.length; // "number"

Nonsense. We aren't talking about the cardinality of sets. We are talking about the cardinality of subsets you can't construct.

A subset is still a set. It does not matter if you can construct it or not. The type of array.length is "natural number".

That's not true. The blank tape problem is equivalent to the halting problem.

The blank tape is about blank input. Regardless of what input you feed to a program without instructions, it will halt without doing anything.

ChatGPT: Is it guaranteed to halt?

Yes — a program with no instructions is guaranteed to halt, because there’s nothing to run. The control just returns back to the system immediately.

In more formal terms (like in Turing machine theory), an empty program is trivially a halting program — there’s no infinite loop or recursion possible because there's nothing to start with.

You haven't constructed the halting and non-halting sets. All you have is the set of all programs.

There is no need to construct the entire set of halting and non-halting sets to pick one element out of either set.
It is possible to construct a halting program.
It is possible to construct a non-halting program.
So, it is possible to choose one element out of either set.

Most elements in the powerset of a countable infinite set -- which is uncountable -- are ineffable.

That's nonsense under axiom of choice.

There are aleph-0 many sentences possible in language. There are aleph-1 many elements in the powerset. So, most elements in the powerset cannot be mapped onto a sentence in language.

pick a random element of a powerset and tell me what it is. Why can't you?

You can pick an element of this powerset. However, there are elements that you cannot pick.

They cannot be expressed in language.

Really? You don't know which element of a powerset you are thinking about?

Yanovsky explains that at length in his paper "true but unprovable".

Let p be an ineffable object.
Now what? Tell me something about it. How does it relate to other objects? What properties does it have?

You cannot choose an ineffable object and do anything with it. That is not supported.

[Skepdick]

typeof cardinality([expression]) == "naturalNumber"
You do not need "expression" to determinate this. You also do not need to run the expression. It can be determined at compile time.

Eh? Could you explain the difference between cardinality(expression) and cardinality([expression])?

Isn't the latter a constant/always 1?

Code: Select all

typeof array.length; // "number"

So what's the length of any non-array passed as an input to array.length?

You don't seem to realize that array.length returns a pair (Number, Error).

A subset is still a set.

OK... so according to you this is always well-defined. For any predicate p() and any set S.

Code: Select all

 {x | x ∈ S and p(x)}

It does not matter if you can construct it or not. The type of array.length is "natural number".

Which is just a vacuous theorem of {x | x ∈ S and p(x)} is always well-defined for any S and any p()

The blank tape is about blank input. Regardless of what input you feed to a program without instructions, it will halt without doing anything.

The tape contains no instructions. The tape contains only data (symbols). The instructions are in the transition function. Which responds/reacts to the data.

There are aleph-0 many sentences possible in language.

so array.length(SetOfAllPossibleSentences) returns aleph-0, not a natural number?

Which contradiction are you going for here?

1. array.length must be able to return infinite cardinals like aleph-0 (contradicting the claim it always returns a natural number)
2. or the SetOfAllPossibleSentences cannot be processed by array.length (contradicting the claim that cardinality operations work on all sets)

There are aleph-1 many elements in the powerset. So, most elements in the powerset cannot be mapped onto a sentence in language.

Who cares?
There is no element in any set that cannot be mapped to a sentence in a language.

Let E be the set of all elements which cannot be mapped to sentences in a language.

You can pick an element of this powerset. However, there are elements that you cannot pick.

What do you mean?!? If the subset of elements I CAN pick is well-defined e.g

Code: Select all

{x | x ∈ Powerset(R) and CanBeChosen(x)}

Then the subset of elements that I CAN'T pick is also well defined e.g

{x | x ∈ Powerset(R) and not(CanBeCHosen(x))) }

Yanovsky explains that at length in his paper "true but unprovable".

Weird! Didn't you just prove that which is "unprovable"?

You cannot choose an ineffable object and do anything with it. That is not supported.

Contradiction. Axiom of choice has no restrictions.

You can choose whatever the fuck you want from any set you can make up.
Negate the set of Effable objects... and there you have it!

Code: Select all

{x | x ∈ SetOfAllObjects and not(Effable(x))}

You are trying to have your cake; and eat it too.
You want to have objects which are beyond our ability to identify or work with; while retaining the ability to make arbitrary choices from any collection of objects.

The whole point of realizability is that we are doing non-deterministic programming.

We are constructing polymorphic choice() operators.
And there is a limit to the sort of choice() functions we can realize. Otherwise you end up with code which can backtrack infinitely.

https://en.wikipedia.org/wiki/Nondeterm ... rogramming

Anything can be abstractly defined in set theory! Even the set of things which are undefinable! It's Nullary types all the way down.

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

[godelian]

Eh? Could you explain the difference between cardinality(expression) and cardinality([expression])?
Isn't the latter a constant/always 1?

It depends on the specifics of the syntax.

==ChatGPT==

JavaScript used to have array comprehensions in some versions of Firefox, but they were non-standard and have been removed from the language (specifically from ECMAScript) because they were not widely adopted and created inconsistencies.
Example of deprecated array comprehension (no longer supported):

// This used to work in older versions of Firefox:

let evens = [for (x of [1,2,3,4,5,6]) if (x % 2 === 0) x];

This syntax is no longer valid in modern JavaScript engines.

What to use instead (modern and standard):

You can use .map(), .filter(), and .reduce()—these methods provide the same functionality in a cleaner and standardized way.

Example: Get even numbers from an array

let arr = [1, 2, 3, 4, 5, 6];
let evens = arr.filter(x => x % 2 === 0);

The array comprehension syntax is nowadays considered inconsistent in Javascript. In my impression, it can easily trigger shift/reduce conflicts.

So what's the length of any non-array passed as an input to array.length?

If you declare something to be an array, it will be one, regardless of whether you attempt to populate it with a possibly uncomputable algorithm.

You don't seem to realize that array.length returns a pair (Number, Error).

That depends on the language. "typeof array.length" could be defined, while array is not even populated. It depends on what is possible at compile time versus runtime, and that in turn depends on the language at hand.

A subset is still a set.

Nonsense. If p() is an invalid predicate this subset doesn't exist:

Code: Select all

 {x | x ∈ S and p(x)}

It does not need to exist at compile time for its cardinality to have a type, which could be a compile time property and not a runtime one.

The type of array.length() is either a Natural Number or a Error.

That depends on the language at hand.

The instructions are in the transition function. Which responds/reacts to the data.

There are no instructions. So, it does not respond/react at all.

Weird! Didn't you just prove that which is "unprovable"?

Gödel's incompleteness theorem does indeed something like that. It proves that there exist true but unprovable sentences in PA (or similar).

Contradiction. Axiom of choice has no restrictions.

That depends on whether you accept the axiom or not.

https://en.wikipedia.org/wiki/Nondeterm ... rogramming

I am not familiar with that.

[Skepdick]

Eh? Could you explain the difference between cardinality(expression) and cardinality([expression])?
Isn't the latter a constant/always 1?

It depends on the specifics of the syntax.

I am asking you what YOU meant by it. e.g which syntax were YOU using?

The array comprehension syntax is nowadays considered inconsistent in Javascript. In my impression, it can easily trigger shift/reduce conflicts.

But it's not inconsistent in set theory. Because halts(x) is either true or false (by LEM).

So this is valid: {x | x ∈ SetOfTuringMachines and halts(x) }

If you declare something to be an array, it will be one, regardless of whether you attempt to populate it with a possibly uncomputable algorithm.

OK..So it's an array.

Code: Select all

{x | x ∈ SetOfAllFunctions and UniversalHaltDecider(x) }

That depends on the language. "typeof array.length" could be defined, while array is not even populated. It depends on what is possible at compile time versus runtime, and that in turn depends on the language at hand.

And if you aren't using a compiled language; but an interpreted one?

It does not need to exist at compile time for its cardinality to have a type, which could be a compile time property and not a runtime one.

And if you aren't using a compiled language; but an interpreted one?

That depends on the language at hand.

Oh? In which language does array.length ALWAYS return a number-value and NEVER return an error-value?

There are no instructions. So, it does not respond/react at all.

So it's the NOOP computational operator. e.g the identity function.

It returns exactly what you input. If you input nothing - it returns nothing.

Gödel's incompleteness theorem does indeed something like that. It proves that there exist true but unprovable sentences in PA (or similar).

So it fails to be an example of that which it claims exists. Namely true but unprovable.

That depends on whether you accept the axiom or not.

Well, you are pretending to be a classical mathematician (e.g somebody who accepts it).

I am not familiar with that.

Of course. Logic programming is a dying art.

[Skepdick]

The crux with Classical Mathematics is that the type of ANY uncomputable predicate is necessarily a sub-singleton set.
e.g forall: x,y in S; x = y

The cardinality of S is <= 1.

What is the truth-value of x=y for x,y in ∅?
Instead of explicitly representing this uncertainty, we simply reduce the problem to a trivial case. In classical logic, universal statements over an empty set are always true e.g ∀ x ∈ ∅. P(x).

And when the set is inhabited - it has only 1 element; so x=y is also true.

What you get is a vacuous tautology + information loss. Which case is being witnessed? The empty or non-empty S?

By always reducing uncomputability to a trivial truth, classical mathematics loses the ability to meaningfully engage with the uncertainties inherent in any information processing.

The way to give this a computational treatment is to use the Maybe monad...

https://en.wikipedia.org/wiki/Monad_(ca ... aybe_monad

Instead of saying: “The set is empty, so the predicate holds!”, a computation-aware model would say: “We don’t have a value, so the result is Nothing. We don’t know whether the predicate holds or not.”

[godelian]

Gödel's incompleteness theorem does indeed something like that. It proves that there exist true but unprovable sentences in PA (or similar).

So it fails to be an example of that which it claims exists. Namely true but unprovable.

Yeah, some words are green.

[godelian]

By always reducing uncomputability to a trivial truth, classical mathematics loses the ability to meaningfully engage with the uncertainties inherent in any information processing.

It just deals differently with corner cases, which by themselves are always contorted anyway.

[Skepdick]

Yeah, some words are green.

Yes, that's how declarative statements work.

The color of this sentence is represented using the word "green".

1. This sentence has a property of type "color"
2. The value of the color-property is "green"

Said simply... "green" is the word I use to represent this color.

Welcome to dependent types...where we blur the line between description and definition.

[Skepdick]

It just deals differently with corner cases, which by themselves are always contorted anyway.

And by "deals differently" you mean - it doesn't fucking deal with them at all.

It erases the distinction between subsets of empty and non-empty sets and replaces them with tautologies.

You do want to identify the unbound variables (lack of knowledge) in your system of thought; don't you?
You want to be able to discern “I don’t know” from “true by uncertainty.”; surely?

Uncertainty and uncomputability are first-class citizens in any epistemic language. That's why we have the Maybe monad!

I guess the reason Classical mathematicians don't care about this is because they think they are omniscient.

Every set is constructible as a vacuous subset of an imaginary superset! ∀ x ∈ ∅. P(x)! YOLO!

[godelian]

It just deals differently with corner cases, which by themselves are always contorted anyway.

And by "deals differently" you mean - it doesn't fucking deal with them at all.

It erases the distinction between subsets of empty and non-empty sets and replaces them with tautologies.

You do want to identify the unbound variables (lack of knowledge) in your system of thought; don't you?
You want to be able to discern “I don’t know” from “true by uncertainty.”; surely?

Uncertainty and uncomputability are first-class citizens in any epistemic language. That's why we have the Maybe monad!

I guess the reason Classical mathematicians don't care about this is because they think they are omniscient.

Every set is constructible as a vacuous subset of an imaginary superset! ∀ x ∈ ∅. P(x)! YOLO!

Especially in terms of classical model theory, but in other subdisciplines as well, most mathematical objects are undescribable and uncomputable. They exist in structures that contain them, but they are not individually accessible.

Constructive mathematics cannot see them and often does not even acknowledge their existence because these objects cannot be constructed.

However, these objects are philosophically very interesting.

Most of the truth is ineffable.

That actually has incredible practical consequences. For example, science will never be able to completely predict the universe. Laplace's demon cannot function. Scientism is an unattainable pipedream. Well, that was Hawkins' opinion as he explained it in his lecture, "Godel and the end of physics".

[Skepdick]

Especially in terms of classical model theory, but in other subdisciplines as well, most mathematical objects are undescribable and uncomputable. They exist in structures that contain them, but they are not individually accessible.

Constructive mathematics cannot see them and often does not even acknowledge their existence because these objects cannot be constructed.

Yeah. Nonsense.

Code: Select all

x = Object()

There you go. Object constructor called.

However, these objects are philosophically very interesting.

Something you can't access; or interact with is "interesting"?

What can you say about such an object other than assert its existence?

Most of the truth is ineffable.

You haven't got any truth to eff. Because you don't know any.

[godelian]

However, these objects are philosophically very interesting.

Something you can't access; or interact with is "interesting"?

What can you say about such an object other than assert its existence?

ChatGPT: In constructive mathematics, is it possible to prove that a true sentence is unprovable?

Constructive vs Classical Mathematics

In classical mathematics, you can talk about the truth of a statement independently of whether you can prove it. For example, Gödel's incompleteness theorems show that there are true but unprovable statements in sufficiently powerful formal systems.

In constructive mathematics, truth is closely tied to proof. To assert "A is true" is effectively to assert "A has a proof."

What About "A is true but unprovable"?

In a constructive framework:

Saying "A is true but unprovable" would mean:
"There exists a proof of A, but there is no proof of A" — which is incoherent constructively.
So, you can't prove constructively that a statement is both:
True (i.e. provable), and
Unprovable.

Because "truth" = "provable" constructively, the claim would contradict itself.

Summary

In constructive mathematics, you cannot prove that a true sentence is unprovable, because:
Truth is defined by provability.
“True but unprovable” is not a meaningful distinction constructively.
You can sometimes prove that a sentence is unprovable, but only in a way consistent with constructive logic.

I reject the constructive view on this matter. I subscribe to the classical view that truth is not defined by provability. Provability implies truth because of soundness theorem. However, the reverse is not true. A sentence can be true without being provable. That is the essence of Gödel's syntactic incompleteness theorem.

[Skepdick]

I reject the constructive view on this matter. I subscribe to the classical view that truth is not defined by provability.

See, I don't believe that you believe that.

P1 X (ANY axiom!)
P2 X -> X (identity axiom)
C X

Or simply... If X then X.

This is a valid proof for any true statement.

Provability implies truth because of soundness theorem. However, the reverse is not true. A sentence can be true without being provable. That is the essence of Gödel's syntactic incompleteness theorem.

Can you give me an example of even one such sentence? A single true statement that can't be proven via the identity axiom.

I can't think of any.

This should be pretty fucking obvious; you know; given that a truth-identifier has to identify those truths.

[godelian]

I reject the constructive view on this matter. I subscribe to the classical view that truth is not defined by provability.

See, I don't believe that you believe that.

P1 X (ANY axiom!)
P2 X -> X (identity axiom)
C X

Or simply... If X then X.

This is a valid proof for any true statement.

Provability implies truth because of soundness theorem. However, the reverse is not true. A sentence can be true without being provable. That is the essence of Gödel's syntactic incompleteness theorem.

Can you give me an example of even one such sentence? A single true statement that can't be proven via the identity axiom.

I can't think of any.

This should be pretty fucking obvious; you know; given that a truth-identifier has to identify those truths.

A tautology is obviously always true. Goodstein's theorem, for example, is not a tautology. You cannot prove it from PA but you can from ZFC. It is true but unprovable in PA.