Authors: Alexander Leitsch and Stella Mahler

Herbrand’s theorem, an important characteristic of formal proofs, bridges propositional and first-order logic by stating that any valid first-order formula can be expressed as a finite disjunction of propositional formulas. Translated to sequent calculus, it asserts the existence of a propositionally valid sequent (the Herbrand sequent) for each proof of a first-order statement, typically obtained through cut-elimination.

In presence of mathematical induction Herbrand’s theorem fails, as a side effect of handling the implicit infinity. While the infinite is never needed for arguing by mathematical induction, it is implicit in its construction.

Yet, methods exist for cut-elimination in the presence of induction, albeit yielding proofs lacking the subformula property and Herbrand’s theorem cannot be realized.

Despite the absence of Herbrand’s theorem for inductive proofs, we demonstrate the construction of a finite representation (the Herbrand system) of an infinite sequence of sequents representing the Herbrand sequent of a proof. This is achieved through a generalization of the cut-elimination method CERES (schematic CERES) to first-order proof schemata [1]. These schemata are parameterized sequences of first-order proofs constructed using primitive recursive definitions.

Additionally, our presentation will delve into an initial exploration of the characterization of inductive proofs analyzable by schematic CERES, with a particular focus on examining the relationship between our formalism of proof schemata and primitive recursive arithmetic.

Bibliography

1. Leitsch, Alexander, Nicolas Peltier, and Daniel Weller,CERES for first-order schemata,Journal of Logic and Computation,vol. 27 (2017), no. 7, pp. 1897–1954.

Authors: Anouk Michelle Oudshoorn, Shqiponja Ahmetaj, Magdalena Ortiz and Mantas Simkus

A standardised and widely used way to organise structured knowledge on the internet are knowledge graphs (KGs). Description logics (DLs), a family of modal logic like logics, can formally describe KGs and define reasoning rules like each student has a student number. However, DLs are not suitable for defining constraints on data: the goal is to find out which parts of the data are not satisfying the constraints, instead of adding the logical consequences, or conclude that the theory is unsatisfiable. For this purpose, the SHACL standard was created. SHACL is a constraint language that has a description logic flavour, and contains features like regular path expressions, negation and recursion.

SHACL reasoners perform validation, while DL reasoners logical inference. Integrating these two tasks into one uniform approach is a relevant but challenging problem. We address this problem by proposing an intuitive semantics for validating SHACL constraints combined with some lightweight DLs. Moreover, we propose an algorithm that rewrites a set of recursive SHACL constraints (with stratified negation, i.e., not allowing the full combination of negation and recursion) combined with DL inference rules, into a stand-alone set of SHACL constraints that preserves validation for every input graph. This is done by pre-computing the results of the inference rules and implementing this in the constraints. We show that validation in this setting is EXPTIME-complete in combined complexity, but only PTIME-complete in data complexity, i.e., if the constraints and the inference rules are fixed.

Feedback Turing machines are Turing machines which can query a halting oracle \(h:\subseteq \omega\times\omega\to \{\downarrow,\uparrow\}\), which has information on the convergence or divergence of feedback computations. That is, given the code \(e\) for a feedback Turing machine and an input \(n\) the oracle \(h\) answers if the computation \(\{e\}^h(n)\) converges or diverges. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A feedback Turing machine freezes when it asks the halting oracle \(h\) about a pair \(\langle{e,n}\rangle\) not in the domain of \(h\).

Feedback Turing machines were first studied by Ackerman, Freer and Lubarsky [1,2]. They proved that the feedback computable sets are the \(\Delta^1_1\) sets and the feedback semi-computable sets are the \(\Pi^1_1\) sets. We can also show that the feedback semi-computable sets are the winning regions of Gale–Stewart games with \(\Sigma^0_1\) payoff [3].

A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? These new machines are second-order feedback machines. Note that we must now have a new and stronger notion of freezing to avoid a contradiction by diagonalization. Having defined second-order feedback computation, it is now natural to ask: what about third-, fourth-, and higher-order feedback?

We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\). We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games. Specifically, we prove the following level-by-level correspondence:
Theorem. For all \(\alpha<\omega_1^\mathrm{ck}\), the following classes coincide:

• the \((\alpha+1)\)-feedback semi-computable sets;
• the sets definable by \(\alpha+1\) simultaneous arithmetical inductive operators; and
• the sets of winning positions of Gale–Stewart games whose payoffs are differences of \(\alpha+1\) many \(\Sigma^0_2\) sets.

(This is joint work with Juan P. Aguilera and Robert S. Lubarsky.)

Bibliography

1. Nathanael L. Ackerman and Cameron E. Freer and Robert S. Lubarsky,Feedback Turing Computability, and Turing Computability as Feedback,30th Annual ACM/IEEE Symposium on Logic in Computer Science,(2015) pp. 523–534.
2. Nathanael L. Ackerman and Cameron E. Freer and Robert S. Lubarsky,An Introduction to Feedback Turing Computability,Journal of Logic and Computation,vol. 30 (2020), no. 1, pp. 27–60.
3. Yannis N. Moschovakis,Descriptive Set Theory,Mathematical surveys and monographs, vol. 155,American Mathematical Society,2009.

The study of word problems dates back to the work of Dehn in 1911. Given a recursively presented algebra \(A\), the word problem of \(A\) is to decide if two words in the generators of \(A\) refer to the same element. Much is known about the complexity of word problems for familiar algebraic structures: e.g., the Novikov-Boone theorem, one of the most spectacular applications of computability to general mathematics, states that the word problem for finitely presented groups is unsolvable. Yet, the computability theoretic tools commonly employed to measure the complexity of word problems (e.g., Turing or \(m\)-reducibility) are defined for sets, while it is generally acknowledged that many computational facets of word problems emerge only if one interprets them as equivalence relations.

In this work, we revisit the world of word problems, with a special focus on groups and semigroups, through the lens of the theory of equivalence relations, which has grown immensely in recent decades. To do so, we employ computable reducibility, a natural effectivization of Borel reducibility.

This talk collects joint works with Uri Andrews, Valentino Delle Rose, Meng-Che Ho, and Andrea Sorbi.

Authors: Dominik Kirst and Haoyi Zeng

The Löwenheim-Skolem (LS) theorem is a central result about first-order logic, entailing that the formalism is incapable of distinguishing different infinite cardinalities. In particular its so-called downward part (DLS), stating that every infinite model can be turned into a countably infinite model with otherwise the exact same behaviour, can be considered surprising or even paradoxical. Therefore the exact assumptions under which the downward Löwenheim-Skolem (DLS) theorem applies have been analysed thoroughly: From the perspective of (classical) reverse mathematics [?,?], the DLS theorem is equivalent to the dependent choice axiom (DC), a weak form of the axiom of choice, stating that there is a path through every total relation [?,?,?].

An even more informative answer, taking into account the computational content, can be obtained by the perspective of constructive reverse mathematics [?,?]. This programme is concerned with the analysis of logical strength over a constructive meta-theory, i.e. in particular without the law of excluded middle (LEM), stating that \(p\lor\neg p\) for all propositions \(p\), and ideally also without countable choice (CC) [?], a consequence of DC. In that setting, finer logical distinctions become visible and thus one can investigate whether (1) the DLS theorem still follows from DC alone, without any contribution of LEM, and (2) whether it still implies the full strength of DC, without any contribution of CC. We show that neither (1) nor (2) is the case by observing that the DLS theorem requires a fragment of LEM, which we call the blurred drinker paradox, and that it implies only a similarly blurred fragment of DC.