This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | |||||||||||
|
How is this related to the abstract definition involving categories?
editSee Handbook of Mathematical Logic. [1] Or Handbook of philosophical logic. [2] Hans Adler 18:16, 19 November 2009 (UTC)
- To speak to your references specifically, what they call an "algebraic theory" is a category whose internal language is capable of expressing an algebraic theory. Category theorists have a habit of re-defining terms already in use to mean particular kinds of categories. For example, category theorists will claim that "a poset is a category with at most one morphism between any pair of objects" even though most non-category-theorists might claim that there are posets which are "not" categories. AshtonBenson (talk) 08:58, 25 November 2009 (UTC)
If the definition is meant to say that an algebraic theory is given by the requirement that certain equations (with free variables) must be true whatever you put into the variables, then this is normally used as an equational class or variety (universal algebra). This is not entirely clear because "Inequalities and quantifiers are specifically disallowed" sounds as if might not be meant to mean , as the latter formula contains a quantifier. Hans Adler 18:21, 19 November 2009 (UTC)
- Any algebraic theory can be expressed in the internal language of a category with finite products (a "Lawvere theory"). The convention in FOL is that any free variable is "implicitly" universally quantified. This way all sentences of propositional logic (which has no quantifiers, but acts as if free variables were universally quantified) are "automatically" valid sentences of first-order logic. AshtonBenson (talk) 23:44, 22 November 2009 (UTC)
- Sorry, but as a professional model theorist I can tell you with absolute certainty that it is not "the convention in FOL" that any free variable is implicitly universally quantified. I am of course familiar with this convention from universal algebra, but I have never seen it in logic proper, and certainly not in first-order logic. It may be a convention that is used in some specific field, but it's definitely not a general convention that we can use without comment. Such a convention would make it extremely complicated to actually work with formulas.
- You obviously didn't mean propositional logic when you wrote "propositional logic". Propositional logic is only about boolean variables. It does not say anything about an underlying set. You obviously mean to talk about a weak form of predicate logic whose strength is between universal algebra (with relations) and first-order logic.
- Oh, and you are abusing the word "sentence" as if sentence (mathematical logic) was a synonym for formula (mathematical logic). It is not. It is the special case without [edited: I meant to say free here] variables.
- These are very fundamental conventions, among the very few universally consistent ones in a field that generally suffers from inconsistent terminology. I have never met anyone who did logic in philosophy, mathematics or computer science who used these words in such a non-standard way. If you are writing about a tiny subfield of logic that has developed its own idiosyncratic terminology then you could at least mention it in your articles, so that others can help you after looking things up.
- Please provide sources for your new articles so that I (and other interested editors) can look up the proper definitions. Otherwise the articles may have to be deleted or rewritten to describe the standard meanings of their titles. In their current state they are extremely misleading. Hans Adler 00:17, 23 November 2009 (UTC)
- Re AshtonBenson: I am also not sure what you mean by "propositional logic" there. — Carl (CBM · talk) 20:29, 23 November 2009 (UTC)
- Congratulations, Hans, you have managed to spend five paragraphs noting the fact that I transposed "propositional" and "predicate" in my casual remark. I too am a professional model theorist, albeit one who edits Wikipedia far later at night than he would (for reasons of accuracy) ever do work on a serious publication.
- The convention that free variables behave -- with respect to provability -- as if they were universally quantified is called the Closure Theorem and is proved near the bottom of page 32 of Shoenfield's Mathematical Logic as a trivial consequence of the conventions established in that book. AshtonBenson (talk) 08:35, 25 November 2009 (UTC)
- I have linkified the term "internal language" in my earlier post (sadly, Wikipedia comes nowhere close to nLab on this topic). Perhaps this will shed some light on the situation. AshtonBenson (talk) 08:43, 25 November 2009 (UTC)
- I can't look it up in Shoenfield right now because my library doesn't have that book (and all the copies that used to exist in Vienna's maths library seem to have disappeared). Will do so when I get home. So you are using a convention that theories may contain formulas with free variables as well as sentences? I have never encountered that before. If that's somewhat common, the article needs to mention it. It needs some work anyway, after Gregbard's latest additions.
- Sorry that I was so cross and showed it. I have an unfortunate tendency to react that way when people create tiny sub-stubs with only a definition that I can't even make sense of. Hans Adler 09:07, 25 November 2009 (UTC)
- I looked it up in Shoenfield's book now. On page 22 he defines a theory as a kind of formal system, and as you say part of it is formulas that may have free variables. I don't remember seeing this point of view before. So far I only knew the definitions of a theory as a set of sentences, or as a set of sentences closed under implication. Of course that doesn't make the definition of algebraic sentence correct outside a very special context, since we do need the ability to distinguish sentences and formulas in contexts in which we want to deal with algebraic formulas, formulas representing equivalence relations, etc. Hans Adler 21:32, 25 November 2009 (UTC)
How about Lawvere's definition, and details, and references?
editI've been looking into ways of extending this article by adding a section with Lawvere's definition; and by adding a bunch of references, from Lawvere's '63 work to nCatLab; now I see that there was already a discussion... so? A professional model theorist might probably do it better than me, so?
I'll update it in a couple of days; hope nobody objects. Not being a logician, but a categorist, I'll focus on the categorical aspects, of course.
Integer quotients
editThe text of Example includes phrase with integer quotients. This phrase should be explained/defined or a reference should be provided. Wlod (talk) 05:42, 2 July 2013 (UTC)
Examples
editI have just added some more examples. The examples I have chosen may not be the most common examples, so I would appreciate it if someone would add the common examples (I am not an expert in mathematical logic) – I know the article says that algebraic theories are almost the same as theories of algebraic structures, but I wanted to be completely sure so I only added theories for which I was able to find references stating that they are algebraic. Joel Brennan (talk) 18:05, 19 January 2021 (UTC)