22
$\begingroup$

Second order logic is a language, but, is it a logic?

My understanding is that a logic (or "logical system") is an ordered pair; it is a formal system together with a semantics. However, the language of second-order logic is associated with a variety of inequivalent formal systems and a variety of semantics. So, is it a logic?

I think not. Supposing not, what do sentences like the following (copied from wikipedia) even mean?

Second-order logic, for example, does not have a completeness theorem for its standard semantics (but does have the completeness property for Henkin semantics).

$\endgroup$
  • 1
    $\begingroup$ "The Road to Modern Logic-An Interpretation" has discussion on why certain topics related to "foundations" are considered part of logic while others are not. It argues that this has mostly historical reasons and cannot be justified a priory. With regards to the other part of the question, I think one should start by considering what one wants to do with monadic second-order logic, before deciding about the status of higher-order logic. $\endgroup$ – Thomas Klimpel May 14 '13 at 0:07
  • $\begingroup$ If I find time, I will try to write an answer arguing in favor of "trying to turn" monadic second-order logic into a "true" logic. $\endgroup$ – Thomas Klimpel May 14 '13 at 0:21
  • $\begingroup$ @ThomasKlimpel, thank you that sounds like exactly the issue I'm interested in. $\endgroup$ – goblin May 14 '13 at 0:23
24
$\begingroup$

This is a very interesting philosophical question! There are philosophers on both sides of the issue. A prominent figure who spoke against SOL as logic was W.V.O. Quine. His argument mostly focuses on the point that SOL, which quantifies over sets explicitly, seems to just be "set theory in disguise", and hence not logic proper (see his Philosophy of Logic for more details). People have also put forth the argument you presented, viz. any putative logic must have a sound and complete deduction system in order to be a genuine logic, and since SOL doesn't have one, it follows that it can't be a logic.

On the other side, a prominent defender of SOL as logic proper is George Boolos. See his "On Second-Order Logic" and his "To Be is to Be the Value of a Variable (Or to Be Some Values of Some Variables)". One argument put forward in favor of SOL from a practical standpoint is that it has a way of really shortening proofs (see "A Curious Inference"). Boolos also suggests that we could use monadic SOL to model talk of plurals, i.e. to model sentences like "Some critics only admire one another". Another great defender of SOL is Stewart Shapiro, whose book Foundations Without Foundationalism not only presents a wonderful technical treatment of SOL but also some good philosophical defenses of it. In particular, Shapiro argues that SOL is needed for everyday mathematical discourse. I would highly recommend this book as an introduction to the subject, both mathematically and philosophically.

The status of completeness theorems in this debate is fascinating, but difficult to pin down. After all, many philosophers might just say "Look, so what if SOL is incomplete? That just means that the set of validities doesn't coincide with the set of provable sentences, i.e. there are some sentences which are logically true, but not provable. And while this is unfortunate, why shouldn't we expect this? Why shouldn't we just accept that logic didn't turn out the way we hoped?" On the other hand, many philosophers might say "Look, logic is about making inferences. If there are truths which don't come from some deduction or inference, then how could they be truths of logic?"

I personally don't find the view that genuine logics must have complete proof systems convincing (or at least convincing enough), but I certainly do feel the pull to search for/work with logics with complete proof systems. Ultimately, it comes down to what you think "logic" and "logical consequence" are, which are highly contentious matters in the philosophical literature, and which have no widely accepted answers.

$\endgroup$
  • 2
    $\begingroup$ Terrific answer and I echo in particular the recommendation of Shapiro's wonderfully illuminating book. $\endgroup$ – Peter Smith May 14 '13 at 6:10
5
$\begingroup$

Second-order logic has a collection of deduction rules. From a collection of statements, we can apply the deduction rules to derive new statements. This is called "syntactic entailment", or more simply, "formal proof".

Standard semantics talks about set-theoretic interpretations with the property that power types are interpreted as power sets. e.g. if $X$ is the interpretation of the domain of objects, then $\mathcal{P}(X)$ (or equivalently, $\{T,F\}^X$) is the interpretation of the domain of unary predicates on objects.

Given a collection of statements, we can consider set-theoretic models of those statements; interpretations where those statements are true. Using the laws of ZFC, one can show that the interpretations of statements are also true in every model. This is called "semantic entailment".

The incompleteness theorem is that syntactic entailment and semantic entailment (with standard semantics) do not coincide for second-order logic. (They do coincide for first-order logic!)


Incidentally, first-order logic also has variations. e.g. on the syntactic side, one can generalize to "free logic" (which, in some settings is what people mean when they say "first-order logic"), and people often consider various restricted fragments of it such as "regular logic" or "algebraic theories". On the semantic side, we can consider interpretations in terms of sheaves or objects in categories rather than in sets.

$\endgroup$
  • $\begingroup$ Hurkyl you write: second-order logic has a collection of deduction rules. Where can I learn what these rules are? $\endgroup$ – goblin May 13 '13 at 23:31
  • $\begingroup$ @user: Sorry, I don't know any references on the topic. I've never actually had the desire to study classical higher-order logic, especially when geared towards standard semantics. $\endgroup$ – Hurkyl May 13 '13 at 23:39
  • $\begingroup$ @user18921 With respect to references for higher-order logic, I liked "The Seven Virtues of Simple Type Theory". It explains higher-order logic, its standard and Henkin semantics, its deduction rules and many more related questions. $\endgroup$ – Thomas Klimpel May 14 '13 at 0:11
  • 1
    $\begingroup$ @user18921 "Second-order logic has a collection of deduction rules": you will find a standard presentation in Shapiro's book (which should be available in any uni library). $\endgroup$ – Peter Smith May 14 '13 at 6:22
  • $\begingroup$ @PeterSmith, thank you. I've been meaning to read Shapiro for some time now. $\endgroup$ – goblin May 14 '13 at 6:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.