I am stuck at the following problem:

Let $\varphi$ be a sentence in a predicate calculus $T$ and $\Sigma$ a set of sentences in $T$. Show that $\Sigma \vdash\varphi$ if and only if $\Sigma\,\cup \{\neg\varphi\}$ is inconsistent.

My attempt:

$(\Leftarrow)$ Suppose $\Sigma\,\cup \{\neg\varphi\}$ is inconsistent, then there exists a formula $\psi$ such that $\Sigma\,\cup \{\neg\varphi\}\vdash\psi$ and $\Sigma\,\cup \{\neg\varphi\}\vdash\neg\psi$.

$(\Rightarrow)$ Suppose $\Sigma \vdash\varphi$. Then, since every theorem of predicate calculus is logically valid, $\varphi$ is logically valid. Then $\neg\varphi$ is not satisfiable.

$\Sigma\,\cup \{\neg\varphi\}\vdash\psi$ and $\Sigma\,\cup \{\neg\varphi\}\vdash\neg\psi$

$\Sigma\,\cup \{\neg\varphi\}$ is inconsistent


If you are allowed to use soundness and completeness theorems (which hold not only in propositional logic but also in first-order logic), the proof is quite easy.

$\Leftarrow$: Suppose $\Sigma \cup \{\neg\varphi\}$ is inconsistent, then there exists a formula $\psi$ such that $\Sigma \cup \{\neg\varphi\}\vdash\psi$ and $\Sigma\,\cup \{\neg\varphi\}\vdash\neg\psi$. By soundness theorem, $\Sigma \cup \{\neg\varphi\} \models \psi$ and $\Sigma \cup \{\neg\varphi\}\models \neg\psi$, which means that every model of $\Sigma \cup \{\neg\varphi\}$ satisfies both $\psi$ and $\lnot \psi$. Now, by definition, there is no structure in first-order logic that satisfies a formula and its negation. Therefore, there is no model of $\Sigma \cup \{\neg\varphi\}$, which means that every model of $\Sigma$ is a model of $\varphi$ as well, i.e. $\Sigma \models \varphi$. According to completeness theorem, $\Sigma \vdash \varphi$.

$\Rightarrow:$ Suppose $\Sigma \vdash \varphi$. Then, $\Sigma \cup \{\lnot \varphi\} \vdash \varphi$, according to the weakening property (which holds in any deduction system for "traditional logics"). But $\Sigma \cup \{\neg\varphi\} \vdash \lnot \varphi$ as well, since $\lnot \varphi \in \Sigma \cup \{\neg\varphi\}$. Hence, $\Sigma \cup \{\neg\varphi\}$ is inconsistent. $\qquad\square$

Note the your use of the soundness theorem in your original post is not correct, or at least not well-written: according to soundness theorem, $\Sigma \vdash \varphi$ does not imply that $\varphi$ is logically valid (a formula is logically valid iff every structure satisfies it), but it implies that every model of $\Sigma$ satisfies $\varphi$ (it is possible that $\Sigma$ has no models and $\varphi$ is unsatisfiable as well).

Roughly, weakening property says that if you can prove something starting from some hypothesis $\Sigma$, you can prove it even when you add more hypotheses to $\Sigma$.

If you are not allowed to use soundness and correctness theorems, the proof of ($\Leftarrow$) is slightly more technical and it depends on the deduction system and the inference rules you are allowed to use. This means that soundness and completeness theorems are not necessary to prove ($\Leftarrow$) but they simplify the proof and also they "universalize" the proof, in the sense that by appealing to these theorems the proof of ($\Leftarrow$) does not depend explicitly on the deduction system and the inference rules you are allowed to use.

Anyway, if the deduction system you are using is Hilbert system with the axiom $(\lnot \varphi \to \lnot \psi) \to ((\lnot \varphi \to \psi) \to \varphi)$ (as the systems described in Mendelson's book, pp. 35 and 69 for propositional and first order logic, respectively), you can easily prove $(\Leftarrow)$ as described in this post, without appealing to the semantic notions involved in soundess and completeness theorems.

  • $\begingroup$ I understood the first one, but I don't know if it's okay for us to use weakening property, since we didn't cover it in class $\endgroup$ – Leyla Alkan Nov 27 '18 at 14:19
  • $\begingroup$ @LeylaAlkan - Which deduction system are you using? I guess you are using Hilbert system and if it is so, weakening is a trivial property which follows immediately from the definition of derivation in such a system. $\endgroup$ – Taroccoesbrocco Nov 27 '18 at 14:20
  • $\begingroup$ What do you mean by deduction system? We are basically following Mendelson's book $\endgroup$ – Leyla Alkan Nov 27 '18 at 14:26
  • $\begingroup$ @LeylaAlkan - Yes, it is also called Hilbert system. The first property of this system proved in Mendelson's book is exactly weakening (p. 35, point 1). $\endgroup$ – Taroccoesbrocco Nov 27 '18 at 14:30

Suppose $\Sigma \vdash \varphi$. Trivially $\neg\varphi \vdash \neg\varphi$. So $\Sigma, \neg\varphi \vdash \varphi \land \neg\varphi$. Therefore $\Sigma, \neg\varphi \vdash \bot$, so $\Sigma, \neg\varphi$ is (syntactically) inconsistent.

Suppose $\Sigma, \neg\varphi$ is (syntactically) inconsistent, i.e. $\Sigma, \neg\varphi \vdash \bot$. Then $\Sigma \vdash \neg\varphi \to \bot$. Whence $\Sigma \vdash \neg\neg\varphi$. Whence, classically, $\Sigma \vdash \varphi$.

There are some details you'll need to fill in depending on the proof-system that you have available (the one that defines the relation symbolized by '$\vdash$'). But you won't need to appeal to soundness and completeness if syntactic consistency is in question. All you need are some simple properties of the relevant proof system.

If semantic consistency is in question then, yes, you'll need the soundness and completeness results that link the syntactic and semantic notions. But is very important for questions like this to be clear which notion of consistency is in question. (Your single turnstile is conventionally the sign for the syntactic proof relation, so this naturally goes along with the notion of syntactic consistency -- classically, not proving $\bot$, or not proving an explicit contradiction, or not proving every sentence.)


Neither for $\Leftarrow$ nor for $\Rightarrow$ is it necessery to involve semantics. The exact derivations depend on the particular deduction system you are using, but the general structure will be as follows.

For $\Leftarrow$, continue with deriving $\Sigma \cup \{ \lnot \phi \} \vdash \psi \land \lnot \psi$. Therefore $\Sigma \vdash \lnot \phi \to (\psi \land \lnot \psi)$. So $\Sigma \vdash \lnot \lnot \phi$ and therefore $\Sigma \vdash \phi$.

For $\Rightarrow$, you already have $\Sigma \vdash \phi$ and therefore also $\Sigma \cap \{ \lnot \phi \} \vdash \phi$. Of course, also $\Sigma \cup \{ \lnot \phi \} \vdash \lnot \phi$. Together you can use this to derive $\Sigma \cup \{ \lnot \phi \} \vdash \psi$ for an arbitrary $\psi$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.