How to prove completness of my axioms for Wumpus world game

Question

I have an implementation of Wumpus world game with some specific rules. Basically, you are an agent which does not see adjacent tiles. There are pits and exactly one wumpus. Moving into pit or tile occupied by alive wumpus kills the agent. You may deduce the presence of pit or wumpus according to given perception.

Agent on tile $[x,y]$ perceives a breeze iff at least one of the adjacent tiles $[x-1,y]$, $[x+1,y]$, $[x,y-1]$, $[x,y+1]$ is a pit.

Agent on tile $[x,y]$ perceives a stench iff exactly one of the adjacent tiles $[x-1,y]$, $[x+1,y]$, $[x,y-1]$, $[x,y+1]$ contains a wumpus.

I came out with several axioms/rules for deducing whether a tile is safe (i.e. not containing alive wumpus and it is not a pit). I have tested my implementation on various maps and it worked correctly: i.e. if a tile was safety and reachable from agent's starting position, agent deduced it and visited it. I am very curious whether this "completeness" of agent's axioms can be proved in general.

That is, is there a way to prove the following implication?

$Map \models safe(x, y)$ implies $Map\vdash safe(x,y)$

where:

• $Map$ is a finite FOL theory describing map. For example $Map = \{agent(1,1), clean(2,1), wumpus(3,1)\}$
• $safe(x,y)$ is a predicate which holds iff tile at $[x,y]$ does not contain an alive wumpus or pit
• deductive system consists of my agent's axioms and uses Modus ponens as inference rule

Answer 1

What if the world has two large empty rooms each surrounded by pits but which are connected by a long narrow hallway which is flanked by pits on either side. Even though the rooms each contain safe tiles and the rooms are reachable from each other, your agent will not walk through the breezy hallway unless it is feeling very brave.