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)

There is no page on Formal Logic! It redirects to this page, and I believe it is missing a huge part. — Preceding unsigned comment added by 64.89.212.40 (talk) 04:24, 23 December 2014 (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)

We certainly need to have a global viewpoint. However, failing to note the Greek influence in Western cultures is also a mistake. There's a clear historical path from Aristotle, the Stoics, medievals, and through to the logical systems as developed and extended by logicians such as Frege, Peano, and Russell; omitting that omits the key parts of its history. Dwheeler (talk) 19:28, 11 August 2019 (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)

Modal logic is part of logic. Indeed, a significant part of Aristotle's work on logic is devoted to it. Dwheeler (talk) 19:23, 11 August 2019 (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

• Absolutely, amazing... Nice job with merging symbolic logic, which is the logic of language meaning and mathematical logic which is the logic of mathematics... Are you a Republican? Way to confuse the topics... Maybe if you do a search on ancient civilizations, you will only come up with Chariots of the Gods and think that all earlier civilization were founded by extraterrestrials... Then we can merge the 2 articles Ancient civilization and Extraterrestrials... Hey, what do you know? If we keep doing this, we can really condense Wikipedia down to a more "manageable" level... Wow, someone really needs to return to college... The entire article that was here on symbolic logic, which I used & contributed to during a semester is entirely gone... There is not a single reference to symbolic logic in this article... You have deleted the entire subject on Wikipedia... As restricted intellectually, as the topic is, it should still be a part (article entry) of Wikipedia... Hey, maybe we can merge Calculus and Algebra - they sort of look the same... Stevenmitchell (talk) 22:55, 1 April 2010 (UTC)

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)

I would never have found my way here (Mathematical logic) without the separate Symbolic logic page, which I found very useful in itself, using terms familiar from my studies back in the 60's. There are authors (e.g. Suzanne K Langer, 1937) who view Mathematical logic as a sub-divison of Symbolic logic. I feel that considerations of "user friendliness", particularly towards older readers, weigh against a merger. JoesphPGrant (talk) 20:51, 9 October 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)

I don't believe that, today, category theory is considered part of mathematical logic by either category theorists or mathematical logicians. Perhaps in 50 years, it will be, but that's hard to predict. — Carl (CBM · talk) 10:43, 21 September 2009 (UTC)

And yes, matheworld's definition of "mathematical logic" is wrong there, unless recursion theory has suddenly morphed into the study of formal proofs. — Carl (CBM · talk) 10:48, 21 September 2009 (UTC)

Pcap proposed this merger 6 months ago. If I understood everything correctly, then everybody agreed, except JoesphPGrant, who created an account to remind us that some older people are more likely to look for the present article under "symbolic logic".

(Historical digression: Talk:Symbolic logic shows that the articles were merged in the past, but then forked again just because a confused editor found a loopy link from the present article to itself via the redirect at Symbolic logic. Apparently nobody ever had a clear idea what the scope of that article should be.)

In my opinion the natural scope of Symbolic logic would be mathematical logic as it was practised in roughly the first half of the 20th century. If we ever need to split this article per summary style, or need to split history of logic in that way, the title is available for that purpose. But I don't think that's going to happen soon.

I have redirected Symbolic logic to Mathematical logic, but left the redirect in Category:Logic so it is easier to find. I think this takes care of JoesphPGrant's concern. A small number of languages still have the split, probably because they got it from us. The Finnish Wikipedia has only an article on Symbolic logic, so I have added their interwiki link to the present page. There wasn't much contentat Symbolic logic, and I have not merged any of it anywhere. Some of it seemed to be wrong, and some of it is very elementary and doesn't really belong in such an article anyway. If someone wants to salvage something, there is a huge choice of articles related to propositional logic; perhaps one of them is suitable.

I have left Talk:Symbolic logic in its old place. It doesn't seem to be very relevant to anything other than the history of the merged article itself. Hans Adler 13:51, 25 March 2010 (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)

The "big four" areas are also reflected in the Handbook of mathematical logic. There are almost certainly some minor areas that will be hard to categorize as proof theory, model theory, recursion theory, or set theory. But most of the "general logic" category is considered proof theory in practice. On the other hand, not everything that involves the word "logic" and is studied by mathematicians is part of mathematical logic.

Fundamentally, though, the MSC is not intended to define mathematical logic, or anything else. For example, the MSC has a whole section on computer science (68), but this obviously doesn't mean that computer science is claimed to be part of mathematics. Similarly, simply because some topic is classified under 03 does not mean it is really claimed to be part of "mathematical logic"; it may be that there is simply no better place to put that topic. — Carl (CBM · talk) 10:41, 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)

It appears to me that "proof theory and constructive mathematics" are being lumped together here, since otherwise we'd use the Oxford comma. However I'm not sure it's an entirely defensible togetherlumping. While it is true that historically a lot of proof theorists have come from an ontologically minimalist tradition, that's not the same thing as saying they're constructivists; conversely, constructivists are by no means limited to proof theory.

I wouldn't separate constructivism out as a separate area, really. Constructivists have their own versions, even if they're sometimes scarcely recognizable, of all four areas. --Trovatore (talk) 07:02, 21 September 2009 (UTC)

Note that part D of the Handbook of Mathematical Logic is entitled "Proof theory and constructive mathmatics". — Carl (CBM · talk) 10:19, 21 September 2009 (UTC)

Thanks. I edited it for clarity but feel free to revert if you think I went too far. 70.90.174.101 (talk) 02:36, 24 September 2009 (UTC)

Collatz conjecture

(Post moved to mathematics reference desk and deleted by poster)

As I just suggested at Talk:Number theory, you should (a) take this to mathematics reference desk instead of posting on article talk pages; (b) explain your proof strategy in English before formalising it. Gandalf61 (talk) 09:26, 2 October 2009 (UTC)

Thanks.--Gilisa (talk) 09:55, 2 October 2009 (UTC)

logic in 21st century

This article (written in 2000) is pretty interesting and may be worth a mention:

Samuel R. Buss, Alexander A. Kechris, Anand Pillay, Richard A. Shore.

"Prospects for mathematical logic in the twenty-first century."

Journal of Symbolic Logic 7 (2001) 169-196.

http://math.ucsd.edu/~sbuss/ResearchWeb/FutureOfLogic/paper.pdf

pdf link from: http://math.ucsd.edu/~sbuss/ResearchWeb/FutureOfLogic/index.html

69.228.171.150 (talk) 06:50, 7 November 2009 (UTC)

Symbolic Logic and Mathematical Logic are not the same thing

Absolutely, amazing... Nice job with merging symbolic logic, which is the logic of language meaning and mathematical logic which is the logic of mathematics... Are you a Republican? Way to confuse the topics... Maybe if you do a search on ancient civilizations, you will only come up with Chariots of the Gods and think that all earlier civilization were founded by extraterrestrials... Then we can merge the 2 articles Ancient civilization and Extraterrestrials... Hey, what do you know? If we keep doing this, we can really condense Wikipedia down to a more "manageable" level... Wow, someone really needs to return to college... The entire article that was here on symbolic logic, which I used & contributed to during a semester is entirely gone... There is not a single reference to symbolic logic in this article... You have deleted the entire subject on Wikipedia... As restricted intellectually, as the topic is, it should still be a part (article entry) of Wikipedia... Hey, maybe we can merge Calculus and Algebra - they sort of look the same... then delete Calculus and we're all set... Stevenmitchell (talk) 23:12, 1 April 2010 (UTC)

Whom you are addressing, and in what way you connect that person's actions with party affiliation, is obscure to me. As I've said above, my understanding of the term symbolic logic is that it's simply an older term for mathematical logic (which by the way is not the same thing as "the logic of mathematics"). It's a term that carries a certain amount of philosophical baggage, that baggage being the most likely reason it's fallen into disuse. If you have a different understanding, one that you can make precise and for which you can give references, by all means share. --Trovatore (talk) 19:29, 2 April 2010 (UTC)

I don't see any "symbolic logic" article at SEP. I generally think of "symbolic logic" as being topics like Venn diagrams, not what we usually think of as mathematical logic. The Mathworld article "Symbolic Logic" cited as the the only reference for the old version (now merged) of symbolic logic, consisted of the single sentence "The study of the meaning and relationships of statements used to represent precise mathematical ideas. Symbolic logic is also called formal logic." with a few "see also" pointers. It might be reasonable to merge some of the old content of "symbolic logic" that didn't make it into this article, into philosophical logic instead of here. 66.127.52.47 (talk) 17:48, 5 April 2010 (UTC)

• It looks to me like the old symbolic logic article was pretty scattered and the topics in it that aren't in the mathematical logic article, are still to be found elsewhere. So I'm thinking of removing the "missing treatment" tag. Let me know your views. 66.127.52.47 (talk) 19:04, 7 April 2010 (UTC)
  • I am the ghost of Ludwig Wittgenstein. See me after class. 90.205.92.37 (talk) 08:13, 7 April 2011 (UTC)

propositional calculus = formal logic?

same thing? very different? do we need 'see alsos' between the two? (I don't know for sure since I only studied it as an undergrad.)  TyrS  chatties  04:35, 14 February 2011 (UTC)

I don't think we need more see also links, but I added a link from the text here to propositional logic. — Carl (CBM · talk) 12:50, 14 February 2011 (UTC)

Formal logic is usually divided into two parts, propositional calculus and predicate calculus. Because "calculus" has today a more common meaning: "the study of limits, derivatives, integrals, and infinite series", I prefer propositional logic and predicate logic, but both phrases are used. Rick Norwood (talk) 13:38, 7 April 2011 (UTC)

Pronunciation guide ;-)

[12]. Tijfo098 (talk) 19:12, 12 April 2011 (UTC)

If mathematical logic is a branch of math..?

is it ever a pre req for other math classes like finite math. Would geting a good grade in mathematical logic convince a counselor to let you skip certain classes? Poppurrpop (talk) 22:42, 23 April 2012 (UTC)

You might consider asking this question at WP:RD/MATH. This page is for discussing improvements to the article. --Trovatore (talk) 22:45, 23 April 2012 (UTC)

Definitions of mathematical logic

I have an objection to the restricted sense given to the expression "mathematical logic". It is true that on the one hand it means what you say, that is the exploration of mathematical concepts and workings by means of logic. On the other hand, in a way the converse is true, that is the formalisation and expression of logic by means of typically mathematical disciplines (or in other words the application of mathematical theories and systems to logic). This is especially the case historically, with the developments brought about by the work of the likes of De Moivre and in particular Boole (whose algebra fit perfectly logic concepts that were earlier handle through different means). The history of the intertwined relationship between logic and mathematics, I agree, is far from linear and id still in fruitful progress, but for such reasons I endorse a two-way view on it. — Preceding unsigned comment added by 2A01:E35:8AD5:C150:790F:3BD7:736A:B759 (talk) 11:49, 12 November 2013 (UTC)

Goedel sentences

The Goedel sentence of a consistent theory is true. That is what reliable sources say, and is also the fact, and that is what we should say. Not to say it risks continuing the confusion promulgated by the popularizers, all this nonsense about the sentence having a truth value that is in some way problematic. It's not problematic at all — it asserts that there is no natural number having a certain primitive-recursive property, and in fact, there is no such number, because if there were, the theory would be inconsistent, contrary to hypothesis.

It is true that there are nonstandard models of arithmetic satisfying the negation of the sentence. But these are nonstandard models. Truth sempliciter of arithmetic statements is the same as truth in the standard model. The fact that the nonstandard models are "useful" has nothing to do with anything. --Trovatore (talk) 18:22, 26 May 2015 (UTC)

"Truth" in mathematics is a technical term. It is not universally accepted that a formal sentence can be "true" or "false" in an absolute sense at all - "truth" is a model-specific property. The fact is that there provably exist nonstandard models of arithmetic that obey the peano axioms, and whose theories do not contain contradictions. To claim otherwise involves importing a distinctly non-formal definition of "truth" and "consistency." It is true to say that the Goedel sentence is true *in the natural numbers*, but it's not well-justified to treat truth in the natural numbers as some sort of privileged "absolute truth." 128.8.140.59 (talk) 18:42, 26 May 2015 (UTC)

The Goedel sentence is an arithmetic statement. That means that the natural numbers are what it is about. (In particular, it is not about the objects of discourse of the formal theory whose Goedel sentence it is, unless that formal theory happens to be a theory of arithmetic. So for example the objects of discourse of ZFC are sets, not natural numbers, but the objects of discourse of the Goedel sentence of ZFC are natural numbers.)

It is important, and sourceable, to say that the Goedel sentence of a consistent theory is true. There is far too much confusion on this point, especially from the popularizers, who like to give the Goedel results a sort of misty glow of something that can be hey-neither-really-true-nor-really-false-wow-man-heavy. --Trovatore (talk) 18:55, 26 May 2015 (UTC)

I agree with the IP editor that Wikipedia articles should not take a platonist POV. Even when authors say it's "true" we all know enough to realize they may only mean that it follows from ZFC, and may or may not endorse the notion that ZFC is "real." Anyway, what is the problem with adding a few more words to say explicitly it satisfies this theory but not that one? --Sammy1339 (talk) 18:59, 26 May 2015 (UTC)

I'm not sure I follow you. What do you mean "it satisfies this theory but not that one"? I can't tell what "it", "this theory", or "that one" are. --Trovatore (talk) 19:06, 26 May 2015 (UTC)

Okay, correct me if I'm wrong because I'm just a stupid geometer, but I think the situation here is that we have a statement about a theory that can interpret "arithmetic," and when the model of arithmetic is N, it is true, but when the model of arithmetic is the non-negative hyperreal integers, it is false. Is that right? If so, could the article say that? --Sammy1339 (talk) 19:33, 26 May 2015 (UTC)

Well, close. There isn't any "the" hyperfinite numbers, per se. There are various nonstandard models (but only one standard one, up to isomorphism). Some of the nonstandard models satisfy the sentence, and some don't. But the standard model definitely does satisfy it, and that's what "true" means unless otherwise qualified.

The problem with this line of discourse is that it leads into the narrative, "oh, well, maybe it's a nonstandard model that's correct, who's to say?". But that's not really a coherent view. If you're a realist about models, then that's abundantly enough Platonism to guarantee that the Goedel sentence of a consistent theory is true. If you're not a realist about models, then I think you owe some sort of account of what you mean when you drag them into the discussion. --Trovatore (talk) 21:17, 26 May 2015 (UTC)

This presupposes that the idea of a "correct" model is a coherent one. This is a contentious claim. 96.231.153.5 (talk) 21:43, 26 May 2015 (UTC)

Well, no, it really doesn't. If there are models, then that's enough realism to justify the claim that the Goedel sentence of a consistent theory is true. If you're enough of an anti-realist to have doubts about that proposition, then you owe an explanation about what you can possibly mean when you bring them into the discussion. --Trovatore (talk) 22:00, 26 May 2015 (UTC)

Also — it is a standard convention in mathematical discourse to talk like a realist whether you are one or not. That convention should be observed here too. An explanatory note could be used to give an overview of the deeper issues. --Trovatore (talk) 22:12, 26 May 2015 (UTC)

Well, I'm not a realist about anything (not even about whether I'm a realist.) Maybe I ought to think about it more (or less.) I think that many readers won't get all this subtext so this seems like a perfect place to explain what is actually happening. A statement like "P is true but unprovable" sounds absurd, or worse, profound, to the uninitiated, and perhaps that's part of what fuels those popularizers you keep (justly) complaining about. You can use this as an opportunity to explain to the reader that the Goedel sentence of a consistent theory is true for the model N, and is false for some other model) and that's how we know it's neither provable nor disprovable within the theory, and also by the way mathematicians may say something is "true" when they really mean that it is provable in the standard model. That's typically the right way to go on all these kinds of issues. More details leads to less philosophy. --Sammy1339 (talk) 23:24, 26 May 2015 (UTC)

Well, some of your details are not quite right :-).

First, that isn't how we know it's neither provable or disprovable within the theory; having proved that it's neither provable nor disprovable in the theory, we then conclude (using Gödel's completeness theorem) that there are models that satisfy it and models that falsify it.

Second, mathematicians don't use "true" to mean "provable in the standard model". They use it (for arithmetic statements, anyway) to mean "true in the standard model", which is different. (In fact, it's precisely the Gödel results that show it has to be different.)

The problem with saying "true in the standard model" is that it makes it sound complicated, whereas it's really very simple. The reader has to ask "what's the standard model?". Oh, well, first you need to know what a model is. That's not deep, but it's a fair amount of structure to absorb. Then you need to find out that the "standard model" is actually just the one you had in mind all along (you know, zero, one, two, three, etc), but explained with all this superstructure around it.

Then you need to parse out that a statement of arithmetic is "true in the standard model" just in case...now you do the whole Tarski thing inductively on the statement, and the way the "standard model" comes in is that you let the variables range over zero, one, two, etc, and interpret plus and times to mean ordinary addition and multiplication, and it all boils down to an arithmetic statement is "true in the standard model" just in case it's ... true.

These are the kinds of things that can be dealt with in asides; explanatory footnotes (as opposed to references) are especially good for this. I think that would be a good solution here. But there shouldn't be any weaseling about whether the statement is true. --Trovatore (talk) 23:56, 26 May 2015 (UTC)

If I'm reading this article these are the main things I want to know, not asides and footnotes. You can generally make math articles look nice by glossing over a lot of fine points, and you may feel like this makes things simpler but actually, to someone unfamiliar with the subject, it ends up being completely opaque. Particularly since this statement involves a specific notion of "true" which may be in common use among mathematicians but is not commonly understood by the article's target audience (e.g. ignorant people like me), that should be explained. --Sammy1339 (talk) 02:24, 27 May 2015 (UTC)

I would argue that this is exactly the intuitive, natural-language meaning of "true", and should not be a surprise to the naive reader (except insofar as that reader expects all truths to be provable, but that's a surprise as to what happens, not as to what things mean).

Example: What does you mean when you say that every natural number is the sum of four squares? Do you mean that there's a formal derivation of the string $\forall x\exists y\exists z\exists w\exists v(x=y*y+z*z+w*w+v*v)$, obtainable by starting with axioms of Peano arithmetic and Hilbert logical axioms and applying modus ponens?

I don't know you, but I'm going to boldly assert that no, that's not what you mean at all. What you mean is that if you take any natural number, say 4 or 17 or Graham's number or whatever it be, there really are four natural numbers whose squares sum to that number.

Well, that's exactly what "true" means in this context. --Trovatore (talk) 03:24, 27 May 2015 (UTC)

My intuitive notion of mathematical "truth" is more like the first thing you said, but I can imagine someone thinking along the lines of your second option. I'm not sure that everyone does, because they would then all say that the Riemann Hypothesis is true because if you apply Riemann's zeta function to any number off the critical line and not a negative even integer, the result is nonzero. (Try it!) Unless what you really mean is that you would get a nonzero result for every number if you actually tried it for every number - that becomes a very unintuitive counterfactual and I'm not sure it's even meaningful. But let's say you accept this. Obviously you can't test it directly, so you then say, okay, it might be true, but since we can't try every case, we can only assert it's true if there's a proof. So you say a statement is true exactly when there is a proof that it is true, which comports with my original intuition that those are the same thing. Anyway, instead of presupposing that naive readers will think your way or mine, it's best to explain the details of what you really mean. --Sammy1339 (talk) 03:50, 27 May 2015 (UTC)

Actually, that's precisely what I mean when I say that. I do not think there is something fundamentally special about the natural numbers and that when I speak of arithmetic I am speaking with those in mind, or that statements that are true in that particular model are somehow closer to being "true" in the natural language sense than statements that are true in any other model. And I'm going to similarly "boldly assert" that I'm not the only person who thinks this way, and that it is bad for this encyclopedia to assume that everyone does. The wording that I suggested is non-contentious regardless of whether or not you think that the natural language meaning of "truth" somehow lands closer to one model than to another - it is best to assume as little as possible, and leave interpretations to the individual. 96.231.153.5 (talk) 04:05, 27 May 2015 (UTC)

To both of you: I'm sorry, but I don't believe you. I don't think that's what you mean at all. I think that's a story you tell yourself to avoid coming to terms with questions involved with real existence of abstract objects. But it's not a natural reading. --Trovatore (talk) 04:18, 27 May 2015 (UTC)

Well I believe that you don't believe me, and would never accuse you of deceiving yourself out of unwillingness to come to terms with the fact that some people don't believe in abstract objects. --Sammy1339 (talk) 04:28, 27 May 2015 (UTC)

It seems to me that a baseline has to be drawn somewhere in set theory and mathematical logic, and that none of these theories can be formalized without the other. Trovatore's POV seems to reflect a fairly high base line ( or high set bar for those of you into high-jumping) , while User talk:128.8.140.59's base line is lower (anything consistent goes?). It comes then down to what the literature says. YohanN7 (talk) 19:05, 26 May 2015 (UTC)

This discussion above begins: "The Goedel sentence of a consistent theory is true. That is what reliable sources say," and assuming that is what reliable sources say, that's where it should end. Paul August ☎ 23:48, 26 May 2015 (UTC)

And why the Fk are the posts ITT intersected so that my early reply appears to be the last one? Just delete it if you aren't interested in other peoples opinion, YohanN7 (talk) 23:54, 26 May 2015 (UTC)

The indentations indicate who is responding to whom. I wouldn't take it that no one is interested in your comment. Just no one has responded to it (as yet, anyway). --Trovatore (talk) 01:10, 27 May 2015 (UTC)

You are right. Both about indentations and about the disputed matter. YohanN7 (talk) 10:38, 27 May 2015 (UTC)

See also True but unprovable on math.stackexchange. Boris Tsirelson (talk) 09:29, 27 May 2015 (UTC)

I think, the meaning of "true but unprovable" is easier to realize on the well-know example of a Turing machine that seeks a proof (in a given formal system) that it (this machine) will never stop and, if found, it stops. If the formal system proves only true statements, then clearly, the machine will never find the proof of the TRUE statement that it will never stop! See also Halting problem#Relationship with Gödel's incompleteness theorems, and Quine (computing). Boris Tsirelson (talk) 09:40, 27 May 2015 (UTC)

(Nice example above.) Even if the suggested (and multiply reverted) formulation was to be taken in, then we would not be talking about Gödel's theorem, but some other (slightly more general) theorem. I'm quite sure Gödel did not have any goofy, yet consistent, theory in mind when he did his original work. YohanN7 (talk) 12:36, 27 May 2015 (UTC)

As for me, it is a pity that the "nice example above" is scantily explained in Wikipedia. A special article about "True but unprovable" would help against misunderstandings with models, axioms, truth etc. (Likewise, I volunteered Equivalent definitions of mathematical structures against misunderstandings with affine spaces etc.) I tried once something alike: "A theory as a crystal ball?" on CZ. Boris Tsirelson (talk) 13:28, 27 May 2015 (UTC)

I'm all for an article called "true but unprovable" provided there are a few sources for it. However if you read the discussion between myself and Trovatore above it ought to be clear why this is a POV phrasing and should not appear in the article without qualification. --Sammy1339 (talk) 13:46, 27 May 2015 (UTC)

I am not an expert in logic, but my feeling is that the POV you mention is in fact the mainstream. The "true but unprovable" statement about the machine is in fact proved in a meta-theory (of the given theory). Due to Goedel we know that a theory cannot be its own meta-theory. A nonstandard model of arithmetic could be of some interest. But a nonstandard model of meta-arithmetic is an exotic idea. Saying "if the machine stops at a time t" I do not mean that t may be a kind of hyper-integer. Do you? Boris Tsirelson (talk) 14:10, 27 May 2015 (UTC)

(EC with Tsirel) Not all POV's are equal. This is not intended as rudeness, but merely stating that minority POV's need not be mentioned (or the majority POV be "explained") if the minority POV is fringe. It is the other way around. The minority POV needs substantial qualification and reference. YohanN7 (talk) 14:15, 27 May 2015 (UTC)

This is not political. Common sense says we should try to make the article intelligible to readers who may misunderstand the statement if they are formalists. (And formalism is not a "fringe" position, by the way - I'm not sure what the predominant view of mathematicians is, but I don't think it's platonism.) --Sammy1339 (talk) 14:47, 27 May 2015 (UTC)

Sorry, no, it has little to do with what most mathematicians "are". It has to do with Gödel's theorem and maybe about what Gödel "were" (Platonist, Realist, Formalist, ...). (He wasn't a goof-bag.) YohanN7 (talk) 15:16, 27 May 2015 (UTC)

(edit conflict) Well, if you really want to get into that way of thinking it might have to do with the published positions about the philosophy of mathematics, which are many and various. I don't see why Goedel's view should be given special weight - mathematical theorems belong to everybody, and Tarski wasn't a goof-bag either. But really we should just include all the details so that this isn't even an issue and everybody can understand it regardless of their philosophical dispositions. --Sammy1339 (talk) 15:41, 27 May 2015 (UTC)

Interestingly, Gödel also investigated closed time-like curves in models of space-time. I guess he was thinking about (at least) two ways to know the future: predict it by math, or observe it, if it is also the past. Boris Tsirelson (talk) 15:39, 27 May 2015 (UTC)

Time-like closed curves go beyond my imagination. Our article on the continuum hypothesis states that Gödel thought CH to be wrong. This is not typical of a formalist, but rather of a Platonist? Believing the CH wrong (or right) and at the same time accepting competing theories for the natural numbers isn't very consistent. I don't think he did that. YohanN7 (talk) 15:52, 27 May 2015 (UTC)

I missed this (simultaneous editing going on: I don't see why Goedel's view should be given special weight... His theorem should give him 100% weight because it is his theorem. "Generalized" statements, using different premises, about it should not refer to it as Gödel's theorem, but rather a generalized version. For this, you absolutely certainly need sources. YohanN7 (talk) 16:04, 27 May 2015 (UTC)

But I think you are missing the point that Goedel's original work is not the only reliable source on the incompleteness theorems. --Sammy1339 (talk) 16:13, 27 May 2015 (UTC)

A lot of people have trouble understanding how a statement can be true but unprovable. A simple example, though NOT a Gödel sentence, is "This statement is unprovable." If it were false, it would state that it is provable. But false statements are never provable. Therefore it is true. Rick Norwood (talk) 15:44, 27 May 2015 (UTC)

A lot of people have trouble understanding how a statement can be true but not true. A simple example, though NOT a Gödel sentence, is "This statement is not true." If it were false, it would state that it is true. But false statements are never true. Therefore it is true, and thus not true. --Sammy1339 (talk) 16:05, 27 May 2015 (UTC)

There is a difference between statements in ordinary language and in mathematical logic. (English is decidedly not consistent. interesting, but not helpful here) YohanN7 (talk) 16:13, 27 May 2015 (UTC)

Well, for a formalist, every theorem is a theorem of a given formal theory, right? Gödel theorem (say, for arithmetic) is a theorem of meta-arithmetic, right? Thus, it is unspecified until you specify not only the formal arithmetic used, but also the formal meta-arithmetic used. Thus, our articles are anyway far not specific for a formalist, right? Boris Tsirelson (talk) 16:36, 27 May 2015 (UTC)

I'm not sure exactly what you're saying, but I'm of the view that this article is indeed far too vague and should specify everything insofar as possible. I think it ought to be expanded a lot with a lot of explicit details, especially by making clear exactly what formal systems we are talking about. I have no objection to using language like "true but not provable," but only provided it is made abundantly clear what this means, because it will otherwise sound like gibberish to people like me and the IP user who commented above. --Sammy1339 (talk) 16:47, 27 May 2015 (UTC)

Footnotes look like a solution. It is also proposed above. Many readers will head off faced with a formal definition of "true but not provable within the theory" in an early section. I dare say also that the mathematical formalist will not be confused at all, since it is extremely unlikely that this is a situation when he faces a statement with a supposedly default meaning for the first time as a professional formalist. YohanN7 (talk) 17:15, 27 May 2015 (UTC)

No, I disagree. I think these are central issues to the topic and need to be addressed in the main text. There is not some unspoken universal understanding that everyone has of all this terminology. And I can't speak for all formalists, but I was confused by the way these statements were written - I knew there must be some underlying platonist assumptions going on, but it wasn't clear to me what they were because I don't think that way. --Sammy1339 (talk) 17:26, 27 May 2015 (UTC)

Agreed, I don't find that "true in the natural numbers" matches my intuition for the natural language word "true" at all (and thus reading "the Goedel sentence is true" seems to me a terrible stretch of the word "true"), regardless of whether Goedel intended his theorem to talk about that specific model. As a formalist, it's rather bizarre to hear it claimed that sentences in a formal language are "about" anything, in particular - they're just strings. Nothing in modern math requires that they be descriptive. 128.8.140.59 (talk) 18:31, 27 May 2015 (UTC)

Wow! Then, I have nothing to say you. We are "mutually bizarre". Boris Tsirelson (talk) 18:56, 27 May 2015 (UTC)

(Edit conflict) I am afraid, this is impossible. About 50 years ago :-) I've read a book with full theory, hundreds of large pages... well, with proofs; but formulations could not be stated in less than 40 pages or so... definitely non-encyclopedic. You'll hear "try Wikibooks or Wikiversity".

Either you specify a formal theory able to be meta-arithmetic (it could be ZF-like but with only finite sets), or you use arithmetic itself, via the Gödel encoding (of statements and proofs by natural numbers). It looks like a computer code of 40 pages.

This is the burden of being a formalist. A human explains to a human programmer in 15 min what is needed; and then the programmer explains the same to a computer during 3 months (now, when programming languages are very powerful; in 20 century it was 12 months). Why? Since the computer is a formalist, while humans are not. (By the way, did you ever try a "proof assistant" software? I did.) Boris Tsirelson (talk) 17:28, 27 May 2015 (UTC)

Yeah, I get that, but we can still do better. See group (mathematics) for an example of an article that gives a brief treatment of its topic without omitting the definitions or relying on unclear, ambiguous intuitions. --Sammy1339 (talk) 17:40, 27 May 2015 (UTC)

OK, I take your challenge about "groups". Let us imagine such discussion on the talk page there:

Formalist A: The article assumes implicitly that groups exist. But no; what really exists, is proofs of theorems within the group theory. Thus, we must specify "group theory". Like First-order logic#Ordered abelian groups.

Formalist B: Yes. And do not forget to define formulas and list not just special axioms, but also logical axioms, formation rules, and rules of inference.

Formalist C: Do you mean natural deduction? That is your POV. As for me, I prefer sequent calculus.

Formalist D: Do not bother; these two are well-known to be equivalent. You'd better think, whether you mean classical or intuitionistic logic. And, why just first-order logic? Higher-order logic can be used, too.

Naive reader: What the hell is happening here? I needs facts about groups. Can I know them without learning all these logics? Could these persons, with their exotic orientations, form a separate club, please?

Conclusion: Being a formalist, face the consequences yourself, and do not make troubles to innocents.

Boris Tsirelson (talk) 06:37, 28 May 2015 (UTC)

One can assume a certain standard foundation for unqualified statements without believing that that choice of foundation is somehow more "privileged" or "fundamental" than another. Moreover, there is a stark difference between agreeing that unqualified statements about mathematical objects share some default foundational assumptions than agreeing that formal sentences have some natural-language interpretations that justify privileging some models over other models (the designation of a "standard model" is not a foundational choice about mathematics - we begin with axioms, not models). It is one thing to say "A group is a mathematical structure obeying these properties" without further qualification, and quite another to say "this sentence in the language of groups is 'true'" because you happen to think that some model of the group axioms is more special or "real" than another. The issue being taken here is not one of disputing foundations, it is disputing the use of one's own natural-language interpretation of a formal sentence to provide a distinctly non-mathematical interpretation of something which does not necessarily have any intrinsic meaning.

This is akin to claiming "the parallel line postulate is 'true'" with the justification that "the parallel line postulate is intended to talk about plane geometry." I find it intensely confusing, and I doubt I am the only one. 96.231.153.5 (talk) 15:13, 28 May 2015 (UTC)

I see. And in the case of the parallel line postulate I agree that it should not be treated as true for the physical space. But on the other hand, "God made the integers; all else is the work of man." Axioms for the (pre-existent!) integers are chosen by us mortals; no wonder that they are not so good as we hoped. This is why I doubt that "we begin with axioms, not models". Moreover, now we know that the Euclidean space applies to diverse problems, not only as an approximation to the physical space; taken this way, it gets a status closer to that of natural numbers. Boris Tsirelson (talk) 15:41, 28 May 2015 (UTC)

My opinion, and that of many published reliable sources, is that there is no God and there are no integers. Per WP:IMPARTIAL, Wikipedia's voice should not be used to take a position on this.

More importantly though, I think you misunderstand what I am asking for. I don't want to hash out the whole realist v. formalist debate on every math page; rather, I just want explicit definitions made available so that it becomes a non-issue. In the article group (mathematics) they don't go and discuss ontological questions, but they do give an axiomatic definition of a group that everyone agrees with, instead of just saying, for example, "groups describe symmetry." In this article, we should have a precise definition of concepts like languages and models, and the axioms of arithmetic and set theory that we are talking about. We can do all that without debating whether some objects are "real." --Sammy1339 (talk) 16:29, 28 May 2015 (UTC)

(1) Do not take this occurrence of "God" literally. (2) No, we cannot do all that (nor even a large part of all that) just because "precise definition of concepts like languages and models, and the axioms of arithmetic and set theory that we are talking about" is much, much longer than "axiomatic definition of a group that everyone agrees with". Boris Tsirelson (talk) 16:38, 28 May 2015 (UTC)

Natural languages are imperfect ways to communicate our ideas. Also formal languages are imperfect ways to communicate our ideas.

Do not think that I am a 100% platonist. I know that my idea of integers is imperfect (and no wonder; I am just a mortal). But I also know that my idea of integers is much more specific than expressed by the well-known formal languages. I definitely prefer models that make "Consis T" true (where T runs over the well-known formalizations of arithmetics). I definitely prefer models that embed into models of ZFC; even better, of ZFC with some large cardinals. In this sense I am much more platonist than a 100% formalist.

In this framework it becomes true that Goedel's statement is unprovable (in T) but true (provable in some T1 that is "better" than T in the sense vaguely expressed above).

Boris Tsirelson (talk) 16:33, 28 May 2015 (UTC)

It is standard in mathematics to state results "realistically" even if you are not a realist. Saves a lot of time, for one thing. Perhaps more importantly in this case, you don't want to conflate an assertion itself with the provability of that assertion, even if you're a formalist.

In this case, saying "the Gödel sentence of a consistent theory is true" is just the natural-language way of expressing the claim Con(T)→G_T, for a particular theory T satisfying the hypotheses. Just taking the troublesome part by itself, "G_T is true" says nothing other than G_T itself. That is, if you expand G_T out into what it says, "for every natural number blah blah blah", then "G_T is true" just means "for every natural number blah blah blah", and the "true" part is redundant (see redundancy theory of truth).

We use this language in mathematics articles all over the place. There's nothing essentially diffrerent here. We should follow the same convention. --Trovatore (talk) 16:43, 28 May 2015 (UTC)

Oh, and in case it's not obvious, I forgot to add: The conclusion Con(T)→G_T is not controversial; formalists can be comforted that it's formally provable in even a very weak theory (say Robinson arithmetic). --Trovatore (talk) 16:45, 28 May 2015 (UTC)

I would dispute that standard statements in mathematics are "realistic", but more importantly there is a significant distinction here, which is that the statement we are arguing about can cause confusion. All cases of "true but unprovable" amount to "provable with a certain set of rules, unprovable with a certain smaller set of rules." We can say that instead of just letting people wonder what "true but unprovable" means. --Sammy1339 (talk) 16:50, 28 May 2015 (UTC)

No, that's trivial — anything can be proved by allowing more axioms, if the axioms are not in any way constrained. The important point to get across here is that, if T is consistent, then the relationships among the natural numbers expressed by G_T must in fact hold. If they did not, there would be a witness, and that witness would code a proof that could be turned into a proof of a contradiction in T. --Trovatore (talk) 16:59, 28 May 2015 (UTC)

Restricting from "arithmetic" to "the natural numbers" (a specific model) is what I meant by going to a larger set of rules. And obviously this has caused confusion. --Sammy1339 (talk) 17:04, 28 May 2015 (UTC)

OK, I'm sorry, I find this weird; it's hard for me to buy that you're making this argument seriously. The natural numbers have been understood at least since Pythagoras (they left out 0 and maybe even 1 but that's a trivial difference); the axiomatizations are maybe 150 years old. It should be obvious that, at least in this case, the axiomatization has a specific intended interpretation, namely the naturals with ordinary addition and multiplication.

The case of groups, by the way, is a bad analogy. In group theory, we study groups, not group elements. The "axioms" of elementary group theory are axioms in a different sense — they're really part of the definition of group, which is the object of study. Arithmetic, on the other hand, does not study models of arithmetic (an interesting topic in its own right, to be sure, but a different one); it studies numbers. --Trovatore (talk) 17:16, 28 May 2015 (UTC)

I'd like you to stop doubting so much and instead accept as empirical fact that not everybody will be on the same page there. I'm not even asking you to abandon language like "true but unprovable," just to say what it means. --Sammy1339 (talk) 23:01, 28 May 2015 (UTC)

Well. Rick's new language says "in the natural numbers", which you seem to have indicated would satisfy you, so hopefully we can move on. Actually even from my perspective I suppose it's useful to point out that it's in the natural numbers, to avoid confusion with the objects of discourse of T, which could be something else. --Trovatore (talk) 23:36, 28 May 2015 (UTC)

Yes, the current wording seems to me perfectly satisfactory, so I think the current discussion has run it's course - we don't need to generate absolute agreement on the nature of mathematical truth here, only arrive at an acceptable wording for the article. 96.231.153.5 (talk) 01:17, 29 May 2015 (UTC)

"we don't need to generate absolute agreement on the nature of mathematical truth here, only arrive at an acceptable wording for the article." Give this person a medal. --JBL (talk) 01:44, 29 May 2015 (UTC)

How is epistemic/temporal/linear/lax/modal logic connected to mathematical logic?

Can someone explain how this new table in the "Formal logical systems" section is connected to mathematical logic?

Logical Judgement	Branch of Logic	Computation phenomenon
K knows A	Epistemic Logic	Distributed Computing
A is true at time t	Temporal Logic	Reactive Programming (partial evaluation)
A is a resource	Linear Logic	Concurrent Computation
A is possible	Lax Logic	Generic effects (monads, state, exception)
A is valid	Modal Logic	Runtime code generation

If this table really does belong here, it's going to need some sort of explanation. A search for "Lax logic" in wikipedia doesn't find much.
--Alan U. Kennington (talk) 13:01, 1 January 2016 (UTC)

It doesn't have a citation and is far too much without a citation so it should just be removed. Dmcq (talk) 13:55, 1 January 2016 (UTC)

Yes, that's what I think too. But I'm not a top expert on this stuff. People who know more than me might know how this kind of thing fits in. So I'm reluctant to delete other people's contributions. I prefer to leave that to people who fully understand this topic area. But in the 45 books on mathematical logic on my personal bookshelf, there's some peripheral mention of modal logic, but nothing about the other four kinds of logic, and there's nothing about runtime code generation either. Maybe this table is related to some kinds of computer software packages for symbolic logic. Either way, it either needs a really good explanation (and citations), or it needs to be removed. If it's about computer logic software, maybe there's another article where this table will make sense. Mathematical logic is already difficult enough to understand without interpolating (at best) peripherally related material into it.
--Alan U. Kennington (talk) 14:32, 1 January 2016 (UTC)

Well they are all valid forms of mathematical logic, but the article overall has far too few references. It really is a bit of a mess that way. I think I'll add some tags on sections which have no citations at all. Dmcq (talk) 14:41, 1 January 2016 (UTC)

I got bold and deleted the table. If someone wants to defend it, let him. Boris Tsirelson (talk) 14:58, 1 January 2016 (UTC)

The table is from (Frank Pfenning - Proof Theory Foundations, Lecture 1, Oregon Programming Languages Summer School 2012, University of Oregon) BostX (talk) 20:04, 6 January 2016 (UTC)

Oh, really? Well, but maybe its place is in another article - about Proof theory, from the viewpoint of computer science rather than math? Boris Tsirelson (talk) 20:12, 6 January 2016 (UTC)

References

Was first-order logic really designed to avoid Russell's Paradox?

This currently appears in the section First-order logic.

First-order logic is a kind of formal system of logic designed to avoid Russell's Paradox.

This doesn't sound right to me at all. I've never read this anywhere, and the name "Russell" does not appear in the First-order logic article. As far as I know, Russell's paradox is a set theory issue, not a first-order language (predicate calculus) logic issue. The paradox is resolved in ZF by the regularity axiom, and it is resolved in NBG by distinguishing sets from classes.

The idea that preventing self-referential propositions in first-order logic prevents Russell's paradox also seems wrong. You can very easily make minor changes to ZF and NBG axioms to permit Russell's paradox to occur. So I don't see that FOL has any power to stop the paradox at all.

Conclusion: Either someone's got to back up the assertion with a reference, or it has to be corrected.
--Alan U. Kennington (talk) 17:22, 1 January 2016 (UTC)

I see, this phrase was added on May 28, 2015 by User:Rick Norwood. Maybe, try to contact him. Boris Tsirelson (talk) 18:04, 1 January 2016 (UTC)

I reverted the entire section to a previous version. — Carl (CBM · talk) 03:26, 2 January 2016 (UTC)

Excellent! You removed some other dubious material as well.

--Alan U. Kennington (talk) 03:31, 2 January 2016 (UTC)

I agree. Thank you for getting in touch with me, and thank you for the correction. Rick Norwood (talk) 12:51, 2 January 2016 (UTC)

Lack of current references for the history and current state of the subject.

Although there are many inline citations in this article to classic historical papers, there are very few references which justify the picture which is painted in this article of both the history and current state of the subject. Many of the paragraphs seem quite dubious to me, just one particular view of the subject and one view of history, and some assertions seem to be false. Just adding citations of classic papers from a hundred years ago does not justify at all the picture which is painted of the scope of the whole subject and its history, nor of the particular assertions which are made. What is needed is more references to particular pages of particular reasonably recent books which cover this subject, especially for assertions which are dubious, controversial or tendentious. I definitely have the impression that this article is inadequately justified.
--Alan U. Kennington (talk) 03:03, 2 January 2016 (UTC)

It would help if you could identify, on this talk page, some claims that seem false or tendentious to you. — Carl (CBM · talk) 03:16, 2 January 2016 (UTC)

See for example the previous section of this talk page: Talk:Mathematical logic#Was first-order logic really designed to avoid Russell's Paradox? I prefer not to make a long list because I don't want to get into prolonged discussions. Life is too short of unproductive adversarial arguments. (Editors on wikipedia typically defend their opinions to the death, especially if they are wrong.) One merely has to read through the article to see that most of the material is a kind of essay which mostly refers to classic papers, not so much to references which support the assertions which are made about history and the current subject.
--Alan U. Kennington (talk) 03:22, 2 January 2016 (UTC)

I think the previous section of the talk page was very apropos, and I have reverted that section of the article to a previous version, which is at least somewhat better. I agree with what you say about long lists, so why not simply mention the main two issues you see? I will attempt to improve them within the month. — Carl (CBM · talk) 03:30, 2 January 2016 (UTC)

Good idea. I'll review the page and make a short list of comments over the next few days. I know enough to say that something is dubious, or even wrong. But I am not a specialist in this area. So I prefer to let others do the fixing, as you have done. Hopefully other people will contribute their lists of dubious passages too!
--Alan U. Kennington (talk) 03:34, 2 January 2016 (UTC)

Assessment comment

The comment(s) below were originally left at Talk:Mathematical logic/Comments, and are posted here for posterity. Following several discussions in past years, these subpages are now deprecated. The comments may be irrelevant or outdated; if so, please feel free to remove this section.

Better overview of logic besides first order logic, more thorough history, the technical reference should be split out. CMummert - 5 Oct 2006

Last edited at 20:43, 16 April 2007 (UTC). Substituted at 20:05, 1 May 2016 (UTC)

Help with term: distinction on Wikidata

I made an initial effort to provide a description and properties of the Wikidata item distinction (Q77227534), but I would appreciate someone with more expertise reviewing this. My initial description is based entirely on the Russian Wikipedia article: "a figure of speech through which the act of cognition is designated, reflecting the objective difference between real objects and elements of consciousness; In formal logic, one of the logical devices that can be used instead of defining". Daask (talk) 20:28, 13 November 2020 (UTC)

formal logic (Q1003009) could also use review. Daask (talk) 20:31, 13 November 2020 (UTC)

Opening sentence

I have read this 10 times over and it still doesn't make sense to me. "Mathematical logic, also called formal logic, is a subfield of mathematics exploring the applications of formal logic to mathematics." This seems like an unnecessary circular definition. I haven't looked at the revision history so I apologise in advance if there is some insight to be found there. Psycho 79 (talk) 23:52, 25 August 2021 (UTC)

I think you're right. Part of the solution is to remove "also called formal logic", which in addition to making the sentence circular, is also wrong. Mathematical logic is the discipline comprising computability theory, proof theory, model theory, and set theory (and I would tend to argue for category theory and perhaps universal algebra, but these are less commonly listed). None of these fields are "called formal logic".

Exactly what these fields have in common is a little hard to put your finger on, but I'm not sure that "applying formal logic to mathematics" is really it. In lots of cases it's actually the reverse, applying mathematics to formal logic.

I think a complete rewrite of the sentence is indicated. We should try to be clear that the boundaries are fuzzy, and avoid trying to capture the essence of mathematical logic by some phrase that sounds more precise than the concept actually is. --Trovatore (talk) 00:23, 26 August 2021 (UTC)

You could have a look at the text over here, both as something to borrow from and perhaps to improve as well! Botterweg14 (talk) 16:11, 27 August 2021 (UTC)

I've gone ahead and rewritten it, using text from the other article. But I'm not at all attached to the new version, so please rewrite it again if you see room for improvement! Botterweg14 (talk) 16:30, 27 August 2021 (UTC)

Hover over Mathematical Logic

When I hover over the Mathematical Logic link to this page from https://en.wikipedia.org/wiki/Peano_axioms (First link in the article), It comes up with disgusting unrelated image attached to the article. Please fix it! I don't know how to sorry. It appears it was griefed or the image was misplaced. Bumv (talk) 11:00, 29 March 2023 (UTC)