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.
Best Answer
"$\vee$" by itself is inclusive or. To express exclusive or, we need to write a more complicated expression.
Remember that "$A$ xor $B$" just means "$A$ or $B$, but not $A$ and $B$." With that in mind, "$A$ xor $B$" can be expressed as $$(A\vee B)\wedge\neg(A\wedge B).$$ Another useful way to express it is $$(\neg A\wedge B)\vee(A\wedge\neg B).$$ It's a good exercise to check that these two expressions are in fact equivalent.