Re-expressing a statement in First Order Logic in Propositional Logic From what I understand a propositional variable must represent a statement (either true or false). If so, eliminating free variables from any predicate by either:
(1) Replacing free variables with constants 
(2) Binding free variables with quantifiers 
should allow us to create statements in FOL that can be expressed in propositional logic (as long as these are named by propositional variables).
However, I remember reading somewhere that in propositional logic statements represented by propositional variables have to be about specific objects. For example, letting some $Q$ stand for "$Shoe_1$ is green" rather than "All shoes are green". So that if we had a finite, known domain in FOL, and wished to express the following statement in propositional logic:
$(\forall x) (x$ is a shoe $\wedge$ $x$ is green)
we'd have to convert it as: ($Shoe_1$ is a shoe $\wedge$ $Shoe_1$ is green) $\wedge$ ($Shoe_2$ is a shoe $\wedge$ $Shoe_2$ is green)  $\wedge$ ... $\wedge$ ($Shoe_n$ is a shoe $\wedge$ $Shoe_n$ is green)
instead of letting some propositional variable $P$ stand for "All shoes are green".
Is this accurate? I'm a beginner so I apologize for any vagueness in the question. Thanks!
 A: Some comments:
(i) In propositional logic, a propositional variable stands for a sentence, i.e. something that can be true or false.
This is the reason why, starting from a first-order formula, we have to remove free variables; a well-formed f-o formula like "$x$ is green" (i.e. $green(x)$) is not a sentence, because we cannot say, without assigning a reference to $x$, if it is true or false.
Thus, we have to do one of the two thing mentioned by you: either replace $x$ with a constant ( a "name") or bind the variable with a quantifier.
(ii) $\forall x green(x)$ is a prefectly understandable sentence: "all objects are green".
You are right in saying that in a finite domain, $\forall x green(x)$ is equivalent to : $green(c_1) \land \ldots \land green(c_n)$.
But with first-order logic we are interested to describe also infinite domain; and in mathematical logic, we are involved primarily with infinite domains and we do not (usually) admit as well-formed formulae infinite long expressions (but see Infinitary Logic).
If we restrict ourselves to finite domain, an universally quantified formula can be reduced to a finite conjunction, while an existetially quantified one to finite disjunction.
Thus, if we restrict ourselves to finite domain, we can simply dispense with quantifiers.
(iii) Having said that, what is the purpose of "downsizing" a first-order formula to a propositional one?
This technique can be useful in order to show that a f-o formula is valid: if the "propositional translation" of a f-o formula is a tautology, we are sure that the original f-o formula is valid.
Consider for example the (obviously) valid formula:

$\forall x (x=0) \lor \lnot \forall x (x=0)$;

we can translate it as $p \lor \lnot p$, that is a tautology: thus, the original f-o formula is valid.
But we have valid formulae that are not instances of tautologies; consider :

$\forall x (x \ge 0) \rightarrow (0 \ge 0)$.

Its propositional translation is $p \rightarrow q$, that is not a tautology.
This fact must be obvious: first-order language as a greater expressive power than propositional language; with f-o language we can perform a deeper decomposition of the logical structure of sentences, compared to that performed in terms of propositional conncetives.
Thus, in f-o logic we have more logical truth than with propositional logic.
