Im having some difficulties trying to move from first order logic to more general "first order theories". The literature is not very consistent on the election of terminology, notation, deductive systems, semantics, etc.

Im currently reading Mendelson, where a first order theory is defined to be:

Let L be a first-order language. A first-order theory in the language L will be a formal theory $K$ whose symbols and wfs are the symbols and wfs of L and whose axioms and rules of inference are specified in the following way. The axioms of $K$ are divided into two classes: the logical axioms and the proper (or nonlogical) axioms.

(Then he proceeds to list axioms and rules)

In Mendelson a "theory" is not treated as a set, the deductive system is not separated from the theory part. Then any theory $K$ for any subject matter is also a first order logic. And if no axioms are present then $K$ is a "pure first order theory". If $\alpha$ is probable from a theory $K$, is written $\vdash_K \alpha$.

Consider the following (meta)lemma 2.12:

If a closed wff $\neg\alpha$ of a theory $K$ is not provable in $K$, and if $K'$ is the theory obtained from $K$ by adding $\alpha$ as a new axiom, then $K'$ is consistent.

In symbols:

$$\text{If} \ \ \not\vdash_K \neg\alpha \ \ \text{then} \ \ K+\alpha \ \ \text{is consistent} \label{a}\tag{1}$$

On the other hand, from what i have seen, other (maybe more "modern") treatments define a "theory" to be something quite different and more concrete, typically just some set. A definition in this sense would be something along the lines of (fixing underlying deductive system):

  • A theory $T$ is a set of sentences.
  • The theorems of $T$ is the smallest set of formulas containing $T$ and the logical axioms closed under the inference rules.

If $\alpha$ is probable from a theory $T$, is written $T \vdash \alpha$.

Now, what would be our equivalent of (1)?. I think is the same as saying for any theory $T$ and sentence $\alpha$:

$$\text{If} \ \ T \not\vdash \neg\alpha \ \ \text{then} \ \ T\cup\{\alpha\} \ \ \text{is consistent} \label{b}\tag{2}$$

Is this translation correct?. Is it just a matter of treat the theory explicitly as a set and express the theory deductions as logical consecuence?

But in this setting i dont see any special reason to talk about theories here, we can establish this fact for any set of sentences $\Gamma$ (ie. ignore if $\Gamma$ is intended to be a "theory"):

$$\text{If} \ \ \Gamma \not\vdash \neg\alpha \ \ \text{then} \ \ \Gamma\cup\{\alpha\} \ \ \text{is consistent} \label{c}\tag{3}$$

But now i wonder if this have the same meaning as (1) or (2), because here if $\Gamma$ is a set of axioms then will be treated just like hypothesis by the meaning of $\vdash$, and i dont know if that is a problem....

As a related example, consider the so called "Strong Soundness/Completeness" wich is stated as:
$$ \Gamma \vdash \alpha \ \ \text{iff} \ \ \Gamma \vDash \alpha $$

Is $\Gamma$ supposed to be a set of hypotesis, a theory, or could be both (because a theory is just a set of formulas)?.

Are these definition of theories presented really different in some important way?.

  • $\begingroup$ @MauroALLEGRANZA Yes, i get that. Im more concerned with the details as in my question, e.g. are the two approaches mentioned the same?. $\endgroup$ – silver89 Jan 5 at 7:48
  • $\begingroup$ In modern model theory a "theory" is a set of sentences (satisfied by a model (a class of models). M's def is more "traditional"; see Euclid's Elements : what follows (by logical rules) from specific (mathematical) axioms. The two are the same ? See logical consequence and completeness ($\vdash$ vs $\vDash$). $\endgroup$ – Mauro ALLEGRANZA Jan 5 at 8:24

The current model-theoretic definition of theory is (see D.Marker, page 13) :

let $\text {Th}(\mathcal M)$ the set of $\mathcal L$-sentences $\varphi$ such that $\mathcal M \vDash \varphi$.

The link with Mendelson's concept is through Completeness :

let $\Gamma$ a set of sentences and $\varphi$ a sentence; then $\Gamma \vdash \varphi \text { iff } \Gamma \vDash \varphi$.

We will use $\text K$ to denote also the set of non-logical axioms of (Mendelson's) theory $\text K$.

We have that if $\varphi$ is a theorem of $\text K$ (i.e. $\text K \vdash \varphi$; in Mendelson's symbols: $\vdash_{\text K} \varphi$), then $\text K \vDash \varphi$.

This means that, if $\mathcal M$ is a model of $\text K$, then $\mathcal M \vDash \varphi$, i.e $\varphi \in \text {Th}(\mathcal M)$.


if $\mathcal M \vDash \text K$ and $\vdash_{\text K} \varphi$, then $\varphi \in \text {Th}(\mathcal M)$.

Now about your doubts...

Yes: (1) and (2) are equivalent.

A (Mendelson's) theory is a set of sentences; e.g. the (infinite) set of first-order Peano's axioms (see Ch.3, page 154).

Is $\Gamma$ (as used in Completeness Th) supposed to be a set of hypothesis, a theory, or could be both (because a theory is just a set of formulas)?

Exactly; the axioms of a formal mathematical theory is the set of hypothesis that we assume to hold for the "theory" we are studying.

| cite | improve this answer | |
  • $\begingroup$ Thanks!. I find some detail a little problematic. Consider M's Corolary (of Completeness) 2.20.a: "A wf $B$ is true in every denumerable model of $K$ iff $\vdash_K B$". Now, using $K$ for the set of axioms of theory $K$, this means $K \vDash B \iff K \vdash B$, wich is strong soundness&completeness. But in M's system this is not true because strong soundness is only valid for sentences (deduction theorem have a restricion). So, we conclude M's use of $\vdash_K ...$ doesnt really mean $K \vdash ...$ ? $\endgroup$ – silver89 Jan 5 at 22:34
  • $\begingroup$ (On the other hand, is true that M's system satisfy Strong Completeness, that is Corolary 2.20.c) $\endgroup$ – silver89 Jan 5 at 22:37
  • $\begingroup$ @silver89 - IMO, there is a "subtle" point here; see this post for some details. $\endgroup$ – Mauro ALLEGRANZA Jan 6 at 8:06
  • $\begingroup$ Well, it is perfectly clear M's semantic consecuence doesnt agree with sintactic consecuence (i.e. no strong soundness/completeness). Then i guess there are only two posibilities: either Mendelson's Completeness is wrong, or we cant read M's $\vdash_K$ as $K \vdash$ in the modern sense. But, the second option seems to contradict your answer. Do you agree?. $\endgroup$ – silver89 Jan 6 at 16:52
  • 1
    $\begingroup$ I think i have found the problem!. In M's Corolary (of Completeness) 2.20.a, the left part "A wf $B$ is true in every denumerable model of $K$" doesnt mean $K \vDash B$ (i.e. is not logical consecuence as defined in M's). So we cant write it in symbols in the usual way, as i did wrongly in previous comment. But now we can write Corolary 2.20.c (about logical consecuence) in symbols: $K \vDash B \Rightarrow K \vdash B$, and this is what we expected, Mendelson doesnt claim Strong Soundness, only Strong Completeness. What you think? $\endgroup$ – silver89 Jan 6 at 23:01

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.