Talk:Mathematical logic

Archived discussion

Major reworking

Although this article is Top-priority, it's really barely more than a stub. I'm going to give this article the thorough reworking it needs to get to the quality it should be. Please feel free to help... and don't be surprised at the changes. — Carl (CBM · talk) 15:59, 26 November 2007 (UTC)

Excellent. Unfortunately I am going to be rather busy in real life for a few days, so I can't help much before the end of the week. Just a thought, as I suspect you might be planning to go into rather more detail than there is right now: I don't know if we currently have a definition of what a "logic" actually is. And I am not sure what it is, exactly, as I usually need only first order. But I would imagine that "language = logic + signature", and that deduction rules are related to a logic almost like structures to a signature. I think making clear the modular character of these concepts should really help to get a uniform terminology that makes sense for people from various branches of logic and from universal algebra – necessary for weeding out duplication. (I am not saying this should be part of this article – I haven't thought about it. It's just something I thought I would do some time, and which might be relevant here, perhaps even at an early stage.) In any case, thanks for doing this. I am sure I am going to learn something from the final result as well as from the way you go about it. --Hans Adler (talk) 16:55, 26 November 2007 (UTC)

My first goal is to expand the depth of historical information and to describe the subfields in more detail. I have found it remarkably difficult to find reliable sources that speculate on the nature of logic itself, or define mathematical logic. This is likely because of the culture within math logic of avoiding philosophical rambling. But I have some leads for history books that might prove useful. I expect that once I copy the new version here, other people will round out the coverage.

My goal is to end up with an article that can be put up for A-class review, which includes meeting the scientific citation guideline. — Carl (CBM · talk) 14:51, 29 November 2007 (UTC)

Very good. I just noticed that the French article (fr:Logique mathématique) is largely independent from this one and twice as long. Its introduction makes some interesting points (alas, without footnotes). If you can't easily read French I can put a quick translation here. (And I really like the two footers they are using for the mathematics and logic portals.) --Hans Adler 16:20, 30 November 2007 (UTC)

I copied my working draft here, so that other people can contribute. It is not by any means complete; many paragraphs are just sketches. I plan to add references for all the years in parentheses, just haven't typed them in yet.

The version on French wikipedia isn't bad. You can get google to translate it for you [1]. But I think it spends too much time on symbolic logic, which is only part of mathematical logic. — Carl (CBM · talk) 17:16, 30 November 2007 (UTC)

Hans, thanks for your help this afternoon. The article is, as everyone can see, still very bare-bones with very little exposition. I am adding references, and will eventually convert them to the {{citation}} template. Many of the sections could use rearranging if not complete rewriting. And the history from 1935 to 1950 is almost nonexistent. — Carl (CBM · talk) 21:10, 30 November 2007 (UTC)

Thank you for doing all this work. It's soon midnight for me, so I will probably print the article tomorrow morning to get a better overview. Believe it or not, I learned something very important about model theory from you today. — You noticed that we have contradictory information on the origins of the ε-δ definition of continuity. My impression from what I have seen on the web is that it was first used by Bolzano, then more rigorously by Cauchy (who actually made wrong claims because he didn't think of the problem of uniform convergence), and then rigorously by Weierstraß. The following article should have more precise and reliable information, but as usual I can't read it from home: Walter Felscher, Bolzano, Cauchy, Epsilon, Delta, 2000. --Hans Adler 23:32, 30 November 2007 (UTC)

Regarding the reference to Shoenfield, I think the inline citation should use the year of original publication, because this identifies the era in which the content was written. Later republications are important for purchasing the text but unless the context was changed they aren't going to be accurate about the content. For example, if a book from 1940 was republished in 1990, it's still not going to have information on results proved after 1940. — Carl (CBM · talk) 03:47, 1 December 2007 (UTC)

I agree that that's a problem. For me the balance was only slightly in favor of 2001, so I am not surprised you prefer 1967. I have changed the footnote to "A classic graduate text is the book by Shoenfield (2001), which first appeared in 1967."

An observation: The Citation tag has the year of the first edition as "origyear=1967", although I don't know if that's the correct use (since the current edition seems to be a reprint of the second edition from 1973, and I found no documentation on the intended purpose of origyear). When I started using these tags a few days ago, this would have resulted in something like [1967](2001), but that's no longer the case. --Hans Adler 09:56, 1 December 2007 (UTC)

I'm not sure about the citation tags. Mentioning the original year in prose is fine with me. One area where I am not strong is the early history of model theory, which is why it is currently just a single sentence about Tarski. You thoughts above about the nature of logic are relevant to the section on formal logic. — Carl (CBM · talk) 16:35, 1 December 2007 (UTC)

Well, I hoped that somebody had given a reasonable mathematical definition for what I would call a "logic", but I am beginning to suspect that I was wrong. "Logical systems" in Lindström's theorem come close to what I mean, and so do institutions. But they also include the model relation, which may not be needed for proof theory, and no inference rules. I was looking for a word just for a functor from signatures to languages, which could then be equipped with functorial model relations and functorial inference rules. — Yes, I imagined that you left the model theory bit for me. I am thinking about this.

I have done all the obvious or trivial changes immediately after proof-reading. Now I will soon start with a few things where I am not entirely sure what to do. You might want to have a look at them afterwards. --Hans Adler 18:31, 1 December 2007 (UTC)

I agree the easy changes are getting harder to find, which is grear. There are still a few gaps in the coverage, and I made a list tonight of several more primary sources to cite, but I think the coverage is filling out well. This is good, because the article is approaching the recommended maximum length.

As it stands, the article now has a lot of information about historical developments, and some information about milestones in particular fields. I think it's weak on analysis, criticism, and other "secondary source" material. So my next goal is to try to add a little more criticism (preferably with sources). I'm not used to writing "nontechnical" articles like this, so it's an experiment for me to find an acceptable presentation. — Carl (CBM · talk) 03:57, 3 December 2007 (UTC)

Yes, the article seems to be converging very well. I am glad you have embarked on this experiment, which really looks like it's going to be a great success. I am not sure that I want to know how many hours you spent on it. Did you have time for eating during the weekend? --Hans Adler 11:37, 3 December 2007 (UTC)

Cantor

I'm delighted to see the improvement in the article, and have just one suggestion.

Cantor first appears in this article in the discussion of the well-ordering principle. Shouldn't his contribution be mentioned earlier in the history section?

Rick Norwood 14:25, 3 December 2007 (UTC)

Yes, certainly, a synopsis of Cantor's work in set theory needs to be added to the 19th century section before the article is complete. Also Hermann Weyl's Das Kontinuum needs to be mentioned. Thanks for reading through the article and giving other suggestions, or editing it. — Carl (CBM · talk) 14:38, 3 December 2007 (UTC)

Vaught's Conjecture

I noticed that in the section "Model theory" it is written that Robin Knight refuted Vaught's Conjecture. However there was an error in Knight's 2002 construction and circa 2003-2004 there were attempts to patch it, but not everyone was satisfied with his arguments. Unless I've missed some new development here in the past few months or so, there's no consensus yet in the model theory community about the status of Vaught's Conjecture.

Skolemizer (talk) 06:41, 5 January 2008 (UTC)

I had never heard about this result before I read it in this article, but since it fell into a period in which I was not very active in mathematics I assumed I had just missed it and was going to read it. Now based on your warning I have asked an expert, who told me that there is in fact no consensus that the counterexample is correct. I think the proposed example should not be mentioned in this article, and I will remove it. --Hans Adler (talk) 00:18, 9 January 2008 (UTC)

This is very interesting. I'm no model theorist, and people I respect referred to Knight's result as a proof at some point, so I assumed they were correct. Wasn't Knight's result published? Thanks for correcting my error, in any case. I'm glad other people are watching these pages. Are there other things that could be added to the model theory sections? — Carl (CBM · talk) 00:15, 11 January 2008 (UTC)

So far as I know it was never published. There was a special session on this at the British Logic Colloquium 2002, so I would assume that's how it became well known to people outside stability theory. The example is extremely complicated, and so it probably took some time for people to make up their minds. His home page has a second draft from January 2003 and more corrections from November 2003. He also says there that he is working on a simplified example which he hopes to have complete "in June" (presumably June 2005, since the page was last changed in May 2005). So unfortunately it looks like this example is dead.

I am feeling a bit guilty that I haven't revised the section on model theory otherwise, as I meant (and promised) to do. I find it very hard to describe what I think is a large, heterogeneous subject in just a few words. --Hans Adler (talk) 11:00, 11 January 2008 (UTC)

CS

it's a branch of CS as well. source: http://wapedia.mobi/en/Outline_of_computer_science#1. —Preceding unsigned comment added by 98.208.55.34 (talk) 07:06, 2 May 2009 (UTC)

Not a reliable source. Note that even if you find a source or two, it's not good enough if it's a fringe view (though it would be reasonable in that case to mention it as a minority view).

On the face of it, though, the claim is just obviously wrong. Math logic considerably predates computer science, so it can't be a "branch" of it. --Trovatore (talk) 07:20, 2 May 2009 (UTC)

On another note, the cycle is bold-revert-discuss. You've been bold, and been reverted. Now it's time for you to see if you can gain consensus. Your orders not to revert, in your edit summaries, are not going to accomplish anything, except piss people off. --Trovatore (talk) 07:23, 2 May 2009 (UTC)

Wapedia is a Wikipedia mirror. You probably meant to refer to Outline of computer science. The outline is right: Computer science has mathematical foundations, and these are in some sense considered to be part of computer science. But not everything that belongs in such an outline is a branch of computer science. Almost everything is in section J of the ACM Computing Classification System. [2] This doesn't mean that education, law, manufacturing, archaeology, health, psychology, music, military etc. are branches of computer science. --Hans Adler (talk) 07:43, 2 May 2009 (UTC)

Mathematical logic is not a branch of computer science. Our outline of computer science ought to be fixed; I left a note on its talk page. That outline confuses two things at present: topics that are learned when studying CS, and things that are part of the CS research landscape. The latter are what constitute "branches" of CS. If all the prerequisites counted as "branches" then calculus would be a branch of physics, economics, biology, etc. — Carl (CBM · talk) 11:10, 2 May 2009 (UTC)

Note that your edits will be reverted until you can provide any reliable sources! —Preceding unsigned comment added by 98.208.55.34 (talk) 20:48, 2 May 2009 (UTC)

Can you point out any source, apart from that wikipedia list, that claims mathematical logic is a branch of computer science? It's hardly compelling to use one WP article as a source for another. — Carl (CBM · talk) 22:24, 2 May 2009 (UTC)

Early history

I reworked some edits to the "Early history" section. Stuff about the 19th century belongs in the following section. In order to have a global viewpoint, and avoid historical myopia, we do need to recognize that non-Western cultures had their own traditions of logic. The dominance of Greek influence in medieval and then 19th century work is, most likely, simply because non-Western work was much less known at the time. The same pattern has repeated itself in many areas of mathematics, where there was much duplication of effort (for example, Pascal's triangle). — Carl (CBM · talk) 19:45, 2 May 2009 (UTC)

Modal logic

Is modal logic really established as part of mathematical logic? Given the ease with which Kripkean modal logics can be expressed in first-order logic, the case for modal logic is not directly one of expressiveness.

In computer science, modal logic is important because of the (relatively) good complexity classes of its various decision procedures. In philosophical logic it is important because of its more natural relationship to natural language. But are there any areas of core mathematical logic where modality is a valuable tool? — Charles Stewart (talk) 14:17, 18 June 2009 (UTC)

Is it a core part of mathematical logic? No, certainly not. But it is important for the more philosophical side, and has the interesting applications to provability logic that are mentioned. So two sentences seems to me like a reasonable amount of time to spend on it, in the spirit of being "just slightly broader than the average mathematical logic textbook". — Carl (CBM · talk) 14:29, 18 June 2009 (UTC)

Algebraic logic

This deserves a section. It may be best to treat it together with categorical logic. — Charles Stewart (talk) 14:22, 18 June 2009 (UTC)

At the moment category theory is mentioned but not in the guise of categorical logic (to be fair, we also don't mention linear logic, etc.). Should we have a paragraph on categorical logic? I'm not sure yet, so the answer is probably yes. — Carl (CBM · talk) 14:38, 18 June 2009 (UTC)

In Mathematical logic#Algebraic logic, we link to Boolean algebra. Since that page is a DAB, does anyone object to replacing that mention with a piped link to Boolean algebra (logic)? The latter seems to be the meaning of 'Boolean algebra' that is intended here. EdJohnston (talk) 14:58, 18 June 2009 (UTC)

Sorry about that. The right link is Boolean lattice. Boolean algebra (logic) is a POV fork of Propositional logic. The latter seems to be in worse shape than I remember. — Carl (CBM · talk) 15:03, 18 June 2009 (UTC)

Carl: thanks for your excellent precis. It may be best to duck stating the relationship, since there is controversy over whether categorical logic is algebraic logic or some quite different way of doing logic algebraically. The right link is Boolean lattice. Boolean algebra (logic) is a POV fork of Propositional logic. The latter seems to be in worse shape than I remember. - oh god, not again! We need some final resolution of this wikisore, I guess an RfC. I don't have either the appetite or time to put one together soon, though. — Charles Stewart (talk) 17:20, 18 June 2009 (UTC)

Merge/Redirect Symbolic logic here

Unless that topic is a different field of study somehow (can't tell from the stubby article), I propose it be turned into a redirect here and mentioned as a synonym. Pcap ping 08:39, 19 September 2009 (UTC)

Based on a few books I've looked at [3], [4], [5] (which are even more basic than the so-called metalogic books), it appears that symbolic logic is the former/traditional name given by philosophers to mathematical logic. Pcap ping 08:48, 19 September 2009 (UTC)

If somebody needs a ref [6] this philosophy book gives them as synonyms. Pcap ping 08:54, 19 September 2009 (UTC)

Even more clearly stated here. Pcap ping 09:01, 19 September 2009 (UTC)

Oddly enough, Jon Barwise defined mathematical logic as only a branch of symbolic logic [7]. But he makes no mention of any other branches of symbolic logic... Pcap ping 11:26, 19 September 2009 (UTC)

But I think we can take Hilbert's and Ackermann's word that it's the same topic. [8]. Pcap ping 11:30, 19 September 2009 (UTC)

Church also says they're the same. [9]. Pcap ping 11:40, 19 September 2009 (UTC)

We can also get a philosopher, Rudolf Carnap, to agree that they are the same. [10]. Pcap ping 11:48, 19 September 2009 (UTC)

This 2008 philosophical encyclopedia says that mathematical logic includes symbolic logic. [11]. Pcap ping 11:54, 19 September 2009 (UTC)

This merge seems OK to me. Honestly I don't know exactly what symbolic logic is, but the claim that it's purely about syntactic relationships, as the lead currently says, I think is just false. My understanding is that it's a mostly-disused phrase for mathematical logic, surviving in traditional titles such as Journal of Symbolic Logic but not much as a description for current research. --Trovatore (talk) 23:16, 19 September 2009 (UTC)

Yeah it's the same thing. A merge is appropriate. Pontiff Greg Bard (talk) 23:19, 19 September 2009 (UTC)

While I have no strong opinion one way or the other about the merge, there is a difference between formal logic, as in Logic for Mathematicians by Hamilton, and the (usually) informal logic used by mathematicians to prove theorems. Proofs of theorems in refereed journals almost never use formal mathematical logic, unless the topic of the paper is formal mathematical logic or, sometimes, axiomatics or set theory. Rick Norwood (talk) 14:11, 20 September 2009 (UTC)

There was a time when Wikipedia explicitly wanted to have an article on every subject that Wolfram Mathworld had an article on. Here, fyi, is a list of their articles on logic:

• Logic (Wolfram MathWorld)

The formal mathematical study of the methods, structure, and validity of mathematical deduction and proof. In Hilbert's day, formal logic sought to devise a complete, ...

• Formal Language (Wolfram MathWorld)

In mathematics, a formal language is normally defined by an alphabet and formation rules. The alphabet of a formal language is a set of symbols on which this language is ...

• Symbolic Logic (Wolfram MathWorld)

The study of the meaning and relationships of statements used to represent precise mathematical ideas. Symbolic logic is also called formal logic.

• Intuitionistic Logic (Wolfram MathWorld)

The proof theories of propositional calculus and first-order logic are often referred to as classical logic. Intuitionistic propositional logic can be described as classical ...

• Equational Logic (Wolfram MathWorld)

The terms of equational logic are built up from variables and constants using function symbols (or operations). Identities (equalities) of the form s=t, (1) where s and t are ...

• Combinatory Logic (Wolfram MathWorld)

A fundamental system of logic based on the concept of a generalized function whose argument is also a function (Schönfinkel 1924). This mathematical discipline was ...

• First-Order Logic (Wolfram MathWorld)

The set of terms of first-order logic (also known as first-order predicate calculus) is defined by the following rules: 1. A variable is a term. 2. If f is an n-place ...

• Predicate Calculus (Wolfram MathWorld)

The branch of formal logic, also called functional calculus, that deals with representing the logical connections between statements as well as the statements themselves.

• Premise (Wolfram MathWorld)

A premise is a statement that is assumed to be true. Formal logic uses a set of premises and syllogisms to arrive at a conclusion.

• Syllogism (Wolfram MathWorld)

A syllogism, also known as a rule of inference, is a formal logical scheme used to draw a conclusion from a set of premises. An example of a syllogism is Modus Ponens.

Whether Wikipedia still wants to have an article on all these topics, I do not know. Rick Norwood (talk) 14:34, 20 September 2009 (UTC)

"Symbolic logic" might be used sometimes as a synonym for basic proof theory. But I don't see any way to classify model theory and recursion theory as part of "the area of mathematics which studies the purely formal properties of strings of symbols." Now, I don't really think that is a good definition of "symbolic logic" in the first place, but it certainly is not a definition of "mathematical logic". So I agree with Trovatore's assessment above. — Carl (CBM · talk) 19:36, 20 September 2009 (UTC)

Not sure how they were in 2007, but today symbolic logic and formal logic are merely WP:DICTDEFs on Mathworld. Pcap ping 14:16, 20 September 2009 (UTC)

Also, they define logic to be mathematical logic: "the formal mathematical study of the methods, structure, and validity of mathematical deduction and proof." Most philosophers would disagree that logic only deals with mathematical proofs. So, MathWorld is not necessarily the best source for definitions that aren't strictly mathematical. Pcap ping 04:57, 21 September 2009 (UTC)

Mathworld defs for comparison:

• Symbolic/formal logic: "The study of the meaning and relationships of statements used to represent precise mathematical ideas. Symbolic logic is also called formal logic."
• (mathematical) logic: "The formal mathematical study of the methods, structure, and validity of mathematical deduction and proof.

A distinction without a difference? Pcap ping 05:03, 21 September 2009 (UTC)

Let's please not be relying on Mathworld for, well, anything really. The corpus of mathematical articles on WP is vastly superior to Mathworld by now, and most of the time when Mathworld shows up, it's to cause trouble (usually, someone copying some silly MW neologism).

In this case, MW's definition of mathematical logic is certainly wrong. That might be what the phrase should have meant, but it's not what it means in contemporary discourse. Mathematical logic is a collection of fields of mathematics that have some historical connection with logic — as Carl says, set theory, recursion theory, model theory, and proof theory (and one probably ought to throw in category theory, and could make a case for universal algebra). --Trovatore (talk) 05:19, 21 September 2009 (UTC)

MSC2010

The new classification divides mathematical logic a bit differently. In particular algebraic logic is considered a separate subfield containing categorical logic etc. contents. Thoughts on integrating this structure in the article? Pcap ping 11:10, 20 September 2009 (UTC)

I see that algebraic loigic is actually mentioned, but in the "formal logic" section. Speaking of which: the classification has a "general logic" subfield which roughly corresponds to our "formal logic" section (which has a silly heading because all mathlogic is formal). In MSC2010 this is considered to contain quite a bit more stuff than what's mentioned here, including substructural logics, many-valued logic, type theory etc. I know this stuff isn't normally included in mathlogic textbooks (well, Peter B. Andrews's book cited here is an exception wrt to type theory), so no they should not have more than a passing mention here, but even that is currently lacking (except for type theory in the history section). Pcap ping 11:35, 20 September 2009 (UTC)

The MSC is not, of course, the controlling definition of "mathematical logic". The article here does mention algebraic logic and categorical logic, but I don't think they should be very heavily emphasized (algebraic logic should be covered in more depth than categorical logic, which should just be alluded to).

Many-valued logics should be added to the section "Nonclassical and modal logic", and type theory should be added to the "formal logics" section. It's hard to remember everything at first.

Not all of mathematical logic is formal, by the way. The meaning there is like the distinction between "formal proof" and "natural language proof". Fields such as set theory and model theory are usually conducted using natural-language proofs, rather than being explicitly treated within a formal logic. So "formal logics" are the ones in which we have a notion of a formal proof. — Carl (CBM · talk) 13:38, 20 September 2009 (UTC)

"MSC is not, of course, the controlling definition" -> A classification system by necessity appears to give equal importance to the topics it includes. (Well, except for their relative placement in the tree). Of course, we shouldn't give equal coverage to, say, modal logic and first-order logic in this article (WP:WEIGHT), and more obscure topics in the rather comprehensive MSC shouldn't even be mentioned here. I was merely asking whether some of the current structure/contents is by design or by accident/omission. Pcap ping 14:29, 20 September 2009 (UTC)

"Not all of mathematical logic is formal." -> This is similar to the argument raised by Rick above (to argue that symbolic logic is not necessarily the same as mathematical logic.) It's true that natural language proofs actually dominate in mathematics; completely formal, that is mechanize[d/able] proofs are rare in mathematical practice. But my understanding is that mathematical logic deals exactly with the metatheory/metalogic of those rather than of the natural language proofs, with the assumption that one can mechanically formalize them if necessary. (This assumption isn't that easy to put in practice; see for instance QED project -- it's really called QED manifesto, by the way. There's opposition to this effort, I can't find a link off the top of my head, but some mathematicians wrote that mechanized proofs are often uninsightful, so such projects are a waste of time.) Pcap ping 14:49, 20 September 2009 (UTC)

FOM post "What is a proof?" echoes what I wrote in the above paragraph. Pcap ping 16:41, 20 September 2009 (UTC)

I don't see how model theory and (even worse) recursion theory can be said to study the metatheory of formal proofs? Mathematical logic includes more than proof theory; see below. — Carl (CBM · talk) 19:26, 20 September 2009 (UTC)

Actually, most of the time I think "mathematical logic" means "symbolic" or "formal" logic, and when it doesn't people just say "logic". Rick Norwood (talk) 14:52, 20 September 2009 (UTC)

For almost every intent and purpose, "mathematical logic" simply means the union of proof theory, recursion theory, model theory, and set theory. None of the latter three of those could possibly be called "symbolic logic".

As a researcher in mathematical logic, if someone told me they studied "logic", I would begin by asking what department they work in, because studying "logic" on its own does not mean very much to me. — Carl (CBM · talk) 19:25, 20 September 2009 (UTC)

Perhaps you are too exclusionary? After all, MSC does include a fairly beefy general logic area besides those four you've mentioned. It's true than many of those are studied with respect to some aspect like proof theory or model theory, which philosophers would call metatheory or metalogic. I don't think Britannica is a good example to follow for organization here, but they take that approach; see my post on Arthur Rubin's talk page. Pcap ping 03:44, 21 September 2009 (UTC)

4=5?

Is mathematical logic consistent? The "Subfields and scope" section says:

Contemporary mathematical logic is roughly divided into four areas: set theory, model theory, recursion theory, and proof theory and constructive mathematics.

which would seem to prove that 4=5 ;-). Can someone straighten this out? There are two obvious possible solutions and I defer to the experts to figure out which is better. 70.90.174.101 (talk) 05:33, 21 September 2009 (UTC)