Examples of mathematical theories that are naturally written in exotic logics

Question

Zermelo's set theory (ZF), Peano's arithmetic (PA), Tarski's theory of closed real fields (RCF), Hilbert-Tarski's geometry, etc. are all naturally expressed in first-order logic (FOL) (with a single sort).

Apart from second-order arithmetic (SOA), which is written in second-order logic (SOL) (or, equivalently in terms of syntax, in two-sorted first-order logic) and type theories such as simple type theory (STT), are there any examples of mathematical theories that naturally use more exotic logics, such as branching quantifiers, counting quantifiers (without classical quantifiers), etc.?

(I know that this would mean losing many tools and results from model theory.)

Answer 1

There is no end to "exotic logics" in computer science, and they express very natural things, such as behavior of programs, communication systems, security protocols, etc. To give just one example, Hoare logic has judgements of the form $$\{P\}\ c\ \{Q\}$$ which read roughly as "if $P$ holds and command $c$ terminates, then $Q$ will hold". For example, $\{ x < 5 \}\ x \mathrel{{:}{=}} x + 1\ \{ x^2 + 5 < 42\}$ is valid. There are many variants and extensions of Hoare logic, depending on what your programming language can do, and what sort of properties of programs we want to talk about.

A more mathematical example is geometric logic, which is used quite a bit in topos theory. It is "exotic" in the sense that it has infinitary disjunctions.

I would also include dependent type theory as a properly mathematical example of an "exotic logic". In particular, homotopy type theory is a variant of dependent type theory that serves as a foundation of mathematics, but is not organized in the traditional way, with a stratification of objects and statements.

Answer 2

It is up for debate how "natural" their approach is, but Smullyan and Fitting use modal logic to develop forcing, in their book, Set Theory and the Continuum Problem. See Michael Weiss's notes for a discussion of the pros and cons of this book.

EDIT: Let me say a bit more. A conventional way to think about forcing is that we are hypothesizing how the universe $M$ of all sets can be expanded by adjoining a new set $G$, to form a larger universe $M[G]$. Intuitively, since $G$ is typically something like "a set with cardinality between $\aleph_0$ and $2^{\aleph_0}$," we don't "know" that $G$ exists, and cannot directly answer questions such as "Is $p\in G$?" On the other hand, we can use logical reasoning to make conditional statements of the form, "if $p\in G$ then statement $\phi$ is forced to hold." This subtle state of affairs motivates the idea that not all statements $\phi$ have a definite truth value. Fairly soon after Cohen's proof, Scott and Solovay used Boolean-valued models to develop forcing; we have a Boolean algebra, and we think of the top element as "provably true" and the bottom element as "provably false," but there is a whole hierarchy in between. A particular choice of $G$ crystallizes the answers to all questions of the form "is $p\in G$?" and singles out a "generic ultrafilter" of the Boolean algebra, which may be thought of as a self-consistent way of assigning truth values to statements $\phi$ that are not provable truths or falsehoods.

Given this state of affairs, it is natural to ask whether modal logic, which formalizes the idea of statements being "possibly true" and "possibly false," can be used to develop the theory of forcing. Smullyan and Fitting show that the answer is yes.

Answer 3

Among some algebraic geometers it is customary to (at least implicitly) use intuitionistic logic when talking about sheaves and their sections. Indeed, this is the foundation of the link between topos theory and logic. But it is also down-to-earth natural, and the lack of law of excluded middle does not feel exotic in this context.

To those who do not know what a sheaf is:

Consider a topological space $X$. The logic formulae in question concern functions on $X$, and more generally on open subsets of $X$. The extra flexibility we get from considering all open subsets at once comes in very handy if we want to talk e.g. about solutions of a differential equation, whose solutions might only exist locally. More generally, we can talk about sheaves on $X$ (which are devices which associate a group compatibly to every open subset of $X$), maps between sheaves, etc. Let me denote the set of "functions" (or differential forms, or solutions to a differential equation, or... "sections" of a sheaf) on an open set $U\subseteq X$ by $\mathcal{F}(U)$.

The point is that in such a formula, the symbol $f$ (or any other variable) will refer to a function $f$ defined on an unspecified open subset of $X$. So in ordinary logic we would write "let $U\subseteq X$ be an open subset and let $f\in \mathcal{F}(U)$." Here, instead we write simply "let $f\in \mathcal{F}$" (which would be a type error in ordinary mathematics). If we write $f+g$ it means "$f+g$ on the open subset where both $f$ and $g$ are defined."

To understand the lack of excluded middle, consider the formula $$ f = 0 \vee f = 1 $$ it means that locally on $X$, $f$ is equal to $0$ or $1$. But, maybe the implicit open set $U$ is disconnected, $U = U_0\sqcup U_1$, and $f$ equals $0$ on $U_0$ and $1$ on $U_1$. In particular, neither of the sentences $$ f = 0, \qquad f \neq 0 $$ holds true.

Once one internalizes this feature, thinking and writing about sheaves becomes easier and more natural.

In order to "come back" to ordinary logic, we could just fix the open set $U$. A different, more natural way of doing this is: we pick a point $x\in X$. We can then "evaluate" $f$ at $x$. More precisely, we only consider $f$ which are defined in an open neighborhood of the point $x$. The direct limit $\mathcal{F}_x$ of $\mathcal{F}(U)$ over all such $U$ is called the "stalk of $\mathcal{F}$ at $x$." It is an ordinary set in which we do business as usual. Let us denote by $=_x$ the relation "equal in a small enough neighborhood of $x$" or, which is the same, "have the same image in the stalk $\mathcal{F}_x$". Then, if $f = 0 \vee f = 1$ then either $f =_x 0$ or $f\neq_x 0$, i.e. excluded middle holds "at x", but we get different meanings for different points of $x$.

In topos theory, we would say that $x$ defines a "point of the topos of sheaves on $X$." For an algebraic geometer, a topos is simply the category of all sheaves on a fixed topological space $X$ (or on a "site", a generalization of a topological space which is natural from the point of view of sheaf theory). Thus, points of $x$ provide "interpretations" of the logic of (the topos corresponding to) $X$ in ordinary first-order logic.

Answer 4

There is infinitary Zermelo-Fraenkel set theory $ZF_{\kappa}$, introduced in the habilitation thesis of Klaus Gloede in 1974. This is a generalization of $ZF$ in which, among other things, the axiom of pairing is replaced by an analogous axiom asserting the existence of a set containing exactly $\kappa$ elements, for some infinite regular cardinal $\kappa$, and where the axiom schema of separation/replacement admit instances based on infinitary formulas.

The infinitary language used by Gloede to formulate $ZF_{\kappa}$ was, however, not $\mathcal{L}_{\kappa, \kappa}$, but rather a generalization of it $\mathcal{L}_{A, A}$ for certain admissible class of sets $A$. The point is to avoid using the axiom of choice in the formulation of the metatheory.

The system arises naturally when one is considering Gödel's constructible hierarchy in infinitary logic, since in general the study of inner models defined by infinitary languages runs into the following metatheoretical issue: while in the finitary case the notion of relativization of a formula to a class and the notion of truth, coincide, the same relation is not at all obvious in the infinitary case, since the relativization of an infinitary formula is an infinitary formula, while in general the notion of truth of an infinitary formula is defined by means of a finitary formula. However in a suitable chosen infinitary set-theoretical system, one can appropriately extend this relation, as shown by Gloede.

In addition to this, the study of Gödel's constructible hierarchy with sets definable in $\mathcal{L}_{\kappa, \kappa}$) is in fact better understood in the context of $ZF_{\kappa}$, since while usually the axiom of choice is not satisfied in such inner models (as there seems to be no way of defining an internal well-ordering), the right generalization that holds in such a model is $WO_{\kappa}$, the generalization of well orderings to total orders in which there is no descending chain of size less than $\kappa$.

Answer 5

From the SEP entry on paraconsistent logics:

A paraconsistent approach makes it possible to have theories of truth and sethood in which the mathematically fundamental intuitions about these notions are respected. For example, as Brady (1989; 2006) has shown, contradictions may be allowed to arise in a paraconsistent set theory, but these need not infect the whole theory.

There are several approaches to set theory with naive comprehension via paraconsistent logic. Models for paraconsistent set theory are described by Libert (2005). The theories of ordinal and cardinal numbers are developed axiomatically using relevant logic in Weber 2010b, 2012. The possibility of adding a consistency operator to track non-paradoxical fragments of the theory is considered in Omori 2015, taking a cue from the tradition of da Costa. Naive set theory using adaptive logic is presented by Verdée (2013); see Batens 2020 for current developments in adaptive Fregean Set Theory.

From the SEP entry on inconsistent mathematics:

But ZF and others such as NBG and the like were in various ways ad hoc, having to include multiple independent principles instead of a single simple comprehension axiom. Hence, a number of people including da Costa (1974), Brady (1971, 1989), Priest, Routley, & Norman (1989, pp. 152, 498), considered it preferable to retain the full power of the natural comprehension principle, and tolerate a degree of inconsistency in set theory. Brady, in particular, has extended, streamlined and simplified these results on naive set theory in his book (2006). For a clear account see also Restall’s review (2007).