Talk:Theory (mathematical logic)

More concrete defs?

Shouldn't this article contain more concrete definitions, like what is a first order signature, a higher-order signature, a lambda-signature etc., and the same for theories Or should those go in separate articles? Pcap ping 19:51, 18 August 2009 (UTC)

Did you mean to ask this at Talk:Signature (logic)? I think these notions would fit well into signature (logic) if you can find them in the literature. I have never seen them or heard of them, although I can guess what a second-order signature or an MSO-signature would be. Hans Adler 20:09, 18 August 2009 (UTC)

Johnstone's Sketches of an elephant, chapters D1 and D4 defines all the stuff I wrote above. It defines not only the signatures I mentioned, but also the associated theories, so the question is relevant here as well, e.g. D1.1.1 defines first-order signature, D1.1.6 some flavors of first order theories. Pcap ping 22:01, 18 August 2009 (UTC)

Coming from the usual logic background the connection to signatures seems to be a bit artificial to me. I believe the usual POV is that a signature and a logic (in some suitable abstract sense) together define a logical language in some sense, and then a theory is just a set of sentences in that language. The signatures are often not even made explicit.

I am quite interested in learning the categorical (categorial?) view of these things, but I do think this is not the right place to discuss all notions of signatures. In a sense this is a key concept for both syntax and semantics, and this is an article just on syntax. Hans Adler 22:44, 18 August 2009 (UTC)

Johnstone does not introduce categories to define those notions (categories enter later as syntactic category -- well, not described in that article), but if you think that it's not an orthodox approach to define stuff that way, perhaps theory (categorical logic) should be started? It seems odd to me because no categories are involved... I see that Higher order logic is a very stubbish article, so perhaps it is the right place, because "higher order" (as well as "first order") is defined in terms of signatures. Pcap ping 23:10, 18 August 2009 (UTC)

Forget about the categories then. Apparently you want to discuss non-first-order theories, which is of course fine. I didn't add them because I don't know enough about them, but I always felt that they should be discussed. But the key for discussing these more general theories seems to be the other logics. It seems that we would lose relatively little information by discussing theories in higher-order logics but only over first-order signatures. The big step happens where we allow higher-order sentences, regardless of the signature. So it seems rather odd to stress them here, when their absence is a significant gap at signature (logic). Perhaps you can add them there. Otherwise I will use your pointer to the elephant book to do it when I get the time. Hans Adler 23:49, 18 August 2009 (UTC)

(ec with reply below) Okay that makes sense. We (as in whoever finds time to do it) add the notions of higher order singnatures to signature (logic). In order to actually get a deduction system, Johnstone uses sequent calculus (although that article seems to consider a simpler variant) because it is sufficiently general for both first- and higher-order languages (but, of course, it's overkill for 1st order logic). Just by classifying first order sequents, some interesting (even though rather trivial observations) can be made: e.g. that the axioms of partially ordered sets form a Horn theory, and so do torsion free abelian groups, whereas the theory of divisible abelian groups is regular; the theory of categories is later shown to be cartesian. I found this classification of first order theories interesting (the 5-page example D1.1.7), and though that this article might be right place for it, even though List of first-order theories or sequent calculus might be better. Suggestions? Pcap ping 00:27, 19 August 2009 (UTC)

It sounds all very interesting and I am looking forward to reading about this approach. But you should be aware that some things may not be mainstream material about theories (outside Cambridge, that is). E.g. I have never heard of regular or cartesian theories, and I had to look it up in the elephant book to understand how Johnstone treats a theory as a category. As usual for him, this seems to be very simple, efficient, elegant, but at the same time somewhat hard to grasp when you are not coming from a category theory background. I think we need a clear separation of this material from the more mainstream approach, so that a reader who just wants to learn what a first-order theory is in the classical sense doesn't get confused. Hans Adler 09:21, 19 August 2009 (UTC)

Higher-order logic is very short but second-order logic is quite complete.

If we want to say anything about higher-order theories, this article is the place. But we need to be careful because for example the "first-order signature" of second-order arithmetic is exactly the same as the "second-order signature" of second-order arithmetic. Similarly the syntax of type theory with first-order (Henkin) semantics is identical to the syntax of type theory with full semantics. Thus there is no way for you to tell whether the following is a "first-order sentence" or a "second-order sentence":

$\forall X\exists n(n\in X).$

I see that Johnstone puts "(first-order)" in parentheses on p. 808. Also, it makes sense to say "first-order signature" if one is trying to distinguish first-order logic from propositional logic. — Carl (CBM · talk) 23:59, 18 August 2009 (UTC)

He defines the signature of a higher order logic in a more restrictive way on p.940 (D4.1.1.), where type constructors can be only from a list he gives: basic, product, function, power and list types. Pcap ping 00:33, 19 August 2009 (UTC)

His definition on p. 940 implies that the type constructors are optional. In particular, every first-order signature (his def 1.1.1) is also a higher-order signature, if the collection of type constructors is declared to be empty.

My main point here is that it is impossible to determine solely on the basis of syntax whether whether $\forall X\exists n(n\in X)$ is a "first-order sentence" or a "second-order sentence". Thus some care is needed when writing about these things. — Carl (CBM · talk) 00:43, 19 August 2009 (UTC)

Hmm, but in Johnstone's D4.1.1, $\in$, or any relation, is typed. Of course the type of $\in$ can be T × T, but that won't ever have sets as model, whereas T × PT, where P is the power type constructor, could. This avoids Russel's paradox. No?

On some further thought, I'm a bit reluctant to take D4.1.1 (or Lambek's slightly more general def, in which types are not necessarily freely generated) as the definition of a higher order signature. Their (Johnstone or Lambek's) definition seem tailored so that categories immediately apply by finding a suitable category for the signature (done in D4.1.4). Is there some other reasonable way to define a higher-order signature? Pcap ping 01:36, 19 August 2009 (UTC)

You are right that the relations in D4.1.1 are typed, but so are the relations in D1.1.1 ... Thus Johnstone considers typed first-order logic and typed higher-order logic.

There are plenty of authors who discuss higher-order logic on the mathematical logic side, so I can look to see if they try to define "higher-order signature". But I doubt that many do, if any. A google books search for "higher-order signature" (in quotes) suggests this is mainly a CS term, and that it refers not to higher-order logic specifically, but to the presence of higher types in the formulas. — Carl (CBM · talk) 01:46, 19 August 2009 (UTC)

(ec) I see what you mean now: the signature alone is indeed not sufficient, but $\forall X\exists n(n\in X)$ is not a (well formed) formula in a higher order logic according to D4.1.3 (atomic formulae); the $\in$ needs to be typed, and written as $n\in _{T}X$ iff n has type T and X has type PT. Of course the type subscript is dropped "whenever its safe to do so", presumably meaning that the types are understood from context. Pcap ping 01:53, 19 August 2009 (UTC)

So we do find out that the rank of n is one less than the rank of X from the formula; rank here is in the sense of type polymorphism article. Pcap ping 02:00, 19 August 2009 (UTC)

Even if one adds a type subscript to the formula, this still doesn't determine whether first-order or higher-order semantics are being used; the syntax is identical in each case. Back to a previous example: the second-order version of Peano arithmetic uses exactly the same signature as the first-order theory named second-order arithmetic. So care is needed to define "second order theory". — Carl (CBM · talk) 02:47, 19 August 2009 (UTC)

I probably don't understand this fully, but what you seem to be saying is: what you can quantify over has to be imposed by a metalanguage because it's not determined syntactically; further whether one gets a first-order theory or not depends on the intended interpretation of the Sigma-sort in D1.1.1. On the other hand, the power type in D4.1.1 (for instance) allows one to have syntactic representation of quantifying over sets as long as the same interpretative restriction over Sigma-sort is imposed in the metalanguage. Pcap ping 04:22, 19 August 2009 (UTC)

Fω?

It's interesting that one seems to get System Fω in D4.1.1 by restricting type constructors to arrow type (iii). Johnstone does not consider it in the book though. Pcap ping 04:22, 19 August 2009 (UTC)

But not dependent types?

Given that type constructors in Johnstone's D4.1.1 cannot take non-types as arguments, it looks like it can only generate a plane of the lambda cube, i.e. it excludes LF (logical framework) and calculus of constructions. You could just encode each term as a type as well, but that seems insane. So, in this sense it's not really a satisfactory definition for a higher order logic... Pcap ping 05:32, 19 August 2009 (UTC)

I found the categorical semantics of CoC in Jacob's book though, see my comment below that of Charles Matthews in the next section. Pcap ping 09:52, 19 August 2009 (UTC)

Comments (?)

I was asked to comment here from the point of view of categorical logic; which puzzles me somewhat (15 years since I had much to do with that area, though I certainly know some of the Cambridge people). The approach is that category theory is what it is; you find "logic" once you start to ask about ways to give presentations of categories (not really a well-defined notion of "presentation", more a working concept). The logic of the presentations will be higher-order in all but relatively trivial cases, because one works with cartesian closed categories. The whole approach is opposite to the sort of post-Tarski logic one is led to expect from model theory, which rations expressive power in order to make the semantic side work as well as possible. Therefore, if you start from a notion of "theory" which comes from the Tarski end, you are likely to see the business from a slightly unnatural angle. Perhaps that's all that the discussion here illustrates. Historically "mathematical logic" was the subject founded in the 1930s as a successor to "meta-mathematics" in Hilbert's conception, to make sense of what Gödel had done. Categorical logic was founded in the 1960s, by Lawvere really, to make sense to logicians of what Grothendieck in particular had done. The computer science connection comes later, and is (according to one of the experts) perhaps mainly a question of category theory having an organising role.

Anyway, there are surely notions in categorical logic corresponding to known notions of traditional mathematical logic. And there are prominent applications in theoretical computer science. What I can't say is whether there is an over-arching explanation of what is going on there. If you start from topos theory, as Johnstone certainly does, you will come in at a particular angle; if you start from proof theory, as Girard for example does, you come in at another angle. Charles Matthews (talk) 06:41, 19 August 2009 (UTC)

Well, of course Tarski is the dominant paradigm and should be the jumping-off point. The other things would be interesting to treat as well; I don't know nearly as much about them and would like to. But they shouldn't be allowed to make the article confusing. --Trovatore (talk) 09:02, 19 August 2009 (UTC)

(ec) Well, Johnstone in part D of his book starts with the classic notions of a (typed) signature, theory, etc., at least in D1 where he deals with first-order languages (first-order logic fragments I guess). He then constructs a syntactic category for a signature and proceeds to give categorical semantics. Then he moves to higher-order logic in chapter D4, and covers some classic results in this area, e.g. the correspondence between simply typed lambda calculus and Cartesian closed categories, which entails defining a lambda-theory (pretty much the higher-order equivalent of an algebraic theory) etc. There are some limitations to his approach. One is artificial, in that he excludes quantifiers from lambda-signatures, so he doesn't quite get System Fω, although that is still definable as a higher order logic under his definition of that notion (D4.1.1 in the discussion above). But Johnstone's definition of a higher-order logic seems narrowed just enough so categories fit perfectly (see question above about dependent types); it does not seem to encompass the calculus of constructions, so it's somewhat unsatisfying to me in that regard.

Thankfully, the categorical semantics for CoC ar covered in Bart Jacob's book Categorical Logic and Type Theory, chapter 11, where it's called "fully higher order dependent type theory". But you need the notions of strong sums and very strong sums to capture the dependencies. Pcap ping 09:20, 19 August 2009 (UTC)

Also, this paper is very interesting in that it defines higher order logic as particular kind of a pure type system. Pcap ping 09:39, 19 August 2009 (UTC)

Found free preprint too. Pcap ping 09:43, 19 August 2009 (UTC)

To follow up on this, there's actually some confusion as to what higher-order logic reefers to. It's both a class of logics, but also, commonly used to refer to a particular member of this class, usually abbreviated HOL. I've added this disambiguation to the higher-order logic article. Pcap ping 15:18, 20 August 2009 (UTC)

Upon reading Johnstone's review of Jacobs book found pointer here, it's clear that Johnstone does not bother with logic over dependent types or polymorphic types because he considers them important only to computer science. Pcap ping 05:48, 20 August 2009 (UTC)

Yes, PTJ has a particular POV as category-theorist. By the way (and this discussion seems ever-broadening, but there are reasons) Johnstone started off working on classifying toposes, and I have found it illuminating that there is a "syntactic" way of presenting those, as written down by Mac Lane and Moerdijk. What you classify is a "theory" much in the sense of this article, but for what is called geometric logic. Getting back to improving the article, an explanation of where that leads could be helpful. Charles Matthews (talk) 08:56, 20 August 2009 (UTC)

Yeah, uhh, all theory aside, it would be nice to have a good clear definition because this stuff actually has practical applications. In particular, the 'theory' of satisfiability modulo theories is the same 'theory' of this article. People write algos for SMT, and SMT gets deployed in quotidian software systems e.g. get used during the design of the cell phone you're carrying. So having a nice, clear definition, readable by the mildly educated software programmer, would be nice ... BTW, there are several PhD's in compiler theory down the hall from me, and *none* of them have heard of category theory.linas (talk) 18:33, 14 June 2011 (UTC)

Guhh, I thought I had some idea of what a theory was until just now, when I actually tried to read this article. Its utterly opaque. Fails to mention the easier case of an equational theory viz something without quantifiers. It really doesn't help that equational theory is just a redirect to universal algebra which is OK, but not very edifying. FWIW, for comp sci, the equational theories are probably mostly enough; its where most of the common problems lie. linas (talk) 18:48, 14 June 2011 (UTC)

General form

Writing "The general form of a theory is $T=\{t_{1},t_{2},\ldots \}$" is just as vacuous as writing "The general form of a formula is φ.". Moreover, a general theory is not countable (e.g. the complete diagram of the field of real numbers). — Carl (CBM · talk) 20:28, 16 June 2010 (UTC)

You are brilliant, but you just don't get it. Why don't you go ahead and try yourself to include some formal language representation that will help someone understand what a theory is. Some people think visually. Everybody knows that you know. Why don't you try writing for someone else besides yourself and your buddies for once? In your mind {t1, t2, t3} is the same thing as φ okay, that's just fine for you. Screw everybody else then?Greg Bard 22:12, 16 June 2010 (UTC)

Would you mind explaining how "Theories generally take the form: ${\mathcal {T}}$: {t₁, t₂, ... , t_n, ...}" will help anyone understand what a theory is, and what this has to do with visual thinking? Algebraist 22:17, 16 June 2010 (UTC)

"The general form of a theory is $T=\{t_{1},t_{2},\ldots \}$" seems to say just that a theory is a set. Since it does not suggest any limit to what t_1, t_2 stand for, it suggest a Theory (or the form of a Theory) ANY set would be in the form of a theory. That does not explain whether a pack of cards is a theory. It's like saying the form a cathedral is a three-dimensional object. Well as they say, every little helps, but not much. And how does the sybolism help: why not say just "A theory is a set"? — Philogos (talk) 23:34, 14 June 2011 (UTC)

Listen, this is just flabbergasting. You want me to explain to you, someone who presumably knows what a theory is, how someone who doesn't understand thinks. Formal language exists for the purpose of giving a visual representation that helps understanding. You are asking me supremely obvious questions, and I have to ask that you back off and consider that there are pedagogical concerns which you should respect. Why don't you explain to me why anyone uses examples at all. Greg Bard 22:27, 16 June 2010 (UTC)

I want you to explain why that incorrect "example" of a theory is helpful. — Arthur Rubin (talk) 00:40, 17 June 2010 (UTC)

Yeah, I don't know what prompted the argument above, but the third or fourth sentence now says ... and normal set-theoretic language may not be appropriate. which begs the question why not? Perhaps we could start at a simpler level, with some statement that a theory might be a finite set of sentences, (in which case {t1, t2, t3} is a reasonable way of listing some of the sentences in the theory), and then move on to the case where 'normal set-theoretic language is not appropriate'. I can't help but notice that the current article doesn't even talk about how to combine two theories into one; it seems to me that, to build up a large theory from smaller ones, one would need a way of combining (perhaps I'm being too constructivist here, but still...) linas (talk) 18:24, 14 June 2011 (UTC)

The puzzling comment about set-theoretic language not being appropriate makes perfect sense once you consider all the relevant parts of the sentence: "When defining theories for foundational purposes, [...] set-theoretic language may not be appropriate." Here, "for foundational purposes" usually means that we want to use first-order logic as the foundation of set theory. If we then base the description of first-order logic on set theory, we are in a loop. That's all. The usual 'solution' is to avoid set theoretic while still doing everything we would have done otherwise, except perhaps things such as application of the axiom of choice, or cardinality arguments.

Since theories are just sets of sentences, with no further assumptions, the obvious way of combining two of them is by taking their set-theoretic union: $T_{1}\cup T_{2}$. (Of course, if each of the two theories was closed in some sense (e.g. under conjunctions or implication), then you will likely want to take the corresponding closure of $T_{1}\cup T_{2}$ as well.) Hans Adler 18:36, 14 June 2011 (UTC)

The article currently begins: ...conceptual class E, the elements of which are called statements. These initial statements are often called the primitive elements or elementary statements of the theory... What the heck is a conceptual class? Is this like a class of category theory? Something else? what is a statement? is it a statement (logic)? or maybe a sentence (mathematical logic)? Something else? Are statements allowed to have quantifiers? How about free variables? Is the aversion to set theory due to the fact that you are trying to deal with an uncountable number of statements? Can I use set theory if I have only a finite but unbounded Kleene star number of them? Tools such as satisfiability modulo theories solvers automatically find interpretation (logic) or model theory models for theories, but to make sense of such tools, one needs a clear definition of what a theory is. linas (talk) 19:33, 14 June 2011 (UTC)

"Conceptual class" is the jargon used by a random philosopher who once wrote about these things. Such out-of-context use of philosophical terms that makes articles impenetrable is a sure sign that Gregbard was here. (And at first he even wrote "conceptual set" instead of "conceptual class", completely ignoring the main point of this terminology, which must have been to avoid set theory.) The discussion above may give you a vague idea of why this can't be fixed easily, but you would have to argue with him yourself to really understand the extent of the problem. Hans Adler 21:48, 14 June 2011 (UTC)

Whether we have quantifiers etc. depends on the logic we are using. Unfortunately there are no standard terms and conventions for logics yet. (Some people wrote an article a while ago, "What is a logic?", in which they tried to settle on one.) In the (almost) most general context, this "conceptual class" is just a set. But usually it's something like the set of equations or first order sentences or quantifier-free first-order sentences over a signature. Hans Adler 22:03, 14 June 2011 (UTC)

This paper: SMT appetizer defines a theory, but does so in a way that I find to be sloppy and incomplete; this article should be able to do better. This paper: SMT give a one-paragraph review of model theory, and then defines a theory as a collection of one or more models, with this footnote: The more traditional way of defining a theory as a set of axioms can be simulated as a special case by taking all Sigma-models of the theory axioms. I think this is an interesting view .. I'd have to ponder it. Somewhere at home I have a copy of Wilifrid Hodges Model Theory, and am now itching to see what he said...linas (talk) 20:14, 14 June 2011 (UTC)

According to Mendelson Introduction to Mathematical Logic (1964) p. 29 A formal theory T ..is defined when.. the symbols are given and the rules for wfs are provided and a sets of wfs is set aside and called the axioms of T..and ..There is a a finite set..or relations amongs wfs, called the rules of inference. In other words a Theory in a given formal language is defined when axioms and rules of inference are provided. This defiintion seems to closely match the defintion of a formal system given in formal system. Has the definution of Theory changed, or is this a different sense of the term Theory, or is Mendelson saying the same thing as this article in different words? — Philogos (talk) 20:19, 14 June 2011 (UTC)

Yes, I think it may have. The Mendelson definition dates back to the 1960's, and predates much of comp-sci. For things like formal languages, or at least for equational theory, I think one would say it's an insufficient/incomplete/vague definition. The problem is that, in order to actually implement algorithms, you have to talk about truth of formulas, and for that you need interpretation (logic) and model theory. Some authors call this the "semantics" of a theory. Now, I myself read almost exclusively about equational theories, and perhaps these concepts don't work in full generality; I don't know. Anyway, the second pdf above [1] defines a theory on page 4 (i.e. you don't have to read much to get to it) as a collection of models, plus that enigmatic footnote about axioms. So, from this, I conclude that there is a notion of theory in an older (1930's-1960's) 'conventional' sense, and also more modern definitions of a 'theory', tailored to the needs of comp-sci, and finally, yet other definitions, presumably tailored for topos, etc. linas (talk) 20:44, 14 June 2011 (UTC)

Yes, it's obsolete terminology. Hans Adler 21:48, 14 June 2011 (UTC)

..and what he called a theory is now called (a) Deductive system or (b) a formal system or (c) a Theory (mathematical logic) whose content is based on some formal deductive system and that some of its elementary statements are taken as axioms (ex this article).?— Philogos (talk) 22:07, 14 June 2011 (UTC)

I am not sure. Mendelson isn't clear to me. He almost sounds as if he is intentionally avoiding to give a precise definition. It's how we still deal with the notion of a "logic". It's not clear what that includes, either. Hans Adler 22:23, 14 June 2011 (UTC)

True that! His account is along the line of the childish "it's what you get when".. Leaving Medelson aside, (a) I have been toggling between Deductive system and formal system and cannot get the hang of the difference (if any) (b) this article Theory (mathematical logic) says initially that a theory is a set of sentences. It later says that these sentences may be (called) theorems. Looking at theorem however, it says that a theorem is either assumed to be true (what I would have called an axiom - be it logical or proper) or derivable. (In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms.) Corrrect me if I am wrong but I understood that for a sentence to be derivable at least one rule of inference is required. If so unless a rule of inference can be construed as (i) a sentence and (ii) part of the theory (i.e. one of the set of sentences that consitutes the theory) (iii) hence not expressed in a metalanguage then I do not quite see how a sentence in a theory defined as just a set of sentences can be a theorem (c) The article to which Linas directed me appears to suggest (it does not give an explict definition) that an impliict part of a theory is an interpretion. If an implict part of a thoery is an interpretation, then it is more than a set of sentences - it is a set of sentences PLUS an interpretation which, correct be if I am wrong, must be provided in a metalanguage. If these questions demonstrate that my lack of knowledge/intelligence excludes me from the intended audience for thas article, just say so and I will withdraw! — Philogos (talk) 23:02, 14 June 2011 (UTC)

I think you misread the theorem article; maybe the sentence should be clarified. This is what it means: "a theorem is a statement that has been proved on the basis of previously proved theorems and of axioms".

Also, the theorem article isn't very helpful here because "theorem" is really a misnomer in this context. Since a theory is an arbitrary set of sentences, it's better to think of them as "axioms". The mathematical POV here is that we are building a mathematical model (in the non-technical sense) of theories, axioms and theories in the plain sense of the words and are using suggestive though ultimately arbitrary words for the mathematical objects representing them. On this mathematical level there is no real difference between axioms and theorems, and by some unfortunate accident the word "theorem" was chosen. And the meaning of "theory" evolved from its original sense, that was closer to the plain meaning, to a simpler one. So the problem is entirely on the side of established mathematics terminology, and has nothing to do with your intelligence, which seems to be excellent. Hans Adler 23:50, 14 June 2011 (UTC)

(A) This article begins

• In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. The individual sentences of a theory are called its theorems.

The Theorem article begins

• In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms.

Do these fit together OK (i.e. is the use of the term theorem in the former corretly defined in the latter? I do not think that the term statement should be used in the latter. A "statement" in common parlamce is not the same thing as a [2] defines a theory on page 4 the former (in common parlance) is either true or false wheras the latter is neither accept under an interpreation. Moreover the the article statement describes a technical use of the term statement as described by Strawson. Again it is quite different to a sentence. B. The article to which Linas directed me appears to suggest (it does not give an explict definition) that an implicit part of a theory is an interpretion. (the ref is [3] defines a theory on page 4 ). If a theory is just a set of sentences in a formal language then I do not see how it can include an intepretation (which is surely in a metalanguage). Is the term theory not being used in a different sense in [4] to the sense defined in this article?— Philogos (talk) 01:38, 15 June 2011 (UTC)

No, they don't fit together. The misleading statement was added to the lead by this edit. While writing this answer, I became aware that one only speaks of theories when a deductive system is understood from context. Otherwise one would refer to the same thing as a "language". (Instead of a deductive system it can be some notion of model or interpretation of a sentence. But any such notion gives rise to a deductive system, although it may not be possible to describe it in the way mentioned in the last paragraph of the article deductive system. The rule of inference is: $A\vdash \phi$ if an only if every model of all sentences in A is also a model of φ.) Here is a better version of the lead:

In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. Usually a deductive system is understood from context. An element $\phi \in T$ of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms ($T\vdash \phi$) is called a theorem of the theory. Every axiom is also a theorem. A first-order theory is a set of first-order sentences.

Gregbard became confused because he was using Curry's book and misunderstood some things. Curry refers to the axioms as "elementary theorems" (which is an unfortunate choice of words because "elementary" can also mean "first-order"). This seems to be intentionally ambivalent terminology, tending both towards "axiom" and towards "theorem". Under modern standard conventions one would refer to an "elementary theorem" as an axiom. But Curry defines a "deductive theory" as a theory that consists of all the theorems that follow from a given decidable set of axioms using a given deductive system. What is really going on here is this: Given any theory T as defined earlier (i.e. a set of "axioms"), we can take the set T' of all theorems of T. Since this is again a set of sentences, it's also a theory, which we could call the "deductive closure" of T. T' has exactly the same theorems as T, but in T' they are all axioms. A "deductive theory" is the deductive closure of a decidable theory. If we really want to mention deductive theories in the lead (I am not sure the notion is sufficiently well known), then we could do it as follows:

A theory is decidable if there is an algorithm for deciding whether any given sentence is an axiom of the theory. A deductive theory is the set of all theorems of a decidable theory.

Hans Adler 06:48, 15 June 2011 (UTC)

Now THAT is clear, even to a non-mathematican. Therefore I sahll be bold and change the lede to the version you propsose above.— Philogos (talk) 13:57, 15 June 2011 (UTC)

On a second reading the follwing in the lede seems to suggest that only the axioms are elements of a theory. A little tweek required?

• An element $\phi \in T$ of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms ($T\vdash \phi$) is called a theorem of the theory. Every axiom is also a theorem.

perhaps

• Each element $\phi \in T$ of a theory T is either an axiom or a sentence that follows from the axioms ($T\vdash \phi$) called a theorem. Every axiom is also a theorem.

I would be happiest if there was a "history" section near the top, which points out the shifting needs and definitions -- viz theorems for ancient greeks, working-mathematicians informal idea of a proof, whitehead->Hilbert program to formalize logic, crisis of 1930's church/godel incompleteness, foundations of 1960's; modern times (1980's-onward) for automated theorem prover algorithms. These are all distinct, and put different demands on what a 'theorem' is. I think its OK to discuss how the notions change ... linas (talk) 19:19, 15 June 2011 (UTC)

Hans can you now reolve the other issue raised above re interprertaions, i.e.

• The article to which Linas directed me appears to suggest (it does not give an explict definition) that an implicit part of a theory is an interpretion. (the ref is [3] defines a theory on page 4 ). If a theory is just a set of sentences in a formal language then I do not see how it can include an intepretation (which is surely in a metalanguage). Is the term theory not being used in a different sense in [4] to the sense defined in this article?— Philogos (talk) 13:57, 15 June 2011 (UTC)

Thanks for the reminder. I didn't have the time for a full response initially, and would have forgotten about it. The definition of a theory in [5] (= [3] = [4]) is as follows:

In SMT [= satifiability modulo theories], one is not interested in arbitrary models but in models belonging to a given theory T constraining the interpretation of the symbols of [the signature] Σ. Following the more recent SMT literature, we define Σ-theories most generally as just one or more (possibly infinitely many) Σ-models. [Footnote:] The more traditional way of defining a theory as a set of axioms can be simulated as a special case by taking all Sigma-models of the theory axioms.

This is a relatively recent definition of a theory that is not mainstream but probably has sufficient currency that we should discuss it briefly in the article. (I believe I have seen something like this before in an abstract model theory context.) Some comments in bullet form:

• It's from a book about "satisfiability modulo theories", apparently a relatively pure (mathematical) topic in pure computer science. Normally when you have a theory you are interested in whether something follows from it (is a theorem). These people are interested in whether it's consistent with the theory. That's a substantially different question. Given a sentence φ and a theory T, it may be the case that both φ and its negation are satisfiable modulo T (though of course not simultaneously).
• The footnote and the guarded language "following the more recent SMT literature" acknowledge that the definition given is not the standard one, and that a theory is normally a set of sentences (axioms).
• You cannot ask satisfiability questions without some notion of models (= interpretations). Therefore working with these does not reduce generality in the context of the book chapter. As this is computer science, not philosophy, there will be a precise technical definition of what a Σ-structure (= Σ-model) is, and when a Σ-structure satisfies a sentence. Saying that a theory is a set of Σ-structures is of course not the same as saying it's a set of sentences, but it's not less precise.
• There is a well known Galois connection between theories (= sets of sentences) and sets of models. (You don't need to know what a Galois connection is. It's actually rather simple, and here we have a typical example.) Given a Σ-theory T₀ (i.e. set of Σ-sentences), we can consider the set M(T₀) of all Σ-structures that satisfy the theory. Conversely, given a set M₀ of Σ-structures, we can consider the set T(M₀) of all Σ-sentences that hold in all structures in M₀. If we make T₀ bigger, M(T₀) will get smaller (anti-monotonicity of the function M). If we make M₀ bigger, T(M₀) will get smaller (anti-monotonicity of the function T). Moreover, we can express "every structure in M₀ satisfies every sentence in T₀" in two different ways:
  • M₀ ⊆ M(T₀) -- every structure in M₀ is among those which satisfy all sentences in T₀
  • T₀ ⊆ T(M₀) -- every sentence in T₀ is among those which hold in all structures in M₀.

These two conditions are therefore equivalent. From the antimonoticity of T and M and the equivalence of these two conditions it follows that for any T₀, T₁ = T(M(T₀)) ⊇ T₀, and that T(M(T₁)) = T₁. In the same way it follows that for any M₀, M₁ = M(T(M₀)) ⊇ M₀, and that M(T(M₁)) = M₁. The nice properties of T(M(.)) and M(T(.)) can be summarised by saying they are closure operators. A set such as T₁ or M₁ above, which does not change under the respective closure operator, is called a closed set. The functions T and M define bijections between the [set of] theories that are closed in this sense and the [set of] sets of structures which (i.e. the sets) are closed in this sense. In other words, a closed theory is basically the same thing as a closed set of structures. This is interesting because (assuming that the completeness theorem holds for our deductive system) a closed theory is precisely the same thing as a theory that contains all theorems as axioms.

For "satisfiability modulo theories" questions, adding the theorems of a theory to it as axioms does not make any difference. Therefore, from that point of view it is harmless to only consider closed theories, and once you are doing that, a theory is basically the same thing as a closed set of structures, via the Galois connection.

• If the previous point was too technical or too detailed, here is a summary: Under a reasonable assumption on the deductive system, a theory that is closed in the sense that every theorem is an axiom is essentially the same thing as a set of structures that is closed in the sense that any structure that satisfies all sentences that are satisfied by all structures in the set is itself in the set. (A structure that satisfies all sentences that hold in all structures in the set is the analogue of a theorem. We just don't have a word for it.)

I guess I will add something like this to the article later, once I have located the abstract model theory stuff that I seem to remember seeing. Hans Adler 17:06, 15 June 2011 (UTC)

combining theories?

I'd like to see a discussion of how to combine theories, in particular, referencing the Nelson-Oppen combination theorem. The mechanics for this seems to require definitions of strongly disjoint theories and a stably infinite theory and a pure formula. Also need definition for a convex theory. Also model-based theory combination. linas (talk) 18:15, 14 June 2011 (UTC)

These appear to be extremely technical notions from computer science that are very far outside the scope of this article. Is there any particular reason why you are interested in them? Are you sure you are at the right article? Hans Adler 19:05, 14 June 2011 (UTC)

Err, well, extremely technical is in the eye of the beholder -- they are clearly far less technical than the arguments immediately above on this talk page. And far outside the scope is utterly .. um .. debatable. I'm currently employed to work as a software engineer, and am currently looking into superoptimization for the LLVM compiler. I'm looking at using a satisfiability modulo theories solver for this purpose. Now, the theories of SMT are supposed to be the same theories as thos of this article, so I thought I'd brush up on this. I thought I vaugely knew what a theory was, but discovered that this article is so utterly opaque and dense and impenetrable, that I have absolutely no clue what to do about it all. I't's kind of frustrating. However, as to actually having a need to combine theories ... I think I do have such a need. Maybe.

Anyway, the theories I'm most likely do deal with will have a countable number of sentences (once I've grounded all variables, e.g. for array length) and they will typically all be equational theory. So having an article that reviews basic notions in a concrete understandable fashion would be really, really nice. linas (talk) 19:21, 14 June 2011 (UTC)

Thanks, that helps. Part of the problem with this article and many other fundamental logic articles is that it tries to satisfy both mathematicians and philosophers. The strange discussion above, which was basically about extreme hand-holding for philosophically oriented readers who have no idea what a set is, has probably given you a glimpse of that.

If I am reading the sources on Google Books correctly (I only skimmed a few and didn't pay too much attention, so just correct me where I am wrong), then the Nelson-Oppen combination theorem is about two equational theories in disjoint (except for sorts) signatures. If both theories are decidable, then under some technical condition the restriction of $T_{1}\cup T_{2}$ to the set of "pure" formulas is also decidable. (For no apparent reason some people write $T_{1}\oplus T_{2}$ for the same thing.) "Decidable" means that there is an algorithm that can decide for every sentence whether it follows from a theory.

The theorem is outside the scope of this article because it's specifically about universal algebra (the main examples in articles on fundamentals are propositional logic and first-order logic), because it involves signatures (confusing to philosophers, who are mostly not used to them), and because of the technical condition and the restriction to "pure" formulas, both of which make this very much an applied topic.

Unfortunately Wikipedia is no help at all for understanding the basic notions and their relations. Referring to a first-order theory as ${\mathcal {QS}}$ rather than T is symptomatic of this: Often non-standard notations and conventions creep in from the works of random philosophers and are then defended valiantly against change. Things are not completely standardised even among mathematicians. I used to work on this, but there were too many stupid fights, and I ran out of steam.

I recommend Herbert B. Enderton's book "A Mathematical Introduction to Logic" as an unusually readable account of the basics and excellent explanations of the terminology. Hans Adler 20:13, 14 June 2011 (UTC)

Well, look, at least some of these problems are solvable; an article such as this can certainly have multiple sections, one section discussing philosophical/historical definitions, another providing a narrow definitions suitable for formal language theory (i.e. the comp-sci part of things), and a third section dealing with Grothendiek and the topos-theory side of things. This article currently does not even list 'equational theory' in the 'see also' section; I feel that a chunk of this article should at least discuss this as a special case. A more comp-sci-centric intro to semantics, universal algebra, models & varieties. would be the book 'term rewriting and all that', which has a reasonably clean review of this in chapter 2, at what I think is suppose to be an undergrad level(?) linas (talk) 20:35, 14 June 2011 (UTC)

That would be in an ideal world in which this article is not owned by a math-phobic pseudo-philosopher, and where a lot of experts are willing to put work into it. But as you have noticed we can't even give a correct and readable definition here, so it's not an inviting environment for more advanced stuff further down. Hans Adler 21:58, 14 June 2011 (UTC)

Can you say who is the math-phobic pseudo-philosopher who owns this article?— Philogos (talk) 01:44, 15 June 2011 (UTC)

I hope you didn't for a moment think it might refer to you. I wouldn't have said it if I had thought there was any chance of such a misunderstanding, but given that not everybody is aware of the context of the earlier discussions on this page (most of which is at other articles), it seems necessary to point out that I was not referring to you at all and that I am very happy to have your extremely helpful comments and questions here. I turned this page from a redirect into an article, but realised that my efforts were futile when these edits struck. (This stuff is badly rephrased from Curry's book Foundations of mathematical logic. Curry's terminology is already non-standard; of course the mistakes make it even worse.) Hans Adler 07:06, 15 June 2011 (UTC)

Say no more. Can you suggest an on-line maths dictionary/encycopaedia where I can look up basic terms in mathematical logic and associated?— Philogos (talk) 13:44, 15 June 2011 (UTC)

Unfortunately there isn't anything good, detailed and extensive. This article by Wilfrid Hodges is pretty good, but of course he doesn't discuss everything. I guess this script by Harold Simmons is also pretty good, and it should have some additional details. The notation and terminology seems to be marginally less standard, though. (With one leg in model theory, one in philosophy, and apparently also an eye for what's going on in computer science, Hodges seems to be setting terminological standards.) Hans Adler 19:51, 15 June 2011 (UTC)

OK, well, my take on it is that it's OK to have several sections dealing with the different ideas of what a theory is; probably best is a historical approach, then a foundational/philosophical overview, then a "narrower"(?) but more precise "mathematical" definition filling the needs of modern automated-theorem-proving algorithms and/or satisfiability solvers. Maybe in a week, I'll give this a whirl. Meanwhile, am reading "a shorter model theory" from page one, and hope to use that as a basis for a formal defn (I think he defines a theory on page 20 or 30 or thereabouts, right?) linas (talk) 19:32, 15 June 2011 (UTC)

Rather than historical divisions, if the term theory is used (slightly) differently in differnt disciplines why not in the lede say, eg In mathematical logic a theory is.., in model theory a theory is.., in computer science a theory is.. I do not belive there is any technical (specialist) use of th term 'theory'. The Cambridge Dictionary of Philosophy eg only the reader to scientific theory.

At [6] we find

• A theory is a set of sentences which is closed under logcal implication. That is given any set of sentence {s1,s2...} in the theory, if r is a logical consequence of {s1,s2...} then r must be in the theory.

At [7] we find

• Theory, formal: The same as a formal system. See also Axiomatic method. : This text originally appeared in Encyclopaedia of Mathematics - ISBN 1402006098

Ths article should make clear the difference between a Theory (mathematical logic) and a Formal system— Philogos (talk) 23:28, 15 June 2011 (UTC)

Your first source links to this, which gives as a reference Enderton's book on set theory. I will check this later, but I would be surprised if he really required theories to be closed under implication. And it's the wrong book for this kind of information anyway. They should have used his book on logic, of course. The second source is something between our redirects and disambiguation pages. It refers to this, where the most recent reference is a topology/algebra/logic paper from 1976 which can almost certainly not be used as a source for standard terminology (MacLane being influential in topology, algebra and category theory, but not in logic), and books by Hilbert, Kleene and Church which obviously use outdated terminology.

There is a modern standard definition, which we are currently giving in the article, and there are some historical variants and the modern one as a set/class of models, which we can of course also present. But it must still be clear what the main meaning is. Hans Adler 06:39, 16 June 2011 (UTC)

Enderton's set theory book doesn't appear to define "theory". The first edition of his logic book appeared around the same time (1976) and does indeed say: "We define a theory to be a set of sentences closed under logical implication." The second edition is borrowed from our library. I will report what it says once I get home. Hans Adler 06:56, 16 June 2011 (UTC)

The second edition of the logic book has the same definition, on page 155. As an aside, this is not the sense that people mean when they talk about the satisfiability problem for a theory. Otherwise the problem would be trivial, you would just ask whether $0 = 1$ or some similar contradiction is in the theory. So in that context they use "theory" to mean the axioms alone. This is a common difficulty in moving from one book to another, along with the similar question about whether a theory is required to be consistent. — Carl (CBM · talk) 15:02, 16 June 2011 (UTC)

lede

The lede begins

• In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. Usually a deductive system is understood from context. An element $\phi \in T$ of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms ($T\vdash \phi$) is called a theorem of the theory. Every axiom is also a theorem. A first-order theory is a set of first-order sentences.

The third sentence seems to imply that only the axioms (and not the other theorems) are members of the theory. If that is not intensional should it say instead, say

• In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. Usually a deductive system is understood from context. Each element $\phi \in T$ of a theory T is either an axiom or a sentence that follows from the axioms ($T\vdash \phi$) called a theorem. Every axiom is also a theorem. A first-order theory is a set of first-order sentences.

This is what the language "Many authors require that the theory be closed under logical consequence", which you removed, was describing. Some authors require that the consequences of the theory must also being the theory; others don't. It also varies by context somewhat. — Carl (CBM · talk) 00:37, 17 June 2011 (UTC)

Why mathematical logic?

Why is the page called "Theory (mathematical logic)" instead of "Theory (logic)"? "Theory (logic)" redirects here, and the page "Mathematical logic" says "Mathematical logic is a subfield of mathematics exploring the applications of formal logic to mathematics". However, this page seems to just be about logic, not its application to mathematics, so it seems it should be called "Theory (logic)". Colonial Overlord (talk) 05:22, 12 June 2016 (UTC)

That seems reasonable to me. The page Theory is about something else, so this article needs some kind of parenthetical suffix, but 'logic' or 'mathematical logic' seems OK to me. — Carl (CBM · talk) 14:33, 12 June 2016 (UTC)

"Logic" is such a broad word. I don't think "theory (logic)" is really specific enough. The whole content of this article is what I would normally think of as "mathematical logic", whatever definition of the latter is given in our article. Maybe it's the math-logic article that needs to be fixed. Especially given that, in practice, mathematical logic is more often the application of mathematical methods to logic than the other way around, but that's not important right now.

I could also live with "theory (formal logic)" or something similar. --Trovatore (talk) 18:35, 12 June 2016 (UTC)

About the defintion of "Theory"

In November 1, 2019, the definition was changed from "... a set of sentences in a formal language", to "...a set of sentences in a formal language that is closed under logical implication". This is not false, since both definitions are in use (see here). But, then, "theory" becomes the same as "deductive theory", and this cause some confusion. So, I restored the definition as it was before. Aris Makridis (talk) 12:49, 12 August 2020 (UTC)