We will show there is no sequence of distinct Sigma^2_1 sets of length (delta^2_1)^+ in L(R). We also discuss how to prove an analogous result for any inductive-like pointclass in L(R). This is joint work with Itay Neeman and Grigor Sargsyan.

There are many duality theorems in both finite and infinite graph theory that relate the maximum number of disjoint paths through a given graph G to the minimum size of a cut-set disconnecting G. The quintessential example is Menger's theorem, which says that the maximum number of vertex disjoint paths between two vertices x and y in a finite graph G is equal to the minimum size of a vertex cut disconnecting x and y.

We present a general approach to proving path/cut-set duality theorems for locally finite graphs. As one consequence of this approach, we give novel proofs of Menger's theorem and another classical duality result due to Halin. As another, we prove the following general existence theorem, which can be viewed as a maximal extension of König's lemma: given an infinite, locally finite connected graph G and a vertex x in G, there is a pruned tree T contained in G and rooted at x that, in a precise sense, splits as early and as often as possible.

After Sela and Kharlampovich-Myasnikov proved that nonabelian free groups share the same common theory, a model theoretic interest for the theory of the free group arose. Moreover, maybe surprisingly, Sela proved that this common theory is stable. Stability is the first dividing line in Shelah's classification theory and it is equivalent to the existence of a nicely behaved independence relation - forking independence. This relation, in the theory of the free group, has been proved (Ould Houcine-Tent and Sklinos) to be as complicated as possible (n-ample for all n). This behavior of forking independence is usually witnessed by the existence of an infinite field. We prove that no infinite field is interpretable in the theory of the free group, giving the first example of a stable group which is ample but does not interpret an infinite field.

Jensen's covering lemma states that either every uncountable set of ordinals is covered by a constructible set of ordinals of the same size or else there is an elementary embedding from the constructible universe to itself. This talk takes up the question of whether there could be an analog of this theorem with constructibility replaced by ordinal definability. For example, we answer a question posed by Woodin: assuming the HOD conjecture and a strongly compact cardinal, there is no nontrivial elementary embedding from HOD to HOD.

Progress in artificial intelligence (AI), including machine learning (ML),
is having a large effect on many scientific fields at the moment, with much more to come.
Most of this effect is from machine learning or "numerical AI", 
but I'll argue that the mathematical portions of "symbolic AI" 
- logic and computer algebra - have a strong and novel roles to play
that are synergistic to ML. First, applications to complex biological systems
can be formalized in part through the use of dynamical graph grammars.
Graph grammars comprise rewrite rules that locally alter the structure of
a labelled graph. The operator product of two labelled graph
rewrite rules involves finding the general substitution 
of the output of one into the input of the next - a form of variable binding 
similar to unification in logical inference algorithms. The resulting models
blend aspects of symbolic, logical representation and numerical simulation.
Second, I have proposed an architecture of scientific modeling languages
for complex systems that requires conditionally valid translations of
one high level formal language into another, e.g. to access different
back-end simulation and analyses systems. The obvious toolkit to reach for
is modern interactive theorem verification (ITV) systems e.g. those
based on dependent type theory (historical origins include Russell and Whitehead).
ML is of course being combined with ITV, bidirectionally.
Much work remains to be done, by logical people.
 

This is part 1 of a 2 part talk. It will cover background on:
Sketch of background knowledge in typed formal languages, 
Curry-Howard-Lambek correspondence, 
current computerized theorem verification, ML/ITV connections;
scientific modeling languages based on rewrite rules
(including dynamical graph grammars),
with some biological examples.