If $\Gamma$ is an infinite set of propositional formulas, is the statement: "$\Gamma$ is satisfiable" decidable?
Here, $\Gamma$ is satisfiable means that there exists a truth function $v$ such that $v(\gamma)=$ True for all $\gamma \in \Gamma$.
Here are some facts I know:
- The set of all propositional formulas is countable (our alphabet is either finite or countable), so $\Gamma$ is countable.
- The compactness theorem tells us that $\Gamma$ is satisfiable if and only if every finite subset, say $\Delta$, of $\Gamma$ is satisfiable.
- The set of all finite subsets of a countable set is itself countable, and the satisfiability of any finite set of propositional formulas is a decidable question (we can use truth tables).
I was only able to prove:
"$\Gamma$ is unsatisfiable" is semi-decidable.
$\Gamma = \bigcup_{n \in \mathbb N} \Delta_n$, where each $\Delta_n$ is finite. We define a procedure $P$ that for each $i \in \mathbb{N}$ checks whether $\Delta_i$ is satisfiable using the truth-table method. If $\Delta_i$ is satisfiable then it iterates the process with $\Delta_{i+1}$. If $\Delta_i$ is unsatisfiable it halts and returns unsatisfiable.
This a common exercise, and the answer is "no". There is no algorithmic method that takes a set $\Gamma$ of propositional formulas, in the variables $A$ and $B$, and tells whether the set is satisfiable. Here the method would use the set of formulas as an oracle, meaning that it can ask questions of the form "is this formula in the set?". The method would need to return a correct value "satisfiable" or "unsatisfiable" for every set of formulas.
The proof that there is no such method is by contradiction, using a diagonalization. Given the method, $e$, we can make a set of formulas $\Gamma_e$ that is satisfiable if and only if method $e$ says that $\Gamma_e$ is not satisfiable.
Begin by putting $\lnot A$ into $\Gamma_e$, along with all the formulas $B$, $B\land B$, $B \land B\land B$, etc. Call that set of formulas $S_e$. Now, we begin to algorithmically simulate what method $e$ would do if we ran it on $S_e$. By assumption, method $e$ will eventually halt and say "satisfiable" or "unsatisfiable". By simulating it long enough, we can tell which of these happens. If method $e$ says $S_e$ is "unsatisfiable", we let $\Gamma_e = S_e$, and method $e$ is wrong, because $S_e$ is satisfiable.
If method $e$ says that $S_e$ is satisfiable, we look at all the formulas that method $e$ actually looked at when making that determination. We can form this list effectively, by simulating method $e$ until it halts. There can only be finitely many such formulas that it looks at, because it only runs finitely many steps before halting. So we can find a formula $\phi \equiv B \land B \land \cdots \land B \land A$ that method $e$ never looked at when we ran it. We now let $\Gamma_e = S_e \cup \{\phi\}$. Then $\Gamma_e$ is a computable set of formulas, and method $e$ will say that $\Gamma_e$ is satisfiable, although it is not. (Although this is not vital to the proof, there is actually a single algorithm that computes $\Gamma_e$ given any input $e$).
We can do a similar thing with just one variable, actually. The important point is that, even with just one variable, there are an infinite number of possible propositional formulas, e.g. $A$, $A \land A$, $A \land A \land A$, ...