Construct a calculus which produces exactly all pairs $(S,t)$, such that $free(t)=S$. This calculus will operate on pairs $(S,t)$, where $S$ is a set of variables and t is a term.
I've got an understanding of free vs bound variable.
for instance, $x^y$, $x$ is bound and $y$ is free.
If I understand the rule or rules I construct for this calculus will be such that any term $t$ will contain all free variables that are in contained in $S$ and any term in $S$ will satisfy this.
I'm not sure what rules I need exactly, maybe
a rule to construct variables, and a rule that generates terms with some n-ary function. But anything quantified is bounded so then that variable is no longer free.
Note that in a term all variables are free. So the following calculus will do:
$${\over (\{v_n\}, v_n)} $$ where $v_n$ is a variable. $${\over (\emptyset, c)}$$ where c is a constant symbols. $${(S_1, t_1) \\ \dots \\ (S_n, t_n) \over ( \bigcup_i S_i, ft_1\dots t_n) }$$
where f is an n-ary function symbol.