Unsatisfiable Set minus Tautology is Unsatisfiable
Jump to navigation
Jump to search
Theorem
Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be an $\mathscr M$-unsatisfiable set of formulas from $\LL$.
Let $\phi \in \FF$ be a tautology.
Then $\FF \setminus \set {\phi}$ is also $\mathscr M$-unsatisfiable.
Proof
Suppose $\FF \setminus \set {\phi}$ were satisfiable.
Then by Satisfiable Set Union Tautology is Satisfiable, so would $\FF$ be, because:
- $\FF = \paren {\FF \setminus \set {\phi} } \cup \set {\phi}$
by Set Difference Union Intersection and Intersection with Subset is Subset.
Therefore, $\FF \setminus \set {\phi}$ must be unsatisfiable.
$\blacksquare$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.5.2$: Theorem $2.47$
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.10$: Exercise $2.15$