Mephist

However, re-reading that thread, I see that I threw even harder (and even less comprehensible) stuff, like this one: "A formal proof makes only use of...

Well, I am surprised. I didn't expect somebody to agree with that kind of categorical assertions! :razz: I mean: it's clear that finding the right def...

:smile: :smile: :smile: Yes!! I was starting to despair that there is a way to make me understand... My objection was only this one: BT doesn't make i...

Yes of course they have to be isometries. I meant: there is no way of decomposing an object in an infinite set of open sets and then recomposing them ...

If topology has nothing to do with it why all the proofs of decomposition of objects that don't preserve volume are decomposing the objects in pieces ...

By "models' factorizations" I mean finding the right definitions that allow you to describe some complex (containing a lot of information) models in a...

I linked it in the post just before this one. Here's the link: https://thephilosophyforum.com/discussion/comment/302364

Yes, I see your point. Maybe you are right.

OK, I think I should give some explanation on this point: I wrote you have to take "open sets" as infinitesimal pieces What I meant is you should impo...

I really didn't want to enter in the discussion about Banach-Tarsky theorem again :worry: I found what I wrote about six months ago: . It's still vali...

It was a joke! Yes, of course I don't believe there's something wrong with physical universe because of this theorem.

Ehm, sorry but I am afraid I made a mistake in what I wrote. Better to fix it before it goes too far... I wrote "The digits in a real number should no...

Perfectly agree. Well, I think a lot of interesting calculus at Euler's level could be done in a enough rigorous way, and just make the students aware...

The decimal symbol is the thing that says which digit of the numerator matches which digit of the denominator. If you prune off the decimal symbol you...

I think the main thing to understand here is that decimal numbers with infinite decimals can be considered as an extension of "regular" decimal number...

Now, just before leaving for vacations, the metaphysical part, that surely I'll not be able to defend in a philosophy forum :razz: The algorithms that...

The point is that "computerizable" does not mean "computable", because terms built in classical logic in general don't correspond to computable functi...

Yes! Exactly!! Proofs are constructions in ANY formal logic, because that's how formal logic is defined! There are computer-based proof verification s...

Now, what does intuitionistic logic have to do with algorithms? Here's the quick answer: in intuitionistic logic a proposition P can be interpreted as...

I completely agree. I don't believe that the world is an algorithm either. And mathematical objects (and of course physical objects too) are not algor...

I don't remember which one is the SEP article. Could you send me a link? Yes, the AC can't be construed as a computation, and it's not part of constru...

Hi @"fishfry". Reading again what you wrote, I think that maybe I am able to explain what I meant here. Here's the axiom of choice, taken from wikiped...

Yes, exactly. Not every domain of quantification (set in set theory or type in type theory) is supposed to be enumerable, or iterable.

I would say that "forall x in S", where S is an arbitrary set, is not interpreted as a step-by-step substitution, because in general not for every set...

I am not sure what you mean by "imprecise use of real numbers", however the rules of calculus give precise results: * The volume of a sphere inscribed...

Yes, I find it interesting too, and probably my problem is that I learned about logic only from a practical point of view: proving the correctness of ...

Well, I wrote about physical events because probability is a concept that belongs both to physics and mathematics, but from the point of view of mathe...

It's not about verifying proofs. In every formal logic proofs can be verified mechanically, otherwise it wouldn't be called "formal" logic. It's about...

You can use exactly the same definition of Cauchy-complete totally ordered field in constructivist logic. Even rational numbers are locations on the r...

If you read my posts I have always said the same thing: constructivist logic DOES NOT MEAN assuming that only computable functions exist! If somebody ...

NO! A constructive real DOES NOT REQUIRE a computable Cauchy sequence! ALL Cauchy sequences of rational numbers (computable AND INCOMPUTABLE) are PERF...

But our use of real numbers (at least for the most part) is in integrals and derivatives, right? So the "dx" infinitesimals in integrals and derivativ...

OK, so I have a question: what is this morally correct model of real numbers? The set of all infinitely long decimal representations?

Well, I agree with you that mathematical ideas are much more variable and arbitrary then what it seems to be when you learn it at school. However, as ...

Hi, I believe the main source of confusion here is the concept of a model. If you take ZFC and remove some axioms (the axiom of choice and the logical...

I had an idea to solve the question about Cauchy completeness, that I should have had a long time ago: just look at the book that proposes constructiv...

Yes... well, half of it: the "proofs-as-programs" interpretation is valid even in the standard first order natural deduction logic, if you don't use e...

Let's look at Kolmogorov axioms here: (http://mathworld.wolfram.com/KolmogorovsAxioms.html) Everything that is needed is a set W, some Q_i, that can b...

Wow!!! I knew there was something that missed! :starstruck: Sorry, but I was thinking that you used the term "computable reals" in an intuitive way, w...

I'll try to answer only to what I think are the most relevant points only, OK? Yes, you are right. Yes, exactly! But I have to tell you that in my opi...

Ops... thank you for pointing it out :yikes:

There are too many points, and I have the impression that this discussion doesn't make sense if we don't agree on the definitions of the worlds. So, l...

Hi Bill, I read the paper on Casimir Force. Well, there are several passages that I don't really understand, like for example the derivation of (2.36)...

The sets that you say are not computable, but computable in ZF, are the ones that in type theory are called Inductive types, and correspond to initial...

If R/Q is the quotient class, 1/2 is contained in only one of it's subclasses: the one that contains all rational numbers.

Are you sure about this? I think turing machines are simply strings that can be enumerated as integers. This is not the same thing as solving the halt...

Power Set in ZF: ?x?y?z Power Set in Coq: Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) := Definition_of_Power_set : forall X:Ensemble U,...

But who said that the sets must made of points? Set theory does not say what is a set, only gives a list of axioms that are valid WHATEVER sets you co...

Why??? What part of probability theory is inconsistent with the negation of axiom of choice? Here's an extract from https://en.wikipedia.org/wiki/Prob...

Yes, you are right. This leaves out all Cauchy sequences whose convergence rates are not computable. Because in ZFC you can define non computable func...