Looking at the Boolean Satisfiability Problem, this says that given a Boolean expression $P(x_1,x_2,...x_j)$, find values where it is true.
Now, suppose we want to find the shortest algorithm for a boolean expression with $j$ symbols.
So we need to find both the set of Boolean expressions with $N$ symbols, and the set of algorithms with $M$ symbols and depth $D$.
If $B_n$ be the set of boolean expressions of length $n$ I guess we could build this recursively as something like $$B_{n+m} = B_n \land B_m \cup B_n \lor B_m $$
$B_0$ would be just the set of variables themselves.
Then presumably, as algorithms can be implemented by binary computers and (perhaps) can be encoded as boolean expressions, the algorithms $A_n$ of n symbols can be built up in the same way. The difference being we want $j$ truth values as an output. So let $C^j_n$ be the set of expressions that output an array of $j$ truth values using n symbols. (The algorithm $A$ would take as it's input the boolean expression $P$ but this could be encoded into binary in an easy way so it would just be a list of $k$ binary values).
So if $P_n$ be a boolean expression with up to $n$ symbols, how would we write that there is an algorithm of length $f(n)$ that can find a solution? (Yes, this is not the P vs NP problem).
Something like this(?): $$\exists A \in C^j_{f(n)}:\forall P\in B_n : P_n(A(P_n))$$
(Translated as: 'there exists an algorithm, $A$, such that for any P of length $n$ it gives a solution).
Really I'm intersested in how you would create sets of expressions in set theory. i.e. something you could put into a proof assistent.