3
$\begingroup$

Given some first-order language and a set of axioms therefrom one still needs to specify a deductive system to turn it into a full-fledged first-order theory.

Currently I'm under the following impression. There are weaker and stronger deductive systems but there is actually a formalization of what it means for a system to be "good", i.e. "of the same strength as unformalized deductive reasoning". The definition calls for the system to be "sound" and "complete". Naturally, for any system with this quality the set of derivable formulas is the same. Furthermore, the most widely considered formal deductive systems are indeed such.

Now, a couple of citations from Wikipedia.

"A deductive system is sound if any formula that can be derived in the system is logically valid. Conversely, a deductive system is complete if every logically valid formula is derivable."

"A formula is logically valid (or simply valid) if it is true in every interpretation."

Are those really the correct definitions? I just can't wrap my head around the resulting definition of completeness. I mean: "every interpretation"?! That's one inconceivable proper class! How on earth could one then prove the completeness of some system?

$\endgroup$
3
  • $\begingroup$ What do you mean by " of the same strength as unformalized deductive reasoning."? $\endgroup$
    – Willemien
    Sep 13, 2014 at 12:09
  • $\begingroup$ This particular phrase is not intended to have any mathematical meaning, I even considered enquoting it. $\endgroup$
    – imakhlin
    Sep 13, 2014 at 12:29
  • $\begingroup$ From my naive point of view, one of the primary goals of proof theory is to formalize the concept of a logically sound argument. Once we've formalized the concept of a "statement" (a closed well formed formula) we still have an intuitive understanding of when one statement follows logically from a set of other statements. A deductive system which complies with that understanding can be said to be "of the same strength as unformalized deductive reasoning". As I said, no formal meaning behind these words. $\endgroup$
    – imakhlin
    Sep 13, 2014 at 12:43

1 Answer 1

Reset to default
4
$\begingroup$

Happily, we don't have to worry about this, at least in the first-order case.

Given a standard deductive system $S$ for classical logic, we know from the appropriate version of the so-called completeness theorem (not worrying about the label just for the moment) that if $\Gamma$ is a set of first-order sentences, and $\varphi$ is a first order sentence, then

If $\Gamma \nvdash_S \varphi$ then there is a countable model -- an interpretation in the natural numbers -- which makes $\Gamma$ all true and $\varphi$ false.

Which is certainly enough to show that

If $\Gamma \nvdash_S \varphi$ then there is a model in your favourite inclusive sense which makes $\Gamma$ all true and $\varphi$ false.

so long as the set or class of models in your favourite inclusive sense include those tiddly little countable models!

Contraposing,

If every model in your favourite inclusive sense which makes $\Gamma$ all true makes $\varphi$ true, then $\Gamma \vdash_S \varphi$.

So $S$ is complete with respect to semantic consequence defined in terms of models in your favourite inclusive sense, however you define them, so long as you include the tiddly little countable ones. Even if you go for a whopping bigger-than-set-sized class of models. So you don't need to worry, even if you allow a proper-class seized collection of models, everything stays under control!

$\endgroup$
3
  • $\begingroup$ Thanks, that was semi-enlightening. A couple of questions though. So we can actually leave the definitions as cited in my question? And you are saying that many specific deductive systems $S$ can be shown to satisfy these three theorems and thus be complete? $\endgroup$
    – imakhlin
    Sep 13, 2014 at 13:17
  • $\begingroup$ Those theorems are not general statements holding for a wide class of $S$'s, are they? (They are certainly false for an empty $S$ =)) They are to be approached as separate results for every specific $S$, correct? $\endgroup$
    – imakhlin
    Sep 13, 2014 at 13:19
  • 1
    $\begingroup$ @IgorMakhlin - Yes and Yes. There are lots of proof system : Natural Deduction, Tableau, Sequent Calculus and many different version of Hilbert-style (axioms + rules of inference); we agrre to use them only because we are able to prove a (specific) Soundness and Completeness Theorme for each of them. $\endgroup$
    – Mauro ALLEGRANZA
    Sep 13, 2014 at 14:34

You must log in to answer this question.

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