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.

  • 3
    $\begingroup$ Every proof uses only finitely many statements from $\Sigma$. $\endgroup$ – Dustan Levenstein Feb 3 '16 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 '16 at 19:32

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$.

  • $\begingroup$ Is there an intuitive reason why a proof has to be finite? $\endgroup$ – azureai Feb 3 '16 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 '16 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 '16 at 20:29
  • $\begingroup$ @Carl Mummert Thank you for the elaboration. $\endgroup$ – azureai Feb 3 '16 at 20:59

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.