What the program was actually doing

The Logic Theorist started with a goal and a list of allowed moves.

Imagine a tiny version. The program starts at A and needs to reach D. Its rules say that A can become B or C, and C can become D.

The program tries one path. A becomes B, but B leads nowhere. So it goes back and tries the other choice. A becomes C, then C becomes D.

It reached the goal using only allowed moves. That chain of steps is the proof.

The real symbols and rules were more complicated, but the process was the same: try a promising step, go back if it fails, and stop when the target is reached.