From Proofs to Computation in Geometric Logic and Generalizations

After a brief introduction to skolemization and to coherent logic, we discuss three possible research directions, relevant for automated reasoning.

• $\mathrm{■}$

  Generalization of skolemization from (properly quantified) atoms to coherent sentences. Due to the implication in the latter, one could call this conditional (or hypothetical) skolemization.

• $\mathrm{■}$

  More efficient proof systems for coherent logic. Ground forward reasoning is conceptually very simple and therefore attractive, but it leads to exponentially longer proofs as compared to non-ground rules.

• $\mathrm{■}$

  Comparison of the length of skolemized and non-skolemized proofs. The latter are known to be (much) longer in the case of first-order logic, but this is unknown for the coherent fragment.

Realizability theory provides a bridge between constructive and computable mathematics. In its basic form, the fundamental result is that there is a mechanical way to extract from any given constructive number-theoretic proof a computable witness, a so-called “realizer” for instance, a realizer for the infinitude of primes is a Turing machine computing larger and larger prime numbers.

From this basic picture, originally due to Kleene, gradually several enhancements emerged: to higher-order statements and proofs; to proofs set in flavors of classical set theory; and to different machine models.

This evening talk featured a leisurely introduction to realizability theory. For building intuition, we focused on the following examples, exploring for each its status in classical mathematics, constructive mathematics, ordinary realizability and realizability based on infinite time Turing machines:

1. 1.

   Every number is prime or not prime.

2. 2.

   Every map $\mathbb{N}\to \mathbb{N}$ has a zero or not.

3. 3.

   Every map $\mathbb{N}\to \mathbb{N}$ is (Turing-)computable.

4. 4.

   Every map $ℝ\to ℝ$ is continuous.

5. 5.

   Markov’s principle holds.

6. 6.

   Countable choice holds.

7. 7.

   Heyting arithmetic is categorical.

8. 8.

   A statement holds iff it is realized.

9. 9.

   There is an injection $ℝ\hookrightarrow \mathbb{N}$.

Our decision to approach our exploration in a constructive metatheory allowed us to discuss inheritance of classical principles. For instance, Markov’s principle is realized if and only if it holds in the metatheory, while countable choice is realized even if it fails in the metatheory.

This was an exploratory talk, outlining the structure of an envisioned geometric type theory.

The idea is to have a type theory capable of formalizing geometric reasoning, proving results such as $((\varphi \to \perp )\to \perp )=1$ for the generic proposition $\varphi$, and similarly other non-geometric properties of generic objects; and also capable of constructing common geometric maps and bundles.

The intended model is based on (small) toposes (or $(\mathrm{\infty },1)$-toposes for a homotopical version), where

• $\mathrm{■}$

  contexts are such toposes $𝒳$

and with two different type judgments:

• $\mathrm{■}$

  $𝒳⊢A$ étale_i corresponding to sheaves over $𝒳$ in ${𝒰}_i$ (classified by the usual univalent universes ${𝒰}_i$)

• $\mathrm{■}$

  $𝒳⊢Y$ space_i corresponding to geometric morphisms $p:𝒴\to 𝒳$ in ${𝒰}_i$.

We mentioned that maybe we should allow $Y$ itself to be in ${𝒰}_j$, necessitating two indices, space_i,j.

Correspondingly, there should be two different element judgments:

• $\mathrm{■}$

  $𝒳⊢a:A$ corresponding to sections of sheaves,

• $\mathrm{■}$

  $𝒳⊢y:P{t}_i(Y)$ corresponding to geometric sections $y:𝒳\to 𝒴$ in ${𝒰}_j$.

We also need to consider two fragments:

• $\mathrm{■}$

  A geometric fragment ($\mathrm{\Sigma }$,Id,finitary HITs) stable under all geometric morphisms, and

• $\mathrm{■}$

  A full fragment ($\mathrm{\Pi }$,W,universes) stable only under étale morphisms.

An inspiration is Mike Shulman’s observation that in the $(\mathrm{\infty },1)$-world atomic=logical=étale.

A question arose as to whether we prove that spaces are exponentiable, or whether we need a separate judgment for that. If we write $[Y,Z]$ for the exponential, then if $A,B$ are étale, the $\mathrm{\Pi }$-type $A\to B$ should be the discrete coreflection $(A\to B)\to [A,B]$.

For the generic proposition (and hence all propositions) $\varphi$, we should get $[[\varphi ,0],0]=\varphi$.

Although classical principles such as the law of excluded middle or the axiom of choice are not available in constructive mathematics, constructive mathematics can make sense of them: The double-negation translation interprets classical logic in intuitionistic logic, and Gödel’s $L$ translation embeds zfc in zf. In this way, proofs in classical mathematics can be understood as blueprints for constructive proofs; classical proofs can be decrypted to unearth obscured constructive content. Several other techniques for making constructive sense of classical proofs exist as well. Adding the law of excluded middle or the axiom of choice typically does not increase the consistency strength at all.

In contrast, there is no similar translation from impredicative mathematics to predicative mathematics; indeed, impredicative foundations are typically much stronger than their predicative counterparts. Hence it seems that predicative foundations cannot make sense of impredicative systems.

The evening talk explored that, fantastically, in some cases it is still possible to extract predicative content from impredicative proofs. As direct translations are no longer possible, the talk offered a whirlwind tour of the required tool, ordinal analysis, including a discussion of the true limits of predicative reasoning.

Algebraic Geometry is about studying shapes given by polynomial equations. Systems of polynomial equations are mapped to some “space” of solutions (the common zeros). It turns out that we can just use sets as “spaces” if we do not insist on the axiom of choice or the law of excluded middle. In their absence we can ask that the SQC axiom (of Blechschmidt) holds: The map $A\to R^{\mathrm{Spec}(A)}$ is an isomorphism for all finitely presented $R$-algebras $A=R[X_1,\mathrm{\dots },X_n]/(P_1,\mathrm{\dots },P_{\mathrm{\ell }})$ and $\mathrm{Spec}(A):=\{x\in R^n\mid \forall i.P_i(x)=0\}$. Together with two other axioms, this is the start of a well-working synthetic version of algebraic geometry which is modeled by a sheaf topos, the Zariski topos.

In the talk we also mentioned the topic of finite schemes in the synthetic setting, hoping to spark new ideas in connecting the geometric-algebraic notion of a finite scheme with finiteness notions in constructive mathematics.

In 1970, building on work of Davis, Putnam, and Robinson, Matiyasevich established a complete classification of subsets of the integers which can be described by an existential first-order formula in the language of rings, in terms of their computability by a Turing machine. After Gödel’s (in)famous Incompleteness Theorems, this marks one of the major milestones in the study of computability in number theory, and it has inspired continued research into (existential) first-order definability of subsets of rings.

This evening talk offers a lighthearted initiation into the realm of first-order and existential definability within fields, with a focus on the field of rational numbers. Through various examples, I highlight the intricacies surrounding the classification of definable subsets of the rationals and associated decidability problems, while showcasing the diverse array of methodologies drawn from algebra, number theory, quadratic form theory, and model theory that have been employed to tackle them. To align with the theme of this week’s seminar, particular attention is devoted to contrasting constructive and non-constructive approaches to these problems. Nonetheless, the talk remains accessible to audiences with classical training and assumes no prior background knowledge.

We investigate seven natural variations of the linearity axiom

and the following principles in the context of intermediate propositional logic and arithmetic:

In fact, the hierarchy of ${\mathrm{\Sigma }}_n$-fragments of the logical principles over Heyting arithmetic $\mathrm{𝖧𝖠}$ is quite different from that of the intermediate propositional logics induced by the logical principles. For a separation result on the ${\mathrm{\Sigma }}_n$-fragment of

in arithmetic, we employ a meta-theorem with respect to extended frame to an appropriate propositional Kripke model which refutes ${\mathrm{LIN}}_7$.

In the Proof Mining paradigm one applies proof-theoretic transformations to extract new computational information (e.g. programs or effective bounds) as well as qualitative improvements (e.g. by weakening of assumptions) from given prima facie noneffective proofs in different areas of core mathematics. In this talk, we will

• $\mathrm{■}$

  discuss recent extensions (mainly due to [8] but see also [5]) of the existing framework for logical bound extraction metatheorems to cover set-valued monotone and accretive operators in Hilbert and Banach spaces;

• $\mathrm{■}$

  indicate the potential of generalizing mined proofs such as the quantitative analysis of a Halpern-type proximal point algorithm in suitable Banach spaces given in [3] to new geodesic settings ([7, 10]) as well as to the context of so-called Bregman strongly nonexpansive mappings ([8], [9]);

• $\mathrm{■}$

  show how a rate of convergence for the Dykstra algorithm in convex optimization which recently has been obtained in [6] under a metric regularity assumption can be explained in terms of a novel extension of the concept of Fejér monotonicity ([4]);

• $\mathrm{■}$

  prove the first linear rates of asymptotic regularity for the
  Tikhonov-Mann algorithm in geodesic spaces as an application of proof mining ([1]);

• $\mathrm{■}$

  present the first effective rate of convergence for the asymptotic regularity of ergodic averages of iterations of nonexpansive mappings in uniformly convex Banach spaces ([2]).

Arithmetic universes were built by A. Joyal in the seventies in some lectures, all still unpublished, to provide a categorical proof of Gödel’s incompleteness theorems. They amount to be exact completions of the lex category of predicates of a given Skolem theory. In [1] we proposed the notion of list-arithmetic pretopos as the general abstract notion of arithmetic universe.

In our talk, we report recent results obtained in joint work with Davide Trotta in [3]. We show that each arithmetic universe is the exact completion of the pure existential completion of the doctrine of its Skolem predicates. The notion of existential completion was introduced by D. Trotta in [4] and further analyzed in [2] in terms of existential free objects relative to an existential doctrine. In particular, we show in [3] that the Skolem predicates of an arithmetic universe provide a projective cover of the exact completion of their free pure existential completion. As a byproduct, we conclude that the initial arithmetic universe is the exact completion of the doctrine of recursively enumerable predicates.

Gurevich logic is an extended constructive three-valued logic obtained from intuitionistic logic by adding a connective $\sim$ of strong negation, with the following axiom schemata, where $\neg$ is intuitionistic negation:

1. 1.

   $\sim \sim A\supset \subset A$,

2. 2.

   $\sim \neg A\supset \subset A$,

3. 3.

   $\sim A\supset \neg A$,

4. 4.

   $\sim (A\wedge B)\supset \subset \sim A\vee \sim B$,

5. 5.

   $\sim (A\vee B)\supset \subset \sim A\wedge \sim B$,

6. 6.

   $\sim (A\supset B)\supset \subset A\wedge \sim B$.

Nelson logic, also known as Nelson’s constructive three-valued logic N3, is the intuitionistic negation-less fragment of Gurevich logic.

The primary formal difficulty in developing a natural deduction system for logics of strong negation lies in the requirement of having rules for $\neg$ and $\sim$ without $\perp$. This is solved using the rules of explosion, of $\neg$-introduction, and of excluded middle:

The following are presented:

• $\mathrm{■}$

  Natural deduction and G3-style sequent calculi systems for Gurevich and Nelson logic.

• $\mathrm{■}$

  A translation between the natural deduction and sequent calculi introduced, with an indirect proof of normalization as a consequence of cut elimination.

• $\mathrm{■}$

  A syntactic embedding of Gurevich logic into intuitionistic logic.

• $\mathrm{■}$

  A classical sequent calculus with strong negation, used as a platform for obtaining classical logics of strong negation, such as Avron and De-Omori logics.

• $\mathrm{■}$

  A Glivenko theorem for embedding classical logic with strong negation into Gurevich logic.

It is known that weak König’s lemma (WKL) is strictly weaker than König’s lemma (KL) in Friedman-Simpson’s reverse mathematics ([2]). Then a natural question is how we can characterise the difference between WKL and KL. In Simpson’s book, it is stated:

• $\mathrm{■}$

  WKL does not imply ${\mathrm{\Sigma }}_1^0$ induction.

• $\mathrm{■}$

  WKL is equivalent to KL for trees with height-wise bounded functions over ${\mathrm{𝖱𝖢𝖠}}_0$.

It is also known that Fan theorem, a classical contraposition of KL, yields ${\mathrm{\Sigma }}_1^0$ induction over ${\mathrm{𝖱𝖢𝖠}}_0^{\ast }$ ([1]). In this talk, we consider the difference between WKL and KL in the context of constructive reverse mathematics and the relationship between KL and ${\mathrm{\Sigma }}_1^0$ induction.

The negation in intuitionistic logic has sometimes been criticised as problematic. One reason for this is the alleged lack of witness for negated conjunctions: not-(A and B) may hold without one of not-A and not-B being so. As a remedy, David Nelson introduced an alternative notion of “constructible falsity”, which promises such a witness. Nelson’s negation can even be made paraconsistent, which also encouraged the abandonment of intuitionistic negation altogether. However, such a move may obscure the notion of negation from the viewpoint of an intuitionistic logician. In this talk, I am going to give an overview of some different views for constructive negation. Then I will suggest another solution to the problem of negated conjunction. This solution, which leads to a variant of Heinrich Wansing’s logic C, hints that intuitionistic negation and paraconsistent constructible falsity may be seen as complementary, once we accept some contradictions to be provable.

We present cs-topologies, or topologies of complemented subsets, as a new approach to constructive topology that preserves the duality between open and closed subsets of classical topology. Complemented subsets were used successfully by Bishop in his constructive formulation of the Daniell approach to measure and integration. We use complemented subsets in topology, in order to describe simultaneously an open set, the first-component of an open complemented subset, and its complement as a closed set, the second component of an open complemented subset. We analyse the canonical cs-topology induced by a metric, and we introduce the notion of a modulus of openness for a cs-open subset of a metric space. Pointwise and uniform continuity of functions between metric spaces are formulated with respect to the way these functions inverse open complemented subsets together with their moduli of openness. The addition of moduli of openness in the concept of an open subset, given a base for the cs-topology, makes possible to define the notion of uniform continuity of functions between csb-spaces, that is cs-spaces with a given base. In this way, the notions of pointwise and uniform continuity of functions between metric spaces are directly generalised to the notions of pointwise and uniform continuity between csb-topological spaces.

Proofs in mathematics often have a narrative quality to them, taking the reader on a long journey. Sometimes the reader has to wait for new mathematical characters (like imaginary numbers) to be created so the journey can be continued. Hilbert called these novel characters ideal elements. His conservation program was the idea that, while being important for the advancement of mathematics, ideal elements should be eliminable from proofs of concrete mathematical theorems.

Investigations by a long list of mathematicians/logicians (e.g. Weyl, Hilbert, Bernays, Lorenzen, Takeuti, Feferman, Friedman, Simpson to name a few) have shown that large swathes of ordinary mathematics can be undergirded by theories of fairly modest consistency strength. This confirms what Hilbert surmised in his program, namely that elementary results (e.g. those expressible in the language of number theory) proved in abstract, non-constructive mathematics can often be proved by elementary means.

The best known program for calibrating the strength of theorems from ordinary mathematics is reverse mathematics (RM). RM’s scale for measuring strength is furnished by certain standard systems couched in the language of second order arithmetic. However, its language is not expressive enough to be able to talk about higher order objects, such as function spaces, directly.

Richer formal systems, in which higher order mathematical objects can be directly accounted for, have been suggested. The price for maintaining conservativity over elementary theories, however, is that one has to use different logics for different ontological realms, allowing classical logic to reign at the level of numbers whereas higher type mathematical objects are merely answerable to intuitionistic logic. In the talk, I’d like to present some of these semi-intuitionistic systems, give a feel for carrying out mathematics within them, and relate them to systems considered in RM.

Continuous model theory is an area of model theory in which one studies structures where the truth values of sentences can be any element of the unit interval. This branch of model theory has applications in areas where metric structures are pervasive, such as in analysis and probability theory.

In this talk we propose an analysis of continuous model theory based on ideas from categorical logic, in particular Lawvere’s notion of a hyperdoctrine. We propose a hyperdoctrine for continuous model theory and show that this hyperdoctrine can be embedded in the subobject hyperdoctrine of a topos. This means that continuous logic can be understood as the internal logic of a suitable topos.

For point-free topology (locales, etc.) we can reason validly in a natural manner using points, provided we restrict ourselves to constructions that are geometric – preserved by pullback along geometric morphisms. This style has now been applied in some results of real analysis, including exponentiation and logarithms (joint with Ming Ng) and the Fundamental Theorem of Calculus.

Are such constructions constructive in the strong sense of yielding algorithms? This is very unclear. My talk discusses some aspects of the question.

1. 1.

   Some constructive taboos are true geometrically! But that is because they have to be interpreted topologically.

2. 2.

   Geometric maths can be understood via an ontology of observations rather than constructions.

3. 3.

   Point-free surjections, which embody conservativity principles, allow us to reason as if certain constructions can be done, even when they can’t.

The Fundamental Theorem of Calculus is so fundamental that, once it has been proved point-free, much subsequent development can be more or less standard. In a 5 minute minitalk I summarized the main features in [1] by which this was achieved.

1. 1.

   Lower and upper integrals, valued as lower and upper reals, were described in [2]. After this, it is necessary only to show how they can be combined to give Dedekind reals.

2. 2.

   Differentiation is treated in a Carathéodory style, with limits replaced by the existence of continuous slope maps. This was used in [3], where also Rolle’s Theorem was proved.

3. 3.

   For the derivative of an integral, the slope map can be defined as an integral with respect to the uniform valuation on $[x_0,x]$. Geometricity guarantees that this is continuous even at the limiting case $x=x_0$.

Infinite time Turing machines provide an exotic model of computation where the the operation of Turing machines is extended to infinite ordinal time. They have been devised by Joel David Hamkins and Andy Lewis and offer an intriguing connection between computability theory and set theory. Among their special features is that the realizability model they give rise to validates the peculiar statement “there is an injection $ℝ\hookrightarrow \mathbb{N}$”, contradicting both classical mathematics and ordinary Turing realizability.

In the working group, we explored possible avenues for formalizing the notion of infinite time Turing machines in proof assistants based on dependent type theory. To the best of our knowledge, infinite time Turing machines have not been object of constructive scrutiny before.

In a constructive setting, a fundamental question is whether the cell contents should be Booleans or general truth values. The latter seem to force their inclusion as limsups of sequences of Booleans, but are at odds with the envisioned mechanical flavor of the computational model. We tentatively resolved this tension by sticking to Booleans, but weakening the transition function to a transition relation. Arbitrary infinite time Turing machines can then not be expected to have a well-defined execution trace, but many machines of interest will.

The working group concluded with a first sketch of the basic definitions in Agda, parametrized by the choice of ordinals used for indexing the time steps.

Agda is one of the commonly-used dependently typed proof assistants, facilitating collaborative verification and development of mathematical proofs. The strategic decision to schedule this tutorial on the first day of the seminar allowed participants to explore Agda during the week. The tutorial was a joint session of several people already well-versed in Agda, and profited greatly from numerous questions and comments from people with varying backgrounds, including familiarity with other different proof assistants and those new to the realm of computer formalization of mathematics.

This working group presented an informal overview of the basics of the proof theory for geometric axioms together with recent developments.

Sara Negri presented and introduction to the method of “axioms as rules” applied to coherent and geometric axioms. By the method, cut- and contraction-free sequent calculi of the G3 family are extended while maintaining their structural properties [3, 5, 4]. One can go beyond geometric axioms by a change of basic notions (such as apartness instead of equality), by the method of systems of rules, and by the method of “geometrization” [1].

Elaine Pimentel showed how focusing and polarities can be applied for the construction of synthetic inference rules. In particular, we showed how this method can be applied for generating sequent rules for geometric axioms, advancing the work developed by Sara Negri and colleagues.

Edi Pavlović discussed the application of these methods in formal metaphysics. In particular, he discussed a four-sided sequent calculus for neutral free logic, how it simplifies quantifier rules for quantified weak Kleene, and what that can tell us.

Eugenio Orlandelli presented a terminating calculus for monadic first-order logic. The calculus has all rules invertible without relying on (implicit) contraction. The decision procedure based on this calculus has optimal complexity.

Giulio Fellin presented an infinitary version of Orevkov’s theorems about the Glivenko sequent classes [2].

In the geometric style of point-free reasoning, just from the existence and nature of classifying toposes $𝒮[{𝕋}_X]$, we can say that

• $\mathrm{■}$

  space $X$ = geometric theory ${𝕋}_X$ (point = model of the theory),

• $\mathrm{■}$

  map = geometric construction of points from points.

I explained how one further gets

• $\mathrm{■}$

  bundle = geometric construction of spaces from points.

This is the essence of dependent type theory. We also get pullbacks of bundles as substitution. I focused on the case of localic bundles, but it does go through more generally for bounded geometric morphisms.

So: how is a map $p:Y\to X$ a bundle?

Joyal and Tierney [2] showed that localic maps $p$ are equivalent to internal frames in the topos of sheaves over $X$. In [3] I showed how to replace an internal frame by a presentation $𝕋$ of it, and then for a map $f:Z\to X$ the pullback $f^{\ast }Z$ can be obtained from $f^{\ast }(𝕋)$, where now $f^{\ast }$ is the inverse image functor. This amounts to substitution.

If $X$ already corresponds to a theory ${𝕋}_X$, then the internal $𝕋$ amounts externally to an extension ${𝕋}_Y$, a process that is easier to work with if one uses “geometric type theory” rather than forcing theories into a standard form such as sites or first order theories.

For more discussion, see [1].