Re: ∞ is a free variable
Posted: Mon Oct 07, 2024 8:14 am
This is precisely where we drift apart. It's not obvious to me what is so "obvious" to you and why.
Do you remember me asking you in the past whether the integer 3 is the same number as the real number 3?
If you want a chuckle - the phrase "the same" has its obvious meaning.
Without loss of generality: is integer X the same number as real number X? Yes - I know their domains differ but 5 is 5 is 5 (or so you said)
If we accept that x:N ≡ x:R is a theorem then by implication there exists no function F such that F(x:N) !≡ F(x:R) is inhabited.
So what is this function F (divisible by 2) inhabiting it?
What is this function "divisible by 2" which is true for 3:R but false for 3:N ?
It seems to me the important philosophical question here is "What does it mean for a number to be NON-divisible by 2"?
That's not "integer division". As our friend Magnus Dorkinson was so kind to inform us (using various reputable sources) integer division means "floor division". Integer division discards the remainder. The function you are talking about isn't doing any discarding.
Surely you see a difference between a Mathematical operator with type signature N -> N -> N and another Mathematical operator with type signature N -> N -> N x N ?
They are not the same (where "the same" has its obvious meaning).
How do you do any Mathematics without word games??!?
Here we are... playing a word game about two things being "the same" a.k.a equivalent.
Yeah. Fine. If you want to prove the negation of "divisible by 2" all you have to do is prove that the co-domain of "divisible by 2" is uninhabited.
Which kind of indeterminate state? There are many kinds of indeterminacy.
https://en.wikipedia.org/wiki/Kind_(type_theory)
I am going to address this further below but...
Is it indeterminate that the number is divisible by 2; or is it indeterminate that the number is NOT divisible by 2?
Without excluded middle it's not impossible that both indeterminacies hold.
EDIT: Such as the indeterminacy of TREE(3).
The exact same thing that would be wrong with the definition "a number is even if it's not odd" - it's circular. You are defining the complement by exploiting an unproven involution.
The english word "Either" is just another way to express Excluded Middle a.k.a the axiom of choice.
Either(A,B) -> {Left Projection, Right Projection}
Nothing's right or wrong with it. It does what it does.
It's not possible to determine which Mathematical operator your machine implements until further empirical testing is performed on it. It's a black box and I am going to fuzz the hell out of that thing to eliminate some options.
Suppose I enter "2" an the machine says "Odd"... OK... the machine can't figure out if 2 is divisible by 2.
Suppose I enter 3" and the machine says "Even"...OK.... the machine knows how to divide 3 by 2.
Suppose I enter Tree(3) and the machine says "Odd". Was it actually odd or is the machine signaling it failed to figure out if it's divisible by 2?
Do observe that you are trapped in Excluded Middle again. You are pre-supposing Odd or Even as all-exhaustive categories.
Which is precisely why you had to make a choice about the inndeterminate state. The default choice.
Why do you return Odd and not Even if you can't figure out if it's divisible by 2 or not divisible by 2?
You can define what an odd and even number is without the law of excluded middle.
But you aren't doing that. You are defining it USING excluded middle.
You are presupposing an involution between Odd and Even..
The way we'd do it constructively is we'd define odd and even as separate properties.
Once you've proven that the two categories are all exhaustive within the domain then the involution trivially follows.
In your mode of reasoning not Even -> Odd is an axiom.
In my mode of reasoning it's a theorem.
Surely you understand the difference between axioms and theorems?
Sure, but how many steps would a Turing machine take to NOT divide an integer by 2?
I don't think so. How many steps would the Turing machine take to NOT divide n by 2?
This is the problem with classical reasoning. It fails to grasp the difference between dedicable and semi-decidable problems.
There's a turing machine that can decide whether the number n is divisible by 2.
There is a turing machine that can decide whether a number n is NOT divisible by 2.
These are two different turing machines.
The intermediate answer is neither of the two turing machines has halted.
When "divisibleBy2" OR "NotDivisibleBy2" halts you'll know what kind of number n is.
It's a race... who will win?
Wait and see.
I think in the end you could just parrot a tautology: Even numbers are those for which division by 2 is defined, and odd numbers are those for which division by 2 is undefined.Mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true.--Bertrand Russel
All the Reals are even...
Half the integers aren't.