Talk:Indecomposability (intuitionistic logic)

A precise definition, please?

So I read this:

indecomposability or indivisibility is the principle that the continuum cannot be partitioned into two nonempty pieces.

What does this mean? The unit interval - that's a continuum, right? Consider all points $x\leq 1/2$ and all points $1/2<x$ . Those are two non-intersecting sets that partition the unit interval into two parts. I'm guessing wildly, but perhaps the precise definition meant to say: the continuum cannot be partitioned into two non-empty open sets that have empty intersection? Something like that? 67.198.37.16 (talk) 17:56, 27 November 2017 (UTC)[reply]

@67.198.37.16: You are evidently unfamiliar with constructive mathematics. You are interpreting the sentence according to conventional logic rather than the logic of constructive mathematics. Michael Hardy (talk) 20:59, 29 June 2021 (UTC)[reply]

The article title is ambiguous, as "constructive mathematics" may refer to other approaches. Moreover the source titles refers to "intuitionistic logic", not to "constructive mathematics". So, I'll move the article to Indecomposability (intuitionistic logic). D.Lazard (talk) 07:46, 4 July 2021 (UTC)[reply]

Is $x\in \mathbb {R}$ "defined" in all points? For example, can you distinguish all points from rational or irrational numbers?--SilverMatsu (talk) 15:18, 4 July 2021 (UTC)[reply]

The answer to this question depends on the theory used to axiomise constructive reals. In general, you can't decide if a Cauchy-convergent sequence will converge to a rational, so a computable theory of reals is not going to be able to answer this everywhere. — Charles Stewart (talk) 18:48, 5 July 2021 (UTC)[reply]

This is an issue in constructive mathematics, not intuitionistic logic: I can construct theories axiomatised in intuitionistic logic where decomposability holds. One can simply take an axiomatisation of the intuitionistic continuum with reals expressed as equivalence classes of Cauchy-convergent sequences of rationals and add trichotomy as a theorem: the theory becomes nonconstructive, but the theory will express formulae to which the principle of the excluded middle will not apply, so its logic remains intuitionistic. The problem with the article is that it fails to do the spadework to make clear the significance of the thesis.

For example, if I define a representation of the reals to be either a rational number (represented as a pair of coprime numbers) or a Cauchy-convergent sequence that does not converge to a rational number (represented as function from naturals to rationals), then every rational has a representation that is entirely arithmetic. But if we try to work with this representation, we can't decide what representation to use in general for the sum of two irrationals, since it is undecidable whether they are a rational.

I'd recommend merging this to either intuitionistic analysis or computable analysis, but neither of those articles have the required background either. There is the rather better article computable number, but it still assumes without discussion one particular representation of computable reals. Our coverage of the intuitionistic continuum sucks, unfortunately. — Charles Stewart (talk) 18:48, 5 July 2021 (UTC)[reply]

Since your arguments apparently concern decomposition into rational and irrational numbers, I'd like to repeat the above question of 67.198.37.16 from 27 November 2017: what about decomposition into (e.g.) negative and non-negative numbers? The article currently says that this isn't possible either - is that correct? If yes, doesn't that mean that no real-number properties at all can be formalized in intuitionistic logic? - Jochen Burghardt (talk) 08:42, 6 July 2021 (UTC)[reply]

The answer is the same: it depends on the representation. There's a representation of computable reals as nested sequences of open intervals on the rationals, where each interval is at most half the length of the previous one. Taking the upper bounds of these intervals gives a monotone decreasing sequence, where the limit is nonnegative iff all the members of this sequence are positive (vica versa we have a criterion for being nonpositive). These criteria are only semidecdable, but if there are schools of constructive mathematics that accept Markov's principle, which essentially says that there is a fact of the matter about semidecidable predicates. For such an approach to constructivism, you have trichotomy (these seqeunces converge to zero iff they are both nonnegative and nonpositive) and allow some instances of decomposability. — Charles Stewart (talk) 10:18, 6 July 2021 (UTC)[reply]

Micheal Hardy wrote: You are evidently unfamiliar with constructive mathematics. -- yes, that would be a fair characterization. Having re-read the article, and read the above discussion, I'm still mostly in the dark. Sure, I understand the "classical analog" of continuous functions to {0,1}, but what's continuity got to do with it? Sure, I understand that in constructive logic, you are not allowed to take limits of infinite sequences (or something like that) so, sure, if you represent real numbers as infinite sequences of some finite thing made from rationals (such as intervals) then, yes, its plausible that difficulties will arise. That is to say, my imagination works well enough to imagine it is so. I am still left guessing: is this trying to tell me that there are a countable number of computable reals, and that therefore, given any "chosen" real, I cannot make a decision? So is this something to do with axiom of choice? Or is this telling me that I can only work with a countable model of the reals? Perhaps this is some variation of Skolem's paradox? (Of course, I could take the time and educate myself, but that is not the point.)

Would you allow me to wander wildly off-topic? All standard results on computability are posed using Turning machines built from finite sets of symbols and finite sets of transition functions. There are interesting variants that provide alternate definitions involving the continuum. In this case, the number of transition functions is still finite, and so you can still "write algorithms" by composing transition functions. The state space itself, though, consists of function spaces on the continuum. Concrete examples include homogenous spaces, with the transition functions being operators. Most famously, operators acting on hilbert spaces, popularly referred to as "quantum computing", although the formal definitions extend to pretty much any kind of space with any kind of automorphisms acting on it. It's an arcane corner of ergodic theory, of topological dynamics (geometric dynamics, when the spaces are geometrical). So, just to pile it on: not only do I not understand indecomposability in some conventional sense of computability applied to representations (models???) of the continuum, but what if my model of computation is formulated in terms of operators (instead of finite state systems (on infinite tapes of finite symbols))? Is the word "model" inappropriate, here? Sorry for the diversion. I hope you found this at least mildly entertaining, as opposed to irritating. 67.198.37.16 (talk) 21:04, 13 July 2021 (UTC)[reply]