Second-order logic

Main points of the debate

• The key debate: is second-order logic logic? Boolos thinks it is; Quine calls it “set theory in sheep’s clothing”.
  • Arguments for:
    • SOL increases FOL’s expressive power in a way that lets us capture more “palpably logical” notions
    • SOL is a natural extension of FOL
  • Arguments against:
    • Ontological commitments
    • Incompleteness and other metatheoretic changes
• First, what makes something logic?
  • Topic-neutrality: logic says nothing about any particular subject matter; it applies universally
    • FOL satisfies this in that quantifiers range over an unspecified domain and predicate letters are schematic.
    • SOL arguably violates by committing to set-like entities (empty collection, universal collection).
    • But as Boolos notes, FOL itself is committed to non-emptiness of the ontology of discourse.
      • Note that Boolos concedes that there is a qualitative difference between the ontological commitments of FOL and SOL.
      • FOL’s commitment to non-emptiness of D is harmless since clearly there are things in the world.
      • But SOL’s quantification over properties/sets requires that the things in our domain form a set, which is more substantive.
      • “There is a striking difference between the commitment to non-emptiness and the commitment to sethood: we believe that our own ontology is non-empty, but not that it forms a set!”
  • Formal/structural character: logic is about the form of reasoning, not its content.
    • SOL’s expressive gains are about structural notions (finitude, ancestry, identity), which support it as a kind of logic.
  • Effectiveness: logic should provide methods for determining truth. There are different versions of this we could insist on, in decreasing order of strictness:
    • Decidability: if there’s an algorithm that, given any sentence, will terminate in finite time and report whether or not it’s logically true.
      • This would exclude both FOL and SOL. Church and Turing proved that FOL isn’t decidable.
    • Completeness: whether there’s some proof system in which every logically valid sentence is provable (e.g. Hilbert; natural deduction)
      • If you insist on this then FOL is included with SOL excluded, but there’s no obvious principled reason to prefer this.
    • Some decidable fragments: having restricted sublanguages which are decidable.
      • Both FOL and SOL have “monadic fragments” which satisfy this.
• To what extent is the debate substantive?
  • Everybody agrees on the formal properties of what SOL can do, and that it’s between FOL and set theory. So perhaps it’s really just a matter of where to draw the line.
    • It’s not obvious there’s a pre-theoretic notion of logic precise enough to settle the question.
    • As Boolos himself says, the label attached to SOL itself is of “little significance”; what matters are the reasons on either side.
  • However, there are some reasons to care:
    • If SOL is logic, then more of mathematics reduces to logic. This matters philosophically, for Frege’s programme (logicism) arguing that mathematical truths are really logical truths.
      • If SOL is logic, the structure of arithmetic is logically determined (since SOL can uniquely characterise ℕ).
    • It might be that there are meaningful ontological costs associated with using SOL, and we’d want to be aware of that. (And this is one of the features which might lead us to conclude it is set theory, not logic.)
    • It helps us sharpen our conception of where logic’s boundaries are. For example: either SOL isn’t committed to the empty set, or SOL isn’t logic, or the empty set is a matter of logic. Each option is philosophically substantive.
    • It matters for the status of logic itself, too. If SOL is logic, then the incompleteness of SOL means that there are logical truths we can never prove.
      • But if SOL is mathematics, then this is a familiar feature, e.g. see Godel’s incompleteness theorems.

Specific arguments

For SOL being logic

• SOL is a natural extension of FOL, with very similar formal structure.
  • The definition of a model (domain + interpretation function) is identical to FOL, as are logical validity and semantic consequence.
  • All that changes is we extend variable assignment to predicate variables, and add two new clauses to the valuation function (for atomic wffs with predicate variables, and quantification over predicate variables).
  • Given that the apparatus is largely the same, it seems odd to call SOL fundamentally different.
• SOL expands our expressive power to infinitude and the ancestral relation, which seem squarely within the domain of logic.
  • Compactness of FOL means that it cannot express infinitude; and it misses out on inconsistencies like {“There are finitely many things” “There is at least 1 thing”, “There are at least 2 things”, …}, which we might want logic to systematically do.
    • Note that FOL can capture inconsistencies like {“There are at least 5 stars”, “There are fewer than 2 stars”} – and the one above seems of the same type, so it’s not unreasonable to want to be able to capture it too.
    • Compactness: A set of sentences T is satisfiable iff every finite subset of T is satisfiable.
    • Reductio:
      • Suppose FOL has a sentence INF true in a model iff the domain is infinite.
      • Let T = {¬ INF} ∪ {∃_≥n​: n ∈ ℕ}, where ∃_≥n says “there are at least n things”
      • T is clearly unsatisfiable: it says there are finitely many things, but also that there are at least n things for every n.
      • However, every finite subset of T is satisfiable, because you just take a domain with n_max elements.
      • So by compactness, T is satisfiable.
      • Contradiction; no such sentence INF exists in FOL.
    • Similarly it can’t express ideas like “finitely many”, or other generalised quantifiers like “most”.
    • Löwenheim-Skolem: if a countable FOL theory has an infinite model [i.e. is satisfied in such a model], it has a countable model (downward) and models of every larger infinite cardinality (upward).
      • So FOL is blind to the size of infinities; SOL is not.
    • Boolos argues that identifying these inconsistencies “has always been the business of logic”.
  • There are some sentences that SOL lets us express which seem clearly logical.
    • ∃X ∀x: Xx (“there is some predicate whose extension is the whole domain”). Valid in SOL; not expressible in FOL
    • We can express Leibniz’s law (identity of indiscernibles): x=y ⟺ ∀X(Xx ↔ Xy), which means = is idle in SOL (i.e. needn’t be defined as a primitive)
• There’s some semantics (Henkin) where you can restore completeness, downward Löwenheim-Skolem, etc

Against SOL being logic

• SOL has more substantive ontological commitments, which make it akin to set theory.
  • In FOL, predicate letters are schematic, and can stand in for anything. But by quantifying over them in SOL, that means we must be ranging over a domain of values.
    • Compare to how in FOL, quantifying a variable with ∀x ranges over the domain, which must thus be non-empty.
  • Quine argues there are two options for what predicate variables range over: attributes or sets. But attributes are inadequate, and sets bring in set theory.
    • Attributes have an individuation problem: two attributes can be extensionally identical but intensionally distinct (e.g. “has a heart” and “has a kidney”). To work with attributes we need a criterion for when two are the same, but that requires a theory of meaning we don’t have.
    • Sets solve the individuation problem, but then SOL presupposes set-theoretic entities.
  • This gets us to Quine’s core argument: SOL means that predicate letters are value-taking variables (i.e. the X in ∀X takes on all subsets of the domain), not the substitution-taking schematic predicates of FOL.
    • And he claims this shift just is the introduction of set theory.
  • SOL seems to be committed to (something like) the universal set and empty set, because of the validity of sentences ∃X ∀x: Xx and ∃X ∀x: ¬Xx.
    • But logic shouldn’t have anything to say about whether specific entities exist.
    • Quine claims SOL “cunningly hides” its set-theoretic assumptions. For instance, the “comprehension schema” ∃X ∀x (Xx ↔ φ(x)) is a trivial logical truth, even though this is a controversial, dangerous axiom in set theory.
      • It says: for any property φ, there exists a set of all things satisfying φ. Unrestricted, this leads to Russell’s paradox.
• However, Boolos argues that the commitments are actually much milder.
  • The sentences ∃X ∀x: Xx and ∃X ∀x: ¬Xx can be glossed as saying every domain has a subset equal to itself and every domain has an empty sub-collection, not talking about specific mathematical objects like the universal and empty set.
    • These are claims about the structure of any domain whatsoever, not particular mathematical entities.
    • So these commitments are similar to FOL’s commitment to non-emptiness – structural presuppositions about domains, not ontological claims about what exists.
  • You might worry that the SOL comprehension schema leads to Russell’s paradox, but actually this isn’t the case.
    • Although ∃X ∀x(Xx ↔ x∉x) is valid (“there is a property had by exactly the non-self-membered things”), it’s not a paradox.
    • This is because there’s no model whose domain is the collection of all sets (since that collection is a proper class, not a set, and domains must be sets).
    • So the SOL-valid sentence just says that in any given (set-sized) domain, there’s a sub-collection of the non-self-membered things in that domain.
  • SOL is silent on many basic set-theoretic truths: e.g., the existence of a two-membered set is not SOL-valid. So it would be odd to call it “set theory” given how much weaker it is!
• Incompleteness and metatheoretic rupture: FOL is complete, compact, and satisfies Löwenheim-Skolem; SOL is incomplete, not compact, and fails downward L-S.
  • Quine objects that SOL breaks the concurrence between different definitions of logical truth, which FOL does satisfy:
    • (i) Truth in all interpretations
    • (ii) Provability in an adequate proof system
    • (iii) Truth under all substitutions of non-logical vocabulary in a sufficiently rich language).
  • However, Boolos responds that there’s no good reason to privilege completeness over decidability as the standard. And if we drew the line at decidability, FOL would also be excluded.
  • Also, Quine’s concurrence only holds in FOL for truth, not semantic consequence. So the relationship is weaker than he suggests even for what is indisputably logic.
  • Moreover, Quine doubts whether identity is “properly logical”, even though FOL with = is complete – so completeness can’t be a clean criterion even for Quine.

Identity

• = is taken as a primitive logical constant with a fixed interpretation: its extension is always {(d, d): d ∈ D}.
  • This distinguishes it from other binary relations, which are implemented as schematic letters that can always be reinterpreted semantically.
• In SOL, = is idle (i.e., eliminable given other primitives). In FOL, it’s also definable, but only more narrowly.
  • For SOL, we’re able to express Leibniz’s Law, and thus define identity as x = y iff ∀X(Xx ↔ Xy).
  • For FOL, in any language with a finite stock of predicates, Quine shows you can construct a facsimile of =, by just enumerating a conjunction over all of those predicates – i.e., x = y iff x and y are indistinguishable by any sentence expressible in this language.
• Quine asks whether = is proper to logic or to mathematics, and tentatively concludes it’s proper to logic.
  • This is relevant to the SOL debate: it means L= is the baseline logic.
  • Otherwise, even basic FOL-with-identity would have crossed over into mathematics/set theory, let alone SOL.

Against identity being proper to logic

• Tautologies involving = are falsifiable by substitution of non-logical vocabulary (i.e., =), but you might think that genuine logical truths aren’t falsifiable by uniform substitution of non-logical vocabulary.
  • In FOL without identity, tautologies like ∀x(Fx → Fx) remain true however you substitute predicates for predicate letters, because predicate letters are schematic.
  • Yet e.g. ∀x(x = x) does become false if you replace = with another binary predicate.
  • We take = to be non-logical vocabulary because it occupies a predicate-like position: a binary relation “is-the-same-thing-as”.
    • In general we say that logical vocabulary has a fixed interpretation across all models.
    • = does have a fixed interpretation across models (the diagonal relation on the domain), though. So arguably it is just logical vocabulary.
• Logical notions tend to require semantic ascent to generalise, whereas identity doesn’t.
  • To generalise “Tom is mortal or Tom is not mortal”, “Snow is white or snow is not white”, … we must ascend to talk about sentences: “Every sentence of the form ‘p or not-p’ is true.”
    • We’re generalising over sentences, so we need the metalanguage.
  • To generalise “Tom is mortal”, “Dick is mortal”, we stay in the object language: “All men are mortal”.
    • We’re generalising over objects; no need for metalanguage.
  • To generalise the identity notion “Tom is Tom”, “Dick is Dick”, …, we can stay in the object language: “Everything is itself”.
    • So if identity is proper to logic, it would be unique among logical notions in that its generalities can be expressed without semantic ascent.
    • Maybe it is better to think of it as a very general non-logic truth, then.

For identity being proper to logic:

• L= is complete (by Godel’s completeness theorem), unlike set theory / number theory.
  • So this puts it on the logic side of the completeness divide along with plain FOL (although Quine doubts whether completeness is a decisive criterion).
• Identity seems topic-neutral.
  • The sentence x=x is meaningful (and true) for all objects, regardless of what is in the domain. So it doesn’t privilege any particular kind of entity.
    • It’s difficult to think of any contexts where ∀x(x = x) should fail, unlike more set-theoretic sentences like ∀x ∃y(x ∈ y).
    • Or, contrast = with a mathematical predicate like “x is prime”, which clearly privileges numbers.
• Quine’s FOL facsimile of = suggests that you can view it as schematic in the same way as ordinary predicates F.
  • = stands in place of the compound indistinguishability sentences (whose exact form depends on which predicates the language has).
  • This undercuts the substitution objection: if = is schematic, then replacing it with e.g. “is taller than” isn’t a proper uniform substitution – it’s like replacing a sentence letter with something that’s not a sentence.

Other PC-extensions

• Definite descriptions (ι operator) and function symbols.
  • They are both semantically superfluous.
    • Definite descriptions are eliminable via Russell’s theory
    • Function symbols are eliminable by replacing each function f with a relation R_f
  • However, they’re notationally convenient – it’s a lot easier to write out sentences when you have these abbreviations.
  • Also, there are linguistic reasons to want them – e.g. natural language treats “the” as a syntactic unit, and we might want to mirror that in our formalisms.
  • This bears on the SOL debate about identity, in that something can be a legitimate part of logic even if it doesn’t add expressive power.
    • We accept function symbols as part of FOL even though they could be eliminated as primitives; perhaps the same should hold for identity in SOL.