I have the following conjecture:
Definition. A topological space $(X,T)$ is connected iff there does not exist disjoint open sets $U,V\in T$ such that $U\cup V=X$.
Definition. A path $f$ between points $x,y\in X$ in a topological space $(X,T)$ is a continuous function $f:[0,1]\to X$, such that $f(0)=x$ and $f(1)=y$.
Conjecture. A topological space $(X,T)$ is connected iff for all $x,y\in X$ there exists a path between $x$ and $y$.
I find it easy to prove the $\impliedby$ part: simply invert the implication: Assume $(X,T)$ is disconnected, so that we have disjoint $U,V\in T$ s.t. $U\cup V=x$. Then pick any $x\in U$ and $y\in V$. Now assume that we have a function $f[0,1]\to X$ with $f(0)=x$ and $f(1)=y$. This function cannot be continuous, and hence cannot be a path, because continuity implies for all open sets $O$ in $X$, $f^{-1}(O)$ must be open in $([0,1],S)$. But we know that in the latter topology, there is no open set whose complement is also open (i.e. it is connected), hence either $f^{-1}(U)$ or $f^{-1}(V)$ must not be open, so $f$ cannot be continuous. Hence there is no path between $x$ and $y$.
But it seems to me that proving the direction $\implies$ is fundamentally harder, in the sense of needing more (logical?) machinery. e.g. I suspect maybe we need something like the axiom of choice? My question is whether this is true, and if so, what kind of logical assumptions do we need to prove the $\implies$ part that we don't need for the $\impliedby$ part.
My thought is as follows: If we want to do a constructive proof, then for the $\impliedby$ part, we only need to construct a points $x\in U$ and $y\in V$. But for the $\implies$ part, we need to construct a function: Based on the assumption that no disjoint $U,V\in T$ with $U\cup V=X$ exist, we need to construct a path for arbitrary $x,y\in X$. But constructing such a path, seems to me, to be in some sense incomputable? In the $\impliedby$ part, given open sets $U,V$, we can just pick arbitrary points from $U$ and $V$. But for $\implies$, given that no such $U,V$ exist, we can't just pick arbitrary paths $f$, and it is not obvious to me how you would make a general algorithm for constructing them. Given that such paths are essentially uncountable, it seems plausible to me that this construction literally cannot be done. Hence I conjecture that we need more than constructive logic for proving the $\implies$ part, even though the $\impliedby$ part can suffice with constructive logic.
Questions:
Is my idea that we cannot construct such paths correct? Can this be made more precise?
How do we prove the $\implies$ part? i.e. what additional logical assumptions do we need beyond constructive logic? Axiom of choice? Law of excluded middle?
Your conjecture is not correct. Any path connected space is connected, but there are connected spaces that are not path connected. One such example is the union of the $y$ axis with the graph of $\sin(1/x)$.