Talk:Second-order logic

From Wikipedia, the free encyclopedia

Contents 1 Kinds of second-order logic 2 second order logic and russell's paradox 3 second order logic and class theory 4 Reverse mathematics 5 terrible sentence 6 Semantics 7 Ambiguous sentence 8 changes needed to beginning part 9 A nice article ... but Holy Smokes! Not a single reference? 10 Finiteness and countability 11 Dumbed down intro? 12 Claims about monadic second order logic

[edit] Kinds of second-order logic

The article should record the widespread existence of logics called second-order, since Leon Henkin, which are not like the intractable theory described in the article:

• Henkin-style second order logic admits complete axiomatisation, and is usually axiomatised in a language with support for lambda-abstractions; this theory can be expressed in first-order logic;
• The intractable theory is what "set theory in sheep's clothing" that cannot be expressed in FOL.

I've no time to tackle this now, but hope to get around to it before too long. --- Charles Stewart 20:18, 22 July 2005 (UTC)

[edit] second order logic and russell's paradox

the article claims that restricting to first order logic was one of the ways they eliminated Russell's paradox. I am wondering if second order logics are more likely to contain Russell's paradox than a first order logic (which can also contain Russell's paradox). -Lethe | Talk 20:56, August 7, 2005 (UTC)

Russell's paradox applies to neither first-order nor second-order logic, indeed, both these logics are consistent. As stated in the article, it applies to Frege's system, which is a kind of "mixed-order" logic. Don't be confused by the fact that it also applies to variants of naive set theory, which can be formulated on top of, say, first-order logic; this is not a problem of the logic, but of the theory. -- EJ 12:04, 18 August 2005 (UTC)

[edit] second order logic and class theory

Another similar question: in the first order language of axiomatic set theory, one can view classes as abbreviations for first order statements about sets, in which case one may not quantify over

class variables. If one extends the language to allow quantification over classes, is that the same as moving to a second order language about sets? -Lethe | Talk 22:34, August 7, 2005 (UTC)

Yes (more or less), if you understand "language" in purely syntactic way, as the set of well-formed formulas. No, if you intend to give the second-order quantifiers also their second-order semantics. That means, Gödel-Bernays or Kelley-Morse set theory is a first-order theory, it does not obey the rules of second-order logic. -- EJ 12:19, 18 August 2005 (UTC)

Nonetheless, the term "second-order" is often used to apply to these sorts of theories, also second-order arithmetic (Z_2) is standard terminology, and the terms second-order and higher-order are regularly used in type theories to refer to first-order-describable logics, eg. Chuch's simple theory of types is often called higher-order logic, and is a little stronger than Z_2. The article really needs to take account of all this. --- Charles Stewart 19:57, 18 August 2005 (UTC)

Yes, this is an unfortunate bit of terminology which further adds to the confusion. Second-order arithmetic is a two-sorted first-order theory. It will be tricky to incorporate this in the article without confusing everybody. Technically, it does not even belong here, as the article is about second-order logic, which is not involved in these "second-order" theories. But I'm not sure whether having a separate article on, say, second-order theory or second-order language would be helpful. -- EJ 10:14, 19 August 2005 (UTC)

[edit] Reverse mathematics

I fail to understand how reverse mathematics could be relevant to the claim that second order logic is needed for topology etc. what ever that means exactly. After all, reverse mathematics is mostly concerned with fragments of second order arithmetic, which - unfortunately, perhaps - is a multisorted first order theory. Is there something I'm missing in the work of Simpson, Friedman or others that would justify the claim in the article? Aatu 21:45, 13 December 2005 (UTC)

The claims in that paragraph are very misleading: Simpson and the others use second-order arithmetic, which is a two sorted first-order theory with quantifiers over numbers and sets of numbers, and one could, with not much difficulty but at the price of some syntactic nuisance, recast it is a single-sorted first-order theory, using a relation singsub(X,Y) which is true iff X is a singleton subset of Y. It is not second-order logic in the sense that is debated here. I'll change the paragraph. --- Charles Stewart 16:33, 15 December 2005 (UTC)

[edit] terrible sentence

Hello, someone can understand the meaning of the first paragraph? I think two sentences are missing.

JPLR

[edit] Semantics

I think it would be nice to add a section describing the various semantics. Right now there is a hint about Henkin semantics, but it is very vague. I will write the section soon unless people object here. - CMummert 11:37, 26 April 2006 (UTC)

[edit] Ambiguous sentence

The article currently states the following: "But monadic second-order logic, restricted to one-place predicates, is not only complete and consistent but decidable--that is, a proof of every true theorem is not only possible but determinately accessible by a mechanical method."

As far as I understand it is only the quantification which is limited to one-place predicates in MSO. Otherwise, n-place predicates also occur in MSO (with n>1). Can someone please confirm before thinking of correcting this?

Thanks.

[edit] changes needed to beginning part

The first part of the article should be broken into a short intro paragraph and a new section on the definition. I think that the special semantics of second order logic need to be emphasized more. The following sentence is just not true:

That is, the following expression: ∃P P(x) is not a sentence of first-order logic.

What is true is (something like): the meaning of the sentence assigned by the semantics of second order logic is not expressible in first order logic. CMummert 15:25, 13 June 2006 (UTC)

[edit] A nice article ... but Holy Smokes! Not a single reference?

To all who have toiled in this soil:

This is a very nicely-written, smoothly flowing article, but ohmygod where are the references?!! Us lesser mortals need more (lower-level, "first-order" <== writ ironic) information.

wvbaileyWvbailey 21:45, 17 September 2006 (UTC)

I'm glad you think this article is clear, but I am planning significant changes. Some of these changes are indicated in higher comments of mine on this page. One part of the changes is to add references; I have been looking into which things are appropriate. Any suggestions would be welcome. CMummert 23:38, 17 September 2006 (UTC)

[edit] Finiteness and countability

I think that you should state that the codomain of a function considered is the same as the domain. Leocat 17 Sept 2006

[edit] Dumbed down intro?

I love to see detailed technical articles on wikipedia, but I can't make any sense of the first paragraph, even though I have a functional understanding of first-order logic. It would be nice if there were one or two more generalized and dumbed-down introduction sentences before launching into the highly technical explanation. --24.200.34.209 21:52, 27 October 2006 (UTC)

Thanks for the feedback. The entire article needs revision, but it has to wait until somebody actually does it. The collection of editors who know about the topic and have a lot of spare time is not so large. I have plans to do it sometime, but I am working on other articles right now. CMummert 22:51, 27 October 2006 (UTC)

[edit] Claims about monadic second order logic

I am moving the following from the article to here.

As George Boolos has pointed out, though, this incompleteness enters only with polyadic second-order logic: logic quantifying over n-place predicates, for n > 1. But monadic second-order logic, restricted to one-place predicates, is not only complete and consistent but decidable--that is, a proof of every true theorem is not only possible but determinately accessible by a mechanical method. In this respect, monadic second-order logic fares better than polyadic first-order logic: monadic second-order logic is complete, consistent and decidable, but polyadic first-order logic, though consistent and complete, is no longer decidable (See halting problem).

The monadic-second-order theory of arithmetic is the same as the full second-order theory, and is not decidable. Boolos probably made a correct claim which has been vaguely reprinted in the paragraph above. Until a reference is found, the claim should be kept off the main page. CMummert 23:55, 21 November 2006 (UTC)