3
$\begingroup$

In a propositional logic system for example, it is sound iff $\Gamma \vdash \varphi \implies \Gamma \vDash \varphi$ and complete iff $\Gamma \vDash \varphi \implies \Gamma \vdash \varphi$ (I don't know if this definition also happens to be the same in higher order logics).

Anyhow, what then does it mean for a system to be "consistent"? Is this the same as a logic system being complete or sound, or does it mean something else? Is it a syntactic claim? A semantic one?

$\endgroup$
9
  • 3
    $\begingroup$ I think you mean $\Rightarrow$ rather than $\Leftrightarrow$ $\endgroup$ Commented Nov 7, 2018 at 15:49
  • $\begingroup$ And "system" is a dangerous word to use here: a system of axioms is a very different thing from a proof system - the former is just a set of sentences (the "$\Gamma$") while the latter is a method for deriving sentences from sets of sentences (the "$\vdash$"). Conflating the two is an easy way to get quickly lost. $\endgroup$ Commented Nov 7, 2018 at 16:04
  • $\begingroup$ Yes I meant $\implies$, fixed, thanks $\endgroup$ Commented Nov 7, 2018 at 16:09
  • 1
    $\begingroup$ @user525966 To be super fussy: "A proof system $\vdash$ for propositional logic is complete, for the usual semantics $\models$, if for every theory $\Gamma$ and every sentence $\varphi$ we have $$\Gamma\models\varphi\implies\Gamma\vdash\varphi$$ (and same but with "$\implies$" switched around for sound)." $\endgroup$ Commented Nov 7, 2018 at 16:25
  • 1
    $\begingroup$ @user525966 Yup, that's correct! And sometimes we start with an alternate semantics and try to find a sound complete proof system for it, and other times we start with an alternate proof system and try to find a semantics with respect to which it's sound and complete. $\endgroup$ Commented Nov 7, 2018 at 16:48

1 Answer 1

Reset to default
6
$\begingroup$

A set of sentences or a theory is consistent if it does not contain a contradiction.

Consistency can be defined in either semantic or syntactic terms. The semantic definition states that the set is consistent if and only if it has a model, i.e., there exists an interpretation under which all formulas in the set are true.

In this case, we say also that the set is satisfiable

In the context of mathematical logic, where we consider a proof system and the corresponding relation of derivability ($\vdash$), we say that

a set $\Gamma$ of sentences is consistent if and only if there is no formula $\varphi$ such that both $\Gamma \vdash \varphi$ and $\Gamma \vdash \lnot \varphi$.

If $\bot$ is part of the language, the above amounts to saying that $\Gamma \nvdash \bot$.

To say that a proof system is sound means that only true formulas can be derived with it.

Thus, soundness implies consistency, because $\bot$ is not true.

Regarding completeness, we have that, in classical logic, where Ex falso holds, an inconsistent proof system is trivially complete : being inconsistent, it proves every formula, and thus also the valid ones.

$\endgroup$
4
  • 3
    $\begingroup$ I have never seen a good discussion, but there is an interesting thing with proof systems. It is possible that a proof system only proves logically valid formulas (so the system is sound when there are no hypotheses) but from some hypotheses it is possible to prove formulas that are not logically implied by those hypotheses (so the proof system is not sound for proofs with hypotheses). One example is a Hilbert style proof system for propositional logic augmented with a new rule of inference $P \vdash \bot$. The system is sound for formulas with no hypotheses because the new rule can't be used. $\endgroup$ Commented Nov 7, 2018 at 15:51
  • 3
    $\begingroup$ Note for the OP (and possibly others) that in a system of the type @CarlMummert describes, the deduction theorem - a principle we often take for granted - must fail. The occasional failure of the deduction theorem in interesting logics is a strange and interesting topic; see the discussion at this mathoverflow question, and in particular the linked paper by Blok and Pigozzi. $\endgroup$ Commented Nov 7, 2018 at 16:02
  • $\begingroup$ Re: the last paragraph: first, by "system" I think you mean "theory," and I think it's a good idea to avoid the overloaded term "system" in this context. It's also worth pointing out that some authors (this is e.g. the by-far-majority use in model theory, in my experience) use "complete" to mean "complete and consistent." $\endgroup$ Commented Nov 7, 2018 at 16:07
  • $\begingroup$ @user525966 We're allowed to use it, but we might never get the opportunity. That is, we're told "If you can derive $P$, then I'll go ahead and let you derive $\perp$ too" - but if we start out with a theory that can't derive $P$, we never get to invoke this clearly bonkers rule. $\endgroup$ Commented Nov 7, 2018 at 16:49

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.