Talk:Second-order logic

From Wikipedia, the free encyclopedia

Mathematics Portal

This article is within the scope of WikiProject Mathematics, which collaborates on articles related to mathematics.

Mathematics rating:

B+ Class

Mid Priority

Field: Foundations, logic, and set theory

Please update this rating as the article progresses, or if the rating is inaccurate. Click to show/hide comments.
Please add to or update the comments to suggest improvements to the article.
Geometry guy 22:50, 9 June 2007 (UTC)

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
13 On the "extensions" of second-order logic
14 re: Expressive power of second order logic
15 Power of the Existential Fragment
16 Explain formula idea

[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)

[edit] On the "extensions" of second-order logic

"In mathematical logic, second-order logic is an extension of first-order logic, ... Second-order logic is in turn extended by type theory." Hmm... so second-order logic is an extension of both first-order logic and type theory? first-order logic + type theory = second-order logic ? User:M K Lai 20 December 2006

Second order logic extends first order logic. Type theory extends second order logic (and thus second order logic is extended by type theory). You may be misreading the article. CMummert 02:11, 21 December 2006 (UTC)

The meaning of the term "extends' could be better explained. Second-order logics are actually less expressive than FOL and there is nothing in a SOL that can not be expressed in FOL. It is the constraints the SOL provides (both formal and through its representation) that provide the additional expressiveness. See the first chapter (I think, I don't have the book to hand) of John Sowa's book on Knowledge Representation. This allows one th think of FOL as defining a design space and the creation of SOLs as an exploration of that design space. The utility of this is the applicaiton of various search algorithms to exploration of the FOL space to devise new SOLs for various purposes. A SOL is restriction on FOL with a (more or less) expressive symbol system that makes it easier to think through specific problems - I am beigging to repeat myself. Steven Forth 12.151.151.3 18:59, 21 February 2007 (UTC)

Can you explain in more detail what you mean by "nothing in a SOL that can not be expressed in FOL"? The article explains how various statements, such as the "the universe is countable" or "the continuum hypothesis holds", can be expressed in second-order logic with second-order semantics while they cannot be expressed with the same meaning under first order semantics. CMummert · talk 22:50, 21 February 2007 (UTC)

Language should be defined in terms of their model-theoretic properties, such as compactness (in many of its various forms), Lowenheim-Skolem properties, interpolation, etc. Given such definitions of languages, it is impossible to e.g. categorically express the natural numbers in a first-order language. While it is true that certain statements such as "the CH holds" are expressible in the language of first-order set theory under one sense of 'express', they are not under another sense; viz., the same sense as regards the categoricity of second-order arithmetic.

Likewise, if you take a first-order language and extend it with a model-theoretic quantifier "there are infinitely many", then you no longer have a first-order language, just because your variables range only over individuals. If you allow simultaneously quantification over infinitely many variables in a single formula, then again, you no longer have a first-order language, since the model-theory of this language exactly coincides with that of second-order languages. If you partially order first-order quantifiers, you no longer have a first-order language. The moral is that it doesn't matter what your variables range over, there is a precise definition of the order of the language specified in terms of (classes of) models and the properties holding between them. In this sense, it is quite clear that SOL extends FOL. Nortexoid 23:17, 21 February 2007 (UTC)

Was the last response intended for me or for S. Forth? In the ordinary contemporary usage of the term "language", it is a syntactic rather than semantic concept. Thus there is no difference between the language of second-order arithmetic using first-order semantics and the language of second-order arithmetic using second-order semantics, because the set of syntactically valid formulas is identical for each of these systems. Nevertheless the second order semantics cause the language to be more expressive. CMummert · talk 00:10, 22 February 2007 (UTC)

It was intended for S. Forth, but regarding your comment, I'm having trouble making sense of it. Do you mean by "FO semantics" "Henkin semantics", and by "SO semantics" "full or standard semantics"? If you check the literature, the vast majority of logicians do not consider languages that do not satisfy a class of model-theoretic properties first-order, even if they have all and only the same grammatical categories as first-order languages. In fact, it seems a rather crude way of categorizing languages according to e.g. whatever the variables range over (e.g. individuals rather than sets or classes). Also, what does "syntactically valid" formulas mean? Do you mean "deducible" ("provable) formulas, or do you mean "deducible formulas that are valid wrt to a certain semantics"? It's a mystery at this point.

There are various notions of "expressiveness". E.g., there is a sentence in the language of first-order set theory that "expresses" there are denumerably many P in the standard interpretation of set-theory, but it does not "express" there are denumerably many P in the sense that each of the members of its class of models is denumerable, because there are nonstandard models of first-order set theory. Hence, people say that no first-order language can express 'there are infinitely many P', a result of its having the (upward) Lowenheim-Skolem property. Nortexoid 01:05, 22 February 2007 (UTC)

When I said "syntactically valid formula" I meant the same things as a "well formed formula" - it is a finite sequence of symbols, built up out of atomic formulas using logical connectives and quantifiers. So $\forall x ( x = x)$ is syntactically valid and $x = \forall x ()$ is not. Yes, when I say "second order semantics" I mean full semantics and by first-order semantics I mean Henkin semantics; I thought that would be clear from context. The fact that the language for second-order logic can be used with two different semantics is a perennial cause of confusion. CMummert · talk 01:41, 22 February 2007 (UTC)

[edit] re: Expressive power of second order logic

Paragraph 3 states 'For example, if the domain is the set of all real numbers, one can assert in first-order logic the existence of an additive inverse of each real number by writing ∀x ∃y (x + y = 0) but one needs second-order logic to assert the least-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a supremum.'

The necessity of SOL asserted in paragraphs 3 might be clarified. This specific point has been addressed by Herbert Enderton here: http://sci.tech-archive.net/Archive/sci.logic/2004-10/0224.html —Preceding unsigned comment added by 66.81.75.254 (talk) 21:28, 27 April 2008 (UTC)

[edit] Power of the Existential Fragment

Was linking 'Monadic second-order logic' to the article on 'Monadic predicate calculus' which doesn't really discuss *second order* so much, but it does give one an intuition what 'monadic' would mean in the context of SOL; I narrowed the scope of what was linked to remove 'second-order' so that ppl going to the target article wouldn't expect to find SOL discussed there. Zero sharp 04:24, 14 October 2007 (UTC)

[edit] Explain formula idea

Next to complicated formula like this one:

$\forall A \Big[(\exists w (w \in A) \land \exists z\,\forall w ( w \in A \rightarrow w \leq z)) \rightarrow \exists x\,\forall y ([\forall w (w \in A \rightarrow w \leq y)] \leftrightarrow x \leq y)\Big].$

it would be good if there were an "Explain Formula" link that would show and hide a box like this:

This essentially says

$\forall A$	For all sets $A$
$\Big[$	[ If
$(\,$	(
$\exists w (w \in A)$	$A$ is non-empty
$\land$	and
$\exists z\,\forall w ( w \in A \rightarrow w \leq z)$	$A$ has an upper bound $z$
$)\,$	)
$\rightarrow$	then
$\exists x$	there exists an $x$ which is a least upper bound for $A$ because it satisfies:
$\forall y$	for all $y$
$($	(
$[\forall w (w \in A \rightarrow w \leq y)]$	If $y$ happens to be an upper bound of $A$
$\leftrightarrow$	then
$x \leq y$	x is less than or equal to y (and also the reverse implication is true)
$)\,$	)
$].$	].

What do you think of this idea? —Egriffin (talk) 16:22, 31 January 2008 (UTC)

The expectation is that the reader will do something like this to break apart the formula. If you think the formula is too long, it would be possible to split it up into pieces. But we generally avoid "popup" things in articles. If something is worth saying, it's worth saying all the time. — Carl (CBM · talk) 18:01, 31 January 2008 (UTC)

I'm against popups too, but agree tht the formula is quite daunting. I suggest a standard approach used in textbooks: break it down into pieces. So define blah to be upper bound of A, and so then if upper bound exists, then blah. (Do it in formulas, not words), although the if-then implication can be done in words. (professional logicians can read long sentences like this easily enough, and seem to prefer them; however, since this is an intro article, and not a proof, the one-big-long-formula style is inappropriate). linas (talk) 18:39, 31 January 2008 (UTC)

There is already a nice prose statement in the same paragraph; the point of displaying the formula is precisely to demonstrate that the words can be represented in the language of second-order logic. The formula itself could be broken into pieces, such as "Bounded(X)" to mean X has an upper bound, etc. — Carl (CBM · talk) 22:32, 31 January 2008 (UTC)

I was suggesting using something like Template:ShowHide or Template:Seemore (not really a popup in that there's no overlapping). Anyway I gather the use of these for article text is "not well liked". —Egriffin (talk) 13:00, 1 February 2008 (UTC)

I don't like the idea, it would only complicate the matters further. As Carl pointed out, the meaning of the formula is already explained in the prose around. If its complexity is a concern nevertheless, I think a better solution would be to use an example which allows for a simpler formula. For instance, switch from reals to natural numbers, and discuss the induction principle

$\forall A\,[0\in A\land\forall x\,(x\in A\to x+1\in A)\to\forall x\,x\in A],$

or something like that. Surely the lub property is not the only real-world example of a second-order formula there is. -- EJ (talk) 13:18, 1 February 2008 (UTC)