I have this question on the CS stackexchange to figure out how to model "a walk of a graph" in a custom formal language. I think the problem is that there is not just one walk of a graph but many (every possible walk). So I would like to learn what it looks like to write "the set of all walks of a graph" in formal logic notation. From there you can just say $w \in W$ (a walk is an element of all walks of the graph). Simple enough. A regular definition of a graph walk is:
A walk in a graph $G = (V, E)$ is a sequence of vertices $v_0, v_1, ..., v_n$ such that $\{v_i, v_{i+1}\} \in E$ for all $0 \leq i \lt n$.
In order to find the walks of the graph, one needs to have all possible subsets of the graph. Then filter the subsets so that you only have the ones where each pair of vertices in each subset are linked directly with an edge. It is over my head how you would write that in formal logic notation (i.e. no natural language, or minimal natural language). I would like to do that so I can see the computational tree structure of the symbols.
I was looking at Is there an algorithm to find all subsets of a set?, but the answer is incomplete:
Let $S = \{1,2,3\}$. The subsets of $S$ are all subsets of $\{1,2\}$ and all subsets of $\{1,2\}$ with the element $3$ appended to each subset...
Building off that, how would you write the formal logic form of "all subsets of vertices of the graph", and then follow up with "all walks of the graph" by taking a subset of the subsets? I guess the first part is writing the definition of a power set. Ah I guess that's not too bad!
$$P(S) = \{T : T \subseteq S\}$$
This is the powerset, now how to figure out the powerwalk.
Is something like this close?
$$\{X : \exists X \subseteq P(S), \forall v_1, v_2 \in X, \{v_1, v_2\} \in E\}$$
I think your trouble arises because you throw away the "temporal" structure of a walk; some vertices come before others. Instead, consider keeping it, and annotate each vertex with where it appears in the walk:
We usually interpret walks as functions $\mathbb{N}\to G$ (or, if you are only studying finite walks, functions from $\{0,1,\dots,N\}\to G$). Of course, not every such function is a walk, since it might "leap" from an unconnected vertex to another. But that is easy enough to remove: $$\text{Walks}(G)=\{f:(\forall n\in\mathbb{N})(f(n)\sim f(n+1))\}\subseteq(\mathbb{N}\to G)$$ where $\sim$ denotes the adjacency relation on the graph.
Since your CS stackexchange question seems to ask about enumeration, I'll add that this allows for an easy way to enumerate all possible walks:
First, store your graph in such a way that, given a vertex $v$, it is easy to compute the set $N(v)$ of all adjacent vertices. Then, iteratively build a list:
Note that this algorithm stratifies the set of infinitely many walks by length: to find all walks of length $n$, just run the "infinite" loop only $n$ times.
To connect my definition to powersets: then the trajectory of each walk (which vertices it hits, independent of order), is just the range of $f$. That is: $$\text{Trajectories}(G)=\{\{f(n):n\in\mathbb{N}\}:(\forall n\in\mathbb{N})(f(n)\sim f(n+1))\}$$ If you want to find the trajectory of each walk first, go for it. But I think figuring out whether an $f$ exists that marks out your set will be tricky. (In the finite case, at least, note that $f$ maps the natural order on $\mathbb{N}$ to a linear order on its trajectory. So maybe you can randomly direct the graph $S$ acyclically and see if it supports a total linear order?)