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!
Best Answer
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 "handle" also infinite domain; and in mathematical logic, we are interested primarily to handle with infinite domain.
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 is a (finite) conjunction, while an existetially quantified formula is a (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:
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 :
Its "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 the "decomposition" that we can perform only in term of the conncetives).
Thus, we are able to "discover" more logical truth than with "propositional decomposition".