3
$\begingroup$

Given that $\Sigma\vdash\phi \Leftrightarrow \Sigma\vDash\phi$, I want to prove: $\Sigma \text{ satisfiable} \Leftrightarrow \text{ every finite subset of } \Sigma \text{ is satisfiable}$.

I will post my idea below, but I can't quite finish the $\Leftarrow$ direction. I would need that the set which I will call $\Delta$ is finite. Can someone point out what I'm missing please? Thank you very much.

Proof: The $\Rightarrow$ direction holds because if $\Sigma$ is satisfiable it has a model, which in turn is a model of every (especially every finite) subset of $\Sigma$.

$\Leftarrow$: Proof by contradiction. If $\Sigma$ is not satisfiable, then it isn't consistent. I.e. $\Sigma \vdash \bot$. This means that there is a subset $\Delta$ of $\Sigma$ from which $\bot$ is derivable. Correctness then gives $\Delta \vDash\bot$, i.e. for every model $\mathscr{A}$ one has that $\mathscr{A}\vDash\Delta$ gives $\mathscr{A}\vDash\bot$. But the last statement applies for no model, so we already have $\mathscr{A}\not\vDash\Delta$ for every $\mathscr{A}$, meaning that $\Delta$ has no model. If I knew that $\Delta$ was finite, then I would have a contradiction.

$\endgroup$
2
  • 3
    $\begingroup$ Every proof uses only finitely many statements from $\Sigma$. $\endgroup$
    – Dustan Levenstein
    Feb 3, 2016 at 19:32
  • 1
    $\begingroup$ If $\Sigma\vdash\bot$ then there is a finite $\Delta\subseteq\Sigma$ such that $\Delta\vdash\bot$. $\endgroup$
    – BrianO
    Feb 3, 2016 at 19:32

1 Answer 1

Reset to default
5
$\begingroup$

Hint: call $n$ the length of a proof of $\bot$ from $\Sigma$. Then, at most $n$ formulas of $\Sigma$ appear in the proof. Set $\Delta=\{\gamma\in\Sigma: \text{$\gamma$ appears in the given proof of $\bot$ from $\Sigma$}\}$. Then $\Delta$ is finite and $\Delta\vdash\bot$.

$\endgroup$
4
  • $\begingroup$ Is there an intuitive reason why a proof has to be finite? $\endgroup$
    – azureai
    Feb 3, 2016 at 19:49
  • 2
    $\begingroup$ I'm not sure what your definitions are, but in most cases, formulas are defined to be finite, if proofs could be infinitely long, then that'd contradict the finiteness of a formula (as you could construct infinite formulas from proofs). $\endgroup$
    – YoTengoUnLCD
    Feb 3, 2016 at 19:53
  • 3
    $\begingroup$ It will be provable from the formal definition of a derivation/formal proof. For example, one book might say that a derivation is a finite sequence of formulas such that each formula is an axiom, an assumption, or derivable form previous formulas by modus ponens. Another book might define a derivation to be a finite tree of a particular kind. There are logics other than first-order logic where a proof may involve infinitely many formulas, but in those logics compactness does not generally hold. @see $\endgroup$
    – Carl Mummert
    Feb 3, 2016 at 20:29
  • $\begingroup$ @Carl Mummert Thank you for the elaboration. $\endgroup$
    – azureai
    Feb 3, 2016 at 20:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .