Non-Extensional Higher Order Logic with Substitution

Abstract: The most widely studied systems of classical higher-order logic are ‘extensional’ in the sense that they validate the schema ∀x₁…xₙ(Fx₁…xₙ↔Gx₁…xₙ) → (F=G): intuitively, this means that they coextensive properties or relations are identical. Although this seems philosophically suspect for obvious reasons, the space of logics that keep the classical laws for propositional connectives and quantifiers while dropping extensionality has been surprisingly little explored. This talk will explore a natural way of weakening extensionality by replacing it with the rule ⊦Fx₁…xₙ↔Gx₁…xₙ / ⊦F=G, or equivalently, a rule that allows provably materially equivalent formulae to be intersubstituted anywhere. I will give several very different axiomatizations of this system, thereby cementing the case for its naturalness. After that I will discuss a range of possible extensions of the system, some of which restore certain arguably attractive consequences of extensionality, and others of which take the view in a more “fine-grained” direction by systematically adding claims of non-identity which the basic system leaves unsettled. Finally, I will describe a technique for constructing set-theoretic models of the system, which can be used to prove the consistency of many of the aforementioned extensions.

The talk will be based on a forthcoming paper coauthored with Andrew Bacon, available here: philarchive.org/rec/BACC-8.

logic

Audience: researchers in the topic

( paper )

---

Online logic seminar

Series comments: Description: Seminar on all areas of logic

---