AVM 2023, Arbeitstagung Verona-München
18.01.2023

Place

Talks

Abstracts

• Hajime Ishihara: Reflexive combinatory algebras
  
  We introduce the notion of reflexivity for combinatory algebras. Reflexivity can be thought of as an equational counterpart of the Meyer-Scott axiom of combinatory models, which indeed allows us to characterise an equationally definable counterpart of combinatory models. This new structure, called strongly reflexive combinatory algebra, admits a finite axiomatisation with seven closed equations, and the structure is shown to be exactly the retract of combinatory models. Lambda algebras can be characterised as strongly reflexive combinatory algebras which are stable.
  
  This is a joint work with Marlou M. Gijzen and Tatsuji Kawai
  
  
• Ingo Blechschmidt: On the scope of the dynamical method in commutative algebra
  
  Since its multiple independent inventions by Dominique Duval and Paul Lorenzen, the general toolbox of the dynamical method has been widely successful in extracting computational content from classical proofs appealing to the transfinite. By connecting dynamical algebra with constructive variants of set-theoretic forcing, we recover the dynamical method as a parametrized version of the celebrated double-negation translation and give formal a priori criteria elucidating the scope of the dynamical method.
  
  Joint work with Peter Schuster
  
  
• Satoru Niki: An alternative notion of constructible falsity
  
  The notion of constructible falsity was proposed by N.D. Nelson (1948) as an alternative account of constructive negation. Systems with constructible falsity can be seen to have a `bilateral' flavour: each connective has a falsification condition on a par with a verification condition. In this talk, I shall introduce alternative systems which modify Nelson's falsification condition for implication to the one that is closer to how an intuitionistic negation of implication behaves. I shall discuss some characteristics of the systems, which can offer reasons to prefer them over Nelson's logics. In addition, I shall give further comparisons with other related systems.
  
  
• Tatutji Kawai: Predicative theory of stably locally compact locales
  
  We give a predicative presentation of stably locally compact locales, the class of locales which includes locally compact regular locales (e.g., localic reals) as its subclass. In our setting, a stably locally compact locale is presented as a quasi-proximity lattice, a quasi-bounded distributive lattice (distributive lattice without top) together with a certain idempotent relation on it. Using this structure, we construct a coreflection from the category of locally compact regular locales and cobounded maps to that of stably locally compact locales and perfect maps. The construction of this coreflection generalizes Dedekind's construction of real numbers as pairs of a lower and an upper cut.
  
  
• Nils Köpp: Strong Negation in the Theory TCF
  
  Following the intuition that in constructive mathematics (CM) connectives are interpreted in a strong fashion, we incorporate strong negation in the theory of computable functionals TCF. TCF, a common extension of Plotkin's PCF and G\"{o}del's system T, is a suitable formal system to formalize large parts of CM. We simultaneously define the strong negation of formulas and (co)inductive predicates. We present various properties of the strong negation, i.p. Double-Negation-Elimination, and examples which reveal the naturality of strong negation in TCF.
  
  Joint work with Iosif Petrakis
  
  
• Giulio Fellin: Glivenko sequent classes and constructive cut elimination in geometric logics
  
  A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules-given in earlier work by Sara Negri-is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer's Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded parameter called proof embeddability. Additionally, conservativity for classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes.
  
  Joint work with S. Negri, E. Orlandelli
  
  
• Iosif Petrakis: Categories with dependent arrows
  
  An arrow is the abstract, categorical version of a function. What is the abstract, categorical version of a dependent function? To answer this question, we first present the notion of fam-Category, a category with family-arrows. A (fam, Sigma)-Category is a fam-Category with Sigma-objects, where a (fam, Sigma)-Category with a terminal object is exactly a type-category of Pitts, or a category with attributes of Cartmell. We introduce categories with dependent arrows, or dep-Categories, and we show that every (fam, Sigma)-Category is a dep-Category in a canonical way. The notion of a Sigma-object in a dep-Category is affected by the existence of dependent arrows, and we show that every (fam, Sigma)-Category is a (dep, Sigma)-Category in a canonical way. All these notions of categories have a dual counterpart.
  
  

  Last change

  18. January 2023