Contributed Talks 5
Chair: PaulAndré Melliès
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
16:30 
Stella Mahler, Herbrand's theorem for inductive proofs 
Authors: Alexander Leitsch and Stella Mahler Herbrand’s theorem, an important characteristic of formal proofs, bridges propositional and firstorder logic by stating that any valid firstorder 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 firstorder statement, typically obtained through cutelimination. 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 cutelimination 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 cutelimination method CERES (schematic CERES) to firstorder proof schemata [1]. These schemata are parameterized sequences of firstorder 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


16:55 
Anouk Michelle Oudshoorn, Combining SHACL and description logics 
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 standalone set of SHACL constraints that preserves validation for every input graph. This is done by precomputing the results of the inference rules and implementing this in the constraints. We show that validation in this setting is EXPTIMEcomplete in combined complexity, but only PTIMEcomplete in data complexity, i.e., if the constraints and the inference rules are fixed. 

17:20 
Leonardo Pacheco, Higherorder feedback computation 
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 semicomputable sets are the \(\Pi^1_1\) sets. We can also show that the feedback semicomputable 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 secondorder feedback machines. Note that we must now have a new and stronger notion of freezing to avoid a contradiction by diagonalization. Having defined secondorder feedback computation, it is now natural to ask: what about third, fourth, and higherorder feedback? We define \(\alpha\)th order feedback Turing machines for each computable ordinal \(\alpha\).
We also describe feedback computable and semicomputable sets using inductive definitions and Gale–Stewart games.
Specifically, we prove the following levelbylevel correspondence:
(This is joint work with Juan P. Aguilera and Robert S. Lubarsky.) Bibliography


17:45 
Luca San Mauro, A new way of classifying word problems 
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 NovikovBoone 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, MengChe Ho, and Andrea Sorbi. 

18:10 
Dominik Kirst, Constructive Reverse Mathematics of the Downwards LöwenheimSkolem Theorem 
Authors: Dominik Kirst and Haoyi Zeng The LöwenheimSkolem (LS) theorem is a central result about firstorder logic, entailing that the formalism is incapable of distinguishing different infinite cardinalities. In particular its socalled 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öwenheimSkolem (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 metatheory, 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. 