-1
$\begingroup$

In this introduction on Satisfiability modulo theories, it is explained that by a "theory" $T$, it is meant a tuple $(\Sigma, I)$ where $\Sigma$ is a signature (i.e. a set of non-logical symbols), and $I$ is a set of models of signature $\Sigma$.

This is different from the definition of "theory" that I'm used to from mathematical logic, namely a set of $\Sigma$-formula's (i.e. axioms).

Essentially, the first definition is a semantic one and the second one is a syntactic one.

Question:

  • From what context does the first definition come? Does it come from model theory? (which I don't know much about).

  • What is the relation between the two?

$\endgroup$
  • 2
    $\begingroup$ Footnote 5 in the document you link to looks like the authors are aware their definition is not mainstream. $\endgroup$ – Henning Makholm Oct 29 '18 at 17:55
  • $\begingroup$ @HenningMakholm, I was aware of that footnote. I'd still like to know where this concept comes from and what the relation between the two is. $\endgroup$ – user600670 Oct 29 '18 at 17:58
3
$\begingroup$

I've never seen the usage you mention before. Certainly if "theory" is said in a room full of mathematical logicians, unless someone says otherwise out loud everyone will assume it means either "set of sentences" or "deductively closed set of sentences." Occasionally specific contexts impose additional constraints - e.g. in model theory we often mean "complete consistent set of theories," and in computability theory we often mean "countable theory" - but $(i)$ those are understood as minor abuses of terminology and $(ii)$ they're still in the usual context of "theories = sets of sentences."

It's worth noting however - and this answers your first question - that every theory in the usual context corresponds to a theory of the type you describe: given a set of sentences $T$, we can look at the pair $(\Sigma,I)$ where $\Sigma$ is the language of $T$ and $I$ is the set of models of $T$. (This is mentioned in footnote $5$, which also points out that the usage here is nonstandard.) This makes that definition the (or at least a) right notion for "semantic" abstract model theory, and However, none of this contradicts the fact that this is definitely a highly nonstandard usage, and in any context where this meaning is used this will be stated explicitly.

As to where it comes from, the notion (as opposed to its name) is a natural one anytime logics other than first-order are considered; I imagine it either emerged in abstract model theory or in computer science (in the study of satisfiability over finite structures, where trans-first-order logics are actually quite important and "safe to use").

$\endgroup$
  • $\begingroup$ Do you happen to know whether the word "theory" in "satisfiability modulo theories" also is generally meant to be "set of sentences"? $\endgroup$ – user600670 Oct 29 '18 at 18:11
  • $\begingroup$ @user600670 Yes. It's everywhere in mathematical logic generally meant to be "set of sentences," so far as I know; certainly in any of the circles I've travelled in (set theory, computability theory, model theory, and proof theory) to my experience. $\endgroup$ – Noah Schweber Oct 29 '18 at 18:12

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.