Mondays, 12:30 – 1:20 PM
Zoom link
Spring 2024
April 15 |
Speaker: Jake Kettinger, Colorado State University Title: New Perspectives on Geproci Sets Abstract: The geproci property is a recent development in the world of geometry. We call a set of points Z ⊆ P3 k an (a, b)-geproci set (for GEneral PROjection is a Complete Intersection) if its projection from a general point P to a plane is a complete intersection of curves of degrees a and b. Examples known as grids have been known since 2011 and nondegenerate non-grids have been known only since 2018. Previously, the study of the geproci property has taken place within the characteristic 0 setting; prior to the work in my thesis, a procedure was known for creating specific nondegenerate non-grid (a, b)-geproci sets for 4 ≤ a ≤ b, but it was not known what other examples there can be. Furthermore, before the work in my thesis, almost all examples of geproci sets that were known were contained in unions of b disjoint lines (known as half grids) and there was no known way to generate new examples of non-half grids. Here, I will discuss how to use geometry in positive characteristics to find new methods of producing geproci half grids and non-half grids. |
April 4 |
Speaker: Sankhaneel Bisui, Arizona State University Title: Rational Powers and Summation Formula Abstract: In commutative algebra, the summation formula is very well studied. Mustaţă proved the summation formula for multiplier ideals. In recent work, Hà, Jayanthan, Kumar, and Nguyen proved the summation formula for symbolic powers. Banerjee and Hà proved that the summation formula holds for rational powers of monomial ideals. In a recent project, S. Das, T.H.Hà, J. Montaño, and I also investigated the summation formula for rational powers. In that project, we introduced the concept of the Rees package, which ensures the summation formula for rational powers. In this talk, I will describe the necessary terms with examples. I will also describe the classes of ideals that satisfy the summation formula for rational powers. I will discuss the results from the joint work with S. Das, T.H.Hà, and J. Montaño. |
March 25 |
Speaker: Alperen Ergur, University of Texas at San Antonio Title: Counting Zeros of Sparse Real Polynomial Systems Abstract: Descartes' rule of signs gives an upper bound for the number of real zeros using only number of terms, and is independent of the degree. |
March 18 |
Speaker: Hoai Dao, Oklahoma State University Title: A new symmetric resolution for the (pinched) nth Veronese Abstract: Let S = k[x_1,..., x_n] be a polynomial ring over an arbitrary field k. We construct a new symmetric polytopal minimal resolution of (x_1,..., x_n)^n and a symmetric polytopal minimal resolution of an equigenerated monomial ideal obtained by removing x_1x_2...x_n from the generators of (x_1,..., x_n)^n. |
February 27 |
Speaker: Michele Torielli, Northern Arizona University Title: Lefschetz Properties and Arrangements Abstract: In this talk we will discuss the notion of Weak and Strong Lefschetz properties for graded ring. We will then connect these properties to the study of generic initial ideals. Finally, we will discuss almost complete intersection and hyperplane arrangements from the point of view of Lefschetz properties. This is partially based on a collaboration with S. Marchesi and E. Palezzato. |
February 19 |
Speaker: Le Tran, New Mexico State University Title: Associated Primes of Monomial Ideals and Depth of Edge Ideals of Unicyclic Graphs Abstract: In this talk, we will investigate the associated primes of monomial ideals. In particular, for an arbitrary monomial ideal I, we describe the minimal associated primes of ideals of the form in_>(I,f), where f is a linear form, in terms of the minimal associated primes of I. Moreover, we will describe the embedded associated primes of arbitrary monomial ideals using the notion of star neighbor sets. The analysis of associated primes of monomial ideals will be used to establish initially regular sequences (introduced by Fouli, Hà, and Morey) on cycles C_{3n+2} for n \ge 1. In the last part of the talk, we will discuss the depth of edge ideals of certain unicyclic graphs. |
February 12 |
Speaker: Michael DiPasquale, New Mexico State University Title: An Introduction to Symbolic Powers of Ideals, Part II |
February 5 |
Speaker: Michael DiPasquale, New Mexico State University Title: An Introduction to Symbolic Powers of Ideals Abstract: The Waring rank of a homogeneous form is the number of terms needed to write the form as a sum of powers of linear forms. I will give an introduction and overview of some of the questions around Waring rank. First, motivated by conjectures in complexity theory, it is of interest to determine and compare the Waring ranks of the determinant and permanent. At this time very little is known; in fact, there are very few forms whose Waring rank is known. I will discuss some of the known lower bounds for Waring rank and approaches to determining Waring ranks. The maximum value of Waring rank is unknown in all but a handful of cases; it is even unknown in most cases whether forms with higher than generic rank exist. I will describe ongoing work on apolarity of general hyperplane arrangements. The symmetric analogue of Strassen's conjecture asserts that Waring rank is additive for forms in independent variables. This remains open, despite Shitov's recent counterexample for Strassen's conjecture in the tensor (non-symmetric) case. Time permitting, I will discuss some sufficient conditions for forms to satisfy the assertion of the conjecture. |
Fall 2023
November 13 |
Speaker: Zach Teitler, Boise State University Title: Invitation to Waring rank Abstract: The Waring rank of a homogeneous form is the number of terms needed to write the form as a sum of powers of linear forms. I will give an introduction and overview of some of the questions around Waring rank. First, motivated by conjectures in complexity theory, it is of interest to determine and compare the Waring ranks of the determinant and permanent. At this time very little is known; in fact, there are very few forms whose Waring rank is known. I will discuss some of the known lower bounds for Waring rank and approaches to determining Waring ranks. The maximum value of Waring rank is unknown in all but a handful of cases; it is even unknown in most cases whether forms with higher than generic rank exist. I will describe ongoing work on apolarity of general hyperplane arrangements. The symmetric analogue of Strassen's conjecture asserts that Waring rank is additive for forms in independent variables. This remains open, despite Shitov's recent counterexample for Strassen's conjecture in the tensor (non-symmetric) case. Time permitting, I will discuss some sufficient conditions for forms to satisfy the assertion of the conjecture. |
November 6 |
Speaker: Matt Mastroeni, Iowa State University Title: Koszul Graded Möbius Algebras and Strongly Chordal Graphs Abstract: The graded Möbius algebra of a matroid is a graded commutative algebra that encodes the combinatorics of the lattice of flats of the matroid. As a special subalgebra of the augmented Chow ring of the matroid, these rings played an important role in the recent proof of the Dowling-Wilson Top Heavy Conjecture, which interpolates between the good algebraic properties of the augmented Chow ring and the combinatorics of the graded Möbius algebra. Recently, Mastroeni and McCullough proved that the Chow ring and augmented Chow ring of a matroid are also Koszul. We will discuss joint work with Jason McCullough and Irena Peeva studying when graded Möbius algebras are Koszul, drawing parallels with the much better studied case of Orlik-Solomon algebras throughout. In the case of graphic matroids, our results suggest a new characterization of strongly chordal graphs via edge orderings. (No prior experience with matroids will be necessary for this talk.) |
October 30 |
Speaker: Bruce Olberding, New Mexico State University Title: Connectedness in the Space of Valuation Rings of a Field, Part II |
October 23 |
Speaker: Bruce Olberding, New Mexico State University Title: Connectedness in the Space of Valuation Rings of a Field, Part I Abstract: Zariski’s Connectedness Theorem asserts connectedness for fibers of closed points of certain projective morphisms. This talk focuses on a lifting of this theorem to the space of valuation rings, with the goal of giving a topological criterion for when an intersection of valuation rings is a local ring. We also discuss the case of valuation overrings of a two-dimensional regular local ring, where the topological criterion can be strengthened to a kind of Nullstellensatz for the space of valuation rings. This is joint work with W. Heinzer, A. Loper and M. Toeniskoetter. |
October 16 |
Speaker: Ilya Shapirovskiy, New Mexico State University Title: Syntactic and semantic conditions for local finiteness of modal algebras Abstract: A modal algebra is a Boolean algebra endowed with a unary operation that distributes with respect to finite joints. Important examples are powerset algebras of directed graphs, where the modal operation is induced by the edges. We will be interested in conditions for local finiteness of such algebras. Some known results and open problems will be discussed. |
October 2 |
Speaker: Stefan Tohaneanu, University of Idaho Title: The geometry of the minimum distance Abstract: Let $\mathbb K$ be any field and let $X\subset\mathbb P^{k-1}$ be a set of $n$ distinct $\mathbb K$-rational points, not all contained in a hyperplane. Let $a\geq 1$ be an integer and let $C(X)_a$ be the evaluation code of order $a$ on $X$. This linear code has minimum distance, $d(X)_a$, equal to $n$ minus the maximum cardinality of a proper subset of $X$ that is contained on a hypersurface of degree $a$. |
September 22 |
Speaker: Frank Sottiler, Texas A&M Title: Critical Points Of Discrete Periodic Operators Abstract: It is believed that the dispersion relation of a Schrodinger operator with a periodic potential has non-degenerate critical points, for general values of the potential and interaction strengths. In work with Kuchment and Do, we considered this for discrete operators on a periodic graph G, for then the dispersion relation is an algebraic hypersurface. We showed how, for a given periodic graph G, this may be established from a single numerical verification, if we knew the number of critical points for |
September 18 |
Speaker: Arvind Kumar, New Mexico State University Title: Koszul Algebras and Subadditivity of maximal shifts, Part II |
Spring 2023
May 1 |
Speaker: Giulio Peruginelli, Università di Padova Title: Polynomial Dedekind Domains Abstract: the link |
April 24 |
Speaker: Pat Morandi, New Mexico State University Title: A unified approach to Gelfand and de Vries dualities: Comparing various dualities with the category of compact Hausdorff spaces, Part II |
April 17 |
Speaker: Pat Morandi, New Mexico State University Title: A unified approach to Gelfand and de Vries dualities: Comparing various dualities with the category of compact Hausdorff spaces Abstract: There are several categories of algebras that are dually equivalent to the category of compact Hausdorff spaces and continuous maps and are therefore equivalent to each other. The proof of each duality requires the axiom of choice. In these talks we will discuss the various categories of algebras and how each type of algebra arises from a topological space. We will then discuss the tools we use to give choice-free arguments to show that the various categories are equivalent. This is joint work with Guram Bezhanishvili, Luca Carai, and Bruce Olberding. |
April 10 |
Speaker: Kuei-Nuan Lin, Penn State University, Greater Allegheny Title: Rees algebras of determinantal ideals Abstract: We will give an introduction to SAGBI basis theory and its application to the Rees algebra. We then present a couple of recent results using SAGBI basis theory to find the presentation equations of Rees algebras of determinantal ideals and their properties. |
March 27 |
Speaker: Laura Cossu, University of Graz, Austria Title: Factorization beyond Factorization Theory II |
March 20 |
Speaker: Laura Cossu, University of Graz, Austria Title: Factorization beyond Factorization Theory I Abstract: Many problems in algebra involve the decomposition of certain elements of a ring (or more generally of a monoid) into a product of certain other elements (hereinafter generically referred to as "building blocks") that are in some sense minimal. The classical theory of factorization investigates factorizations in which the building blocks are atoms, i.e., non-unit elements of a monoid that are not products of two non-units. For example, it is well known that every non-zero non-unit of a Dedekind domain (more generally, of a Noetherian domain) can be written as a finite product of atoms and that in general such decompositions are not unique. On the other hand, examples of factorizations that lie beyond the scope of the classical theory include additive decompositions into multiplicative units in rings; cyclic decompositions of permutations in the symmetric group of degree n; idempotent factorizations of the "singular elements'' of a monoid; and so on. |
February 27 |
Speaker: Janet Vassilev, University of New Mexico Title: Constructing new closures and interiors Abstract: In extending a closure operation defined on the ideals of a ring R to a closure on the submodules R-modules, typically 3 different methods have been used. We will discuss these methods along with some standard examples of these extensions. Then we will show that these constructions work to produce new operations from old for a broader class of operations which include interior operations. This talk is based on joint work with Neil Epstein and Rebecca R.G. |
February 20 |
Speaker: Bruce Olberding, New Mexico State University Title: Varieties as topological spaces, Part II |
February 13 |
Speaker: Bruce Olberding, New Mexico State University Title: Varieties as topological spaces, Part I Abstract: We discuss recent work of Kollar, Lieblich and Olsson on the underlying topology of varieties, as well as previous work of R. Wiegand on this topic. |
Fall 2022
November 28 |
Speaker: Bruce Olberding, New Mexico State University Title: A very non-Noetherian ring in a Noetherian setting Abstract: There exist a great variety of non-Noetherian rings (and Noetherian rings, for that matter) but some of the textbook non-Noetherian examples occur in settings that are less familiar. In this talk we do a side-by-side comparison of a certain Noetherian ring and a certain non-Noetherian ring that occur together in a very natural setting. One is familiar (a polynomial ring), and the other not so much (a holomorphy ring). We use these examples to mention some different approaches to commutative algebra that share familiar origins but different goals. |
November 14 |
Speaker: Louiza Fouli, New Mexico State University |
November 7 |
Speaker: Louiza Fouli, New Mexico State University Title: The Depth Function for Monomial Ideals, Part I Abstract: Let $R$ be a polynomial ring and $I$ a monomial ideal in $R$. One important invariant associated to the ideal $I$ is the depth of $R/I$ or more generally, the depth function $f(t)=\depth R/I^t$ for $t\in \mathbb{N}$. We will discuss known and new results regarding this function. |
October 31 |
Speaker: Le Tran, New Mexico State University Title: Initially regular sequences on cycles, Part II |
October 24 |
Speaker: Le Tran, New Mexico State University Title: Initially regular sequences on cycles, Part I Abstract: Let $I$ be a homogeneous ideal in a polynomial ring $R$. Initially regular sequences on $R/I$ are a type of sequence that behaves like regular sequences and whose length provides a lower bound for the depth of $R/I$. We discuss the notion of initially regular sequences on $R/I$ and give an explicit description of an initially regular sequence of length equal to the depth of $R/I$, where $I$ is the edge ideal of any cycle $C_{n}$, for $n\ge 3$. We examine the associated primes of the initial ideal of the form $\text{in}_>(I,f)$, where $f$ is a trinomial and show that they arise from the associated primes of the ideal $I$. I will also discuss some results for the depth of edge ideals of graphs that are extensions of cycles. |
October 17 |
Speaker: Louiza Fouli, New Mexico State University Title: On the core of ideals and modules, Part II |
October 10 |
Speaker: Louiza Fouli, New Mexico State University Title: On the core of ideals and modules, Part I Abstract: In this talk we will discuss the notions of reductions of an ideal and core of an ideal in a Noetherian local ring. We will review basic properties and known results on this topic. As time permits, we will discuss the generalization to minimal reductions of modules and cores of modules. |
September 19 |
Speaker: Alessandra Costantini, Oklahoma State University Title: Ordinary and symbolic powers of symmetric strongly shifted ideals Abstract: Symmetric strongly shifted ideals are a special class of monomial ideals, which is invariant under the action of the symmetric group by permutation of the variables. In this talk, I will describe how their combinatorial structure dictates the algebraic properties of their ordinary and symbolic powers. |
September 12 |
Speaker: Bruce Olberding, New Mexico State University Title: Local rings and connectedness |
Spring 2022
April 4 |
Speaker: Thai T Nguyen, Tulane University Title: Chudnovsky's Conjecture for General Points Abstract: Chudnovsky’s Conjecture suggests lower bounds for the degrees of elements in the symbolic powers of the defining ideal of a set of finitely many points in projective space. In this talk, we will discuss some recent developments on this conjecture with focus on results for general points. I will also present a result for sufficiently large number of general points from our joint work with Sankhaneel Bisui, Eloísa Grifo and Tài Huy Hà; and a more recent result for a smaller number of general points from our joint work with Sankhaneel Bisui. |
March 28 |
Speaker: Janet Vassilev, University of New Mexico Title: Dualizing operations defined via colons Abstract: Building on the duality for submodule selectors developed by Epstein and R.G., we develop a duality between pairs of modules, which we use to produce a dual interior operation for basically full closure on a pair of Artinian modules called basically empty interior which also has a nice formula in terms of colons. Through our duality, we are also able to develop criteria for when a submodule of the injective hull of the residue field is integrally open and formulas to compute the integral-hull of some submodules of the injective hull of the residue field. This is talk is based on joint work with Epstein and R.G. |
March 14 |
Speaker: Marco Abbadini, University Of Salerno, Italy Title: Free extension of universal algebras Abstract: Given an equational class of algebras (such as groups, Boolean algebras, etc.), and a fixed sublanguage of this class (such as monoid operations, lattice operations, etc.), we can show the equivalence of two properties. The first, which is called free extension property, is more semantic: it concerns extensions of certain partial functions to homomorphisms. Whereas the second, called expressibility of equations, is concerned with terms and identities, thus being more syntactic. |
February 28 |
Speaker: Art Duval, UT El Paso Title: Enumerating simplicial spanning trees of shifted and color-shifted complexes, using simplicial effective resistance Abstract: Simplicial electrical networks generalize electrical networks from graphs to higher dimensional simplicial complexes, where resistances, currents, and voltages on the facets of the complex satisfy a generalized Ohm’s law. Simplicial effective resistance, developed by Kook and Lee, generalizes to this setting the notion of effective resistance, which is the resistance of a new facet required to replace a network of resistors. We use simplicial effective resistance to enumerate the simplicial spanning trees of shifted complexes, reproving a known result, and of color-shifted complexes, proving a previously conjectured result. |
Fall 2021
November 15 |
Speaker: Igor Arrieta, University of Coimbra Title: A new diagonal separation and its relations with the Hausdorff property Abstract: Let P be a property of subobjects relevant in a category C. An object X in C is P-separated if the diagonal in X × X has P; thus e.g. closedness in the category of topological spaces (resp. locales) induces the Hausdorff (resp. strong Hausdorff) axiom. Moreover, a topological space is T_1 if and only if the diagonal is an intersection of open subspaces. In this talk we consider locales whose diagonal is fitted (i.e., an intersection of open sublocales - we speak about F-separated locales). Among others, we will show that F-separatedness is a property strictly weaker than fitness. Moreover, we will explore a pleasant parallel with the strong Hausdorff axiom, including a Dowker-Strauss type theorem and a characterization in terms of certain relaxed morphisms (preframe homomorphisms preserving covers in a suitable sense). We will also compare F-separatedness with other point-free separation axioms and finish with some open questions. This is a joint work with Jorge Picado and Aleš Pultr. |
November 8 |
Speaker: Sudipta Das, New Mexico State University Title: A volume = multiplicity formula for Hilbert-Kunz multiplicity |
October 18 |
Speaker: Peter Jipsen, Chapman University Title: Unary-determined distributive l-magmas Abstract: A distributive lattice-ordered magma (dl-magma) (A,^,v,⬝) is a distributive lattice with a binary operation⬝ that preserves joins in both arguments, and when ⬝ is associative then (A,v,⬝) is an idempotent semiring. A dl-magma with a top T is unary-determined if xy = (xT ^ y) v (x ^ Ty). These algebras are term-equivalent to a subvariety of distributive lattices with T and two join-preserving unary operations p,q. We obtain simple conditions on p,q such that xy = (p(x) ^ y) v (x ^ q(y)) is associative, commutative, idempotent and/or has an identity element. Furthermore, we show that a dl-magma with a Boolean lattice reduct and idempotent ⬝ (xx=x) is always unary-determined. |
October 4 |
Speaker: Jonathan Montano Martinez, New Mexico State University Title: Blowup algebras of determinantal ideals in prime characteristic |
September 27 |
Speaker: Bruce Olberding, New Mexico State University Title: Quadratic Transforms, Part 2 |
September 20 |
Speaker: Bruce Olberding, New Mexico State University Title: Quadratic Transforms |
September 13 |
Speaker: Marcus Tressl, University of Manchester Title: An Introduction to Real Closed Rings Abstract: A real closed ring is -- roughly speaking -- an abstract version of a ring of continuous real valued functions on a topological space. |
August 30 |
Speaker: Vladislav Slyusarev, New Mexico State University Title: Modal Logic of Cayley Graphs |
Spring 2021
May 3 |
Speaker: Nick Galatos, University of Denver Title: Almost minimal varieties of commutative integral residuated lattices (joint work with P. Agliano and M. Marcos) Abstract: Residuated structures include lattice-ordered groups, relation algebras, and ideal lattices of rings. They also form algebraic semantics of various non-classical logics, such as linear, relevance, many-valued and intuitionistic; therefore Boolean and Heyting algebras also form examples. Maximal consistent logics correspond to minimal non-trivial varieties of residuated lattices. We focus on the case of integral and commutative residuated lattices and we study their minimal and almost minimal subvarieties, showing that even at these very low levels there is a lot of complexity. We will start with a quick review of the necessary tools from universal algebra. |
April 26 |
Speaker: Susan Morey, Texas State University Title: Resolutions of Powers of Monomial Ideals Abstract: Using combinatorial structures to obtain resolutions of monomial ideals is an idea that traces back to Diana Taylor’s thesis, where a simplex associated to the generators of a monomial ideal was used to construct a free resolution of the ideal. This concept has been expanded over the years, with various authors determining conditions under which simplicial or cellular complexes can be associated to monomial ideals in ways that produce a free resolution. |
April 19 |
Speaker: Jim Madden, Louisiana State University Title: Conjunctive Join Semilattices Abstract: A join-semilattice L is said to be conjunctive if it has a top element 1 and it satisfies the following first-order condition: for any two distinct a, b in L, there is c in L such that EXACTLY one of the two suprema a∨c and b∨c is equal to 1. Equivalently a join-semilattice is conjunctive if every principal ideal is an intersection of maximal ideals. This talk discusses the history of the concept and numerous applications in topology, frame theory, and lattice theory. |
April 12 |
Speaker: James Lewis, New Mexico State University Title: Binomial Edge Ideals of Graphs and Ideals of Konig-type |
March 29 |
Speaker: Robert Walker, University of Wisconsin Title: Uniform Asymptotic Growth of Symbolic Powers of Ideals Abstract: Algebraic geometry (AG) is a major generalization of linear algebra which is fairly influential in mathematics. Since the 1980's with the development of computer algebra systems like Mathematica, AG has been leveraged in areas of STEM as diverse as statistics, robotic kinematics, computer science/geometric modeling, and mirror symmetry. Part one of my talk will be a brief introduction to AG, to two notions of taking powers of ideals (regular vs symbolic) in Noetherian commutative rings, and to the ideal containment problem that I study in my thesis. Part two of my talk will focus on stating the main results of my thesis in a user-ready form, giving a "comical" example or two of how to use them. At the risk of sounding like Paul Rudd in Ant-Man, I hope this talk will be awesome. |
March 15 |
Speaker: Warren McGovern, Florida Atlantic University Title: When is C(X) an h-local Ring Abstract: The h-local domains were originally studied by Matlis in an attempt to generalize results on Dedekind domains and local domains. The domain D is said to be h-local if every non-zero prime ideal is contained in a unique maximal ideal and every non-zero element has finite character. Olberding (2007) has a list of 20 equivalent conditions characterizing h-local domains. |
March 1 |
Speaker: Darío García, Universidad de los Andes Title: Pseudofinite Dimensions and Cardinalities of Definable Sets in Finite Structures Abstract: The fundamental theorem of ultraproducts ( Los' Theorem) provides a transference principle between the finite structures and their limits. It states that a formula is true in the ultraproduct M of an infinite class of structures if and only if it is true for ”almost every” structure in the class, which presents an interesting duality between finite structures and their infinite ultraproducts. This kind of finite/infinite connection can sometimes be used to prove qualitative properties of large finite structures using the powerful known methods and results coming from infinite model theory, and in the other direction, quantitative properties in the finite structures often induce desirable model-theoretic properties in their ultraproducts. These ideas were used by Hrushovski (cf. [2]) to apply ideas from geometric model theory to additive combinatorics, locally compact groups and linear approximate subgroups. |
February 22 |
Speaker: Keller Vandebogert, University of South Carolina Title: Linear Strands Supported on Cell Complexes Abstract: In this talk, we will consider linear strands of ideals that can be supported on a cell complex. It turns out that certain classes of "rainbow" monomial ideals will always have this property; as a consequence, any such ideal with linear resolution must have cellular resolution. We will then look at some conditions ensuring linearity (that can be turned into an equivalence with an extra assumption), and apply these results to say some words about polarizations of Artinian monomial ideals. Some of this work is joint with Ayah Almousa. |
February 8 |
Speaker: Rick Ball, University of Denver Title: The Anatomy of A Completely Regular Frame Abstract: The apparatus of point free topology can be fruitfully brought to bear on the most classical of topological subjects: namely completely regular frames. Such a frame is a (canonical) union of an ascending cardinally indexed sequence of kappa-frames, starting with the cozero part. In addition, every such frame has a (canonical) descending cardinally indexed sequence of minimal dense kappa Lindelof sublocales, ending with its booleanization. Taken together, these features form a kind of scaffolding which is descriptive of many of the salient attributes of the frame. |
February 1 |
Speaker: Morgan Sinclaire, New Mexico State University Title: Formally Verifying Peano Arithmetic Abstract: Gentzen's consistency proof is a central result in proof theory that demonstrates the consistency of Peano arithmetic (PA) using a technique known as cut-elimination. The proof can be carried out in the weaker finitist system of primitive recursive arithmetic (PRA), if one extends that system with the principle of transfinite induction over the ordinal ε_0. In our work, we have partially implemented a version of this proof as a computer program in the Coq theorem prover. Consequently, the key steps in the proof have been computer verified, and many of its interesting structures-such as Cantor normal form ordinals and infinitary proof trees-have been built as constructive, finitistic objects. |