Semantic consequence

Question

I'm studying refutation trees in computer science II, but I have a big doubt:

Let $\Gamma, \Psi \subseteq F_m$

Is the following hypothesis true?

$\Gamma \vDash \Psi \iff \not\vDash\{\Gamma,\lnot \Psi\} \iff \vDash (\Gamma\rightarrow \Psi) \iff \not \vDash \lnot(\Gamma \rightarrow \Psi)$

i.e.:

Let $A, B, C \subseteq F_m$ such that $\{A\rightarrow B, \lnot B \rightarrow\lnot C\} \vDash A \rightarrow C$

Then, to prove this I can apply:

$\{A\rightarrow B, \lnot B \rightarrow \lnot C, \lnot (A \rightarrow C)\}$ is unsatisfiable $\implies \not \vDash ((A\rightarrow B) \land (\lnot B \rightarrow \lnot C) \land \lnot ( A \rightarrow C ) )$

Or I can use:

$\not \vDash \lnot (((A\rightarrow B) \land (\lnot B \rightarrow \lnot C)) \rightarrow (A \rightarrow C))$

So, this is true?

Thanks!

Answer 1

About your question, it is correct to say that, according to the definition of logical consequence, in order to prove that :

${A→B,¬B→¬C} \vDash A→C$,

we have to show that :

$\{ A→B, ¬B→¬C, ¬(A→C) \}$ is unsatisfiable.

We have that :

$\varphi$ is unsatisfiable iff $\lnot \varphi$ is (universally) valid.

Note. When $\varphi$ is valid, we write : $\vDash \varphi$.

A set $\Gamma$ of formulae is unsatisfiable iff there is no valuation that "makes true" simultaneously all formulae in $\Gamma$.

If $\Gamma$ is a finite set of ($n$) formulae, this amount to the unsatisfiability of the conjunction of the formulae $\gamma_i \in \Gamma$, $i \le n$.

Thus, $\Gamma$ finite is unsatisfiable iff $\lnot (\gamma_1 \land ... \land \gamma_n)$ is valid.

In conclusion, $\{ A→B, ¬B→¬C, ¬(A→C) \}$ is unsatisfiable iff :

$\vDash \lnot ((A→B)∧(¬B→¬C)∧¬(A→C))$.