Propositional Logic and First-Order Logic I am having a hard time distinguishing between the two different logics.  If we consider the statement, “Squares adjacent to the Wumpus are smelly,” and are asked to express it as First-Order Logic, we can express First-Order Logic as so:
\begin{gather}
\forall x,y.\left(\left(\mathit{Square}(x) \land \mathit{Wumpus}(y) \land \mathit{Adjacent}(x,y)\right) \to \mathit{Smelly}(x)\right) \\
\forall x,y,a,b.\mathit{Adjacent}([x, y],[a, b]) \leftrightarrow (x= a  \land (y=b-1 \lor (y=b+1)) ) \lor (y=b \land (x=a-1 \lor (x=a+1)) )
\end{gather}
But I have friends who expressed their answers as so:
$$ \forall x,y. \mathit{Wumpus}([x, y]) \leftrightarrow \mathit{Smelly}([x - 1, y]) \land Smelly([x + 1 , y]) \land \mathit{Smelly}([x , y - 1]) \land \mathit{Smelly}([x , y + 1]) $$
My argument that their answers are not First-Order Logic, but rather Propositional Logic because there is a need to repetitively write $\mathit{Smelly}$ for all tiles that are smelly. I think my argument might be a little vague.
So, is the answer provided by my friend correct and why?
 A: Both formalizations of the sentence are in first-order logic.  The propositional calculus does not contain quantification, so something starting with $\forall x,y \dots$ isn't a propositional formula.  
However, you have hit upon an interesting point.  When the domain of discourse is known to be finite, e.g., the set $\{a,b,c\}$, then we can replace the formulae
$$ \forall x.\phi(x) \qquad \exists x.\phi(x)$$
with the equivalent formulae
$$ \phi(a) \land \phi(b) \land \phi(c) \qquad \phi(a) \lor \phi(b) \lor \phi(c)$$
When the domain is fixed, you can use this technique to remove quantifiers from all your formulae.  For instance, in a smaller domain, $\{a,b\}$, the sentence
$$ \forall x.\exists y.P(x,y) $$
can be replaced first by 
$$ \exists y.P(a,y) \land \exists y.P(b,y) $$ 
which in turn is replaced by 
$$ (P(a,a) \lor P(a,b)) \land (P(b,a) \lor P(b,b)) $$ 
Here we have an opportunity to replace some sentences in first-order logic with sentences in the propositional calculus.  We can replace each first-order ground literal with a propositional symbol, and turn the previous sentence into 
$$ (P_{a,a} \lor P_{a,b}) \land (P_{b,a} \lor P_{b,b}) $$
which is in the propositional calculus.
To propositionalize a Wumpus world, you would take your grid (for ease, let's assume it's 3×3), and identify each cell in the grid:
\begin{array}{|c|c|c|}
\hline A & B & C \\
\hline D & E & F \\
\hline G & H & I \\
\hline
\end{array} 
Now, instead of the arithmetic based definition of adjacent, you simply have the long propositional formula:
\begin{gather}
\lnot A_{A,A} \land A_{A,B} \land \lnot A_{A,C} \land A_{A,D} \land \lnot A_{A,E} \land \dots \land \\
A_{B,A} \land \lnot A_{B,B} \land A_{B,C} \land \lnot A_{B,D} \land A_{B,E} \land \dots \land \\
\dots
\end{gather}
You can keep applying this process to your other definitions, and entirely propositionalize the formalization of the domain.  The number of sentences will be much bigger, but there are very efficient propositional reasoners, so in some cases the translation can be justified.
