PCC 2018 Contributed Talks with Abstracts

Abstract: I will discuss some theorems of Specker, Mostowski and myself. If time permits, I will also discuss some variants of b-adic representations.

(This is the talk I intend to give at PCC 2017. The talk was canceled since
I was poisoned in an Italian restaurant.)

Abstract: A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this paper we will develop a theory for these computational flows to design a classical direct reading of the Dialectica interpretation. This theory makes a sound and complete interpretation for bounded theories of arithmetic as well as the low complexity statements of strong unbounded systems. We will first use this fact to extract the computational content of the low complexity statements in some bounded theories of arithmetic such as $IU_k$, $T^k_n$, $I\Delta_0(exp)$ and $PRA$. And then we will apply the theory on some strong unbounded mathematical theories such as $PA$ and $PA+TI(\alpha)$ using the bridge of continuous cut elimination technique.

Abstract: A recursive representation of formal proofs has proven essential for proof analysis in the presence of induction by global cut elimination methods such as CERES (Cut Elimination by Resolution). Such {\em schema of proofs} played an integral role in the proof analysis of F\"{u}rstenberg's proof of the infinitude of primes by Baaz et al. Over the past few years the proof analysis methods for so called {\em proof schemata} have been developed enough to ask meta-theoretic questions concerning complexity, expressive power, and completeness; of particular interest is deepening our understanding of the evaluation procedure of the recursive cut structure extracted from proof schemata. This is the heart of schematic proof analysis and also the most difficult step to perform. We discuss the recent advancements in the field as well as an interesting problem concerning refutational complexity of recursive clause sets.

Abstract: The central feature of Belnap’s Display Logic is the possibility of
displaying every formula occuring in any given sequent as the only
formula in either the antecedent or succedent. This is accomplished by
means of structural connectives that retain the positional information
of the contextual formulae as they are moved aside. Goré accomodates
substructural, intuitionistic and dual intuitionistic logic families by
building upon a basic display calculus for Bi-Lambek logic. His version
uses two nullary, two unary, and three binary structural connectives.
Since the structural connectives are not independent of one another,
display equivalences are required to mediate between the binary
structural connectives.

I propose an alternative approach in which two graph-like ternary
structural connectives express one set of three structural connectives
each. Each of these new connectives represents all three sequents making
up one of the two display equivalences. The notion of sequent disappears
and is replaced by that of a structure tomograph consisting of systems
of ternary connectives in which nodes mark the linking of the
connectives and of formulae to those connectives. The turnstile of a
sequent is represented by the highlighting of a single node linking
connectives.

Abstract: The aim of our study, which is work in progress, is to determine a spartan formal theory of sets and functions that will reflect the practice of Bishop's constructive mathematics while avoiding serious unexpected features with respect to it.

Abstract: In the framework of Bishop's constructive mathematics, we show that for convex functions on compact intervals all kinds of contuinuity notions are equivalent.

Abstract: The researchers Cai, Ganchev, Lempp, Miller and Soskova proved that the total Turing degrees TOTe are definable in the enumeration degrees De: a degree is total iff it is trivial or a join of a maximal Kalimullin pair. The result may generalize to an α-level in higher computability theory for an admissible ordinal α. I will outline the proof of Aut(Dαe) embeds into Aut(TOTαe) based on the 3 statements:
1. TOTαe degrees are embeddable in Dαe,
2. TOTαe are an automorphism base for Dαe,
3. TOTαe are definable in Dαe.
The various parts of the results are established for different classes of admissible ordinals α. The talk will focus on the open problems in the area to initiate a further progress in solidifying the results.

Abstract: This work is in the context of Heyting arithmetic in all finite types (HA omega). In "A direct proof of Schwichtenberg's bar recursion closure theorem" (J. Symbolic Logic, 2018), Oliva and Steila introduced a variant of bar recursion, called general bar recursion, where the stopping condition of Spector's bar recursion is replaced by a monotone decidable bar. It is non-trivial whether any such bar admits a functional that satisfies the general bar recursion with respect to the bar. However, we can show that the decidable bar induction (of a suitable type) ensures the existence of the general bar recursor for any monotone decidable bar. Conversely, in HA omega extended with a suitable tree type, the existence of the bar recursor for any monotone decidable bar implies the decidable bar induction. This is a joint work with Makoto Fujiwara (Waseda Institute of Advanced Study).

Abstract: We show that several weakenings of the Cauchy condition are all equivalent under the assumption of countable choice, and investigate to what extent choice is necessary. We also show that the syntactically reminiscent notion of metastability allows similar variations, but is empty in terms of its constructive content.

Abstract: The bounded comprehension axiom asserts that for any formula A(x), we have
fragments of the characteristic function of the set {x: A(x)} of
arbitrary finite length.
In classical reverse mathematics, it is known to be equivalent to the
induction principle.
In constructive reverse mathematics, it is characterized by some
combination of induction principles and the law of excluded middle.
Recently, it turned out that bounded comprehension is needed to prove
the monotone convergence theorem (MCT), i.e., any bounded monotone
sequence is convergent.
In this talk, I will explain a constructive proof of MCT and where we
need the bounded comprehension axiom.