The notion of relative interpretation is one of the essential tools of proof theory. In [1]\, Avigad demonstrated how forcing can be understood in the context of proof theory and how it is related to relative consistency or c onservation proofs. Indeed\, one may see that forcing is a generalization of a relative interpretation by means of the Kripke semantics.
\n \n
M oreover\, such an interpretation usually provides a feasible (polynomial) proof transformation as digested in [2]. In this talk\, we will overview s uch ideas and show that many conservation theorems for systems of second-o rder arithmetic can be converted to non-speedup theorems.
\n \n[1] J. Av
igad\, Forcing in proof theory. Bull. Symbolic Logic 10 (2004)\, no. 3\, 3
05-333.
\n[2] J. Avigad\, Formalizing forcing arguments in subsystems o
f second-order arithmetic. Ann. Pure Appl. Logic 82 (1996)\, no. 2\, 165-1
91.
\n[3] L. A. Kolodziejczyk\, T. L. Wong and K. Yokoyama\, Ramsey's t
heorem for pairs\, collection\, and proof size\, submitted.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dale Miller (Inria & IP Paris)
DTSTART:20210303T170000Z
DTEND:20210303T180000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/10
DESCRIPTION:Title: Focusing Gentzen's LK proof system\nby Dale Miller (Inria & IP Par
is) as part of Proof Theory Virtual Seminar\n\n\nAbstract\nGentzen's seque
nt calculi LK and LJ are landmark proof systems. They identify the structu
ral rules of weakening and contraction as notable inference rules\, and th
ey allow for an elegant statement and proof of both cut-elimination and co
nsistency for classical and intuitionistic logics. Among the undesirable f
eatures of those sequent calculi is the fact that their inferences rules a
re very low-level and that they frequently permute over each other. As a r
esult\, large-scale structures within sequent calculus proofs are hard to
identify. In this paper\, we present a different approach to designing a s
equent calculus for classical logic. Starting with Gentzen's LK proof syst
em\, we first examine the proof search meaning of his inference rules and
classify those rules as involving either don't care nondeterminism or don'
t know nondeterminism. Based on that classification\, we design the focuse
d proof system LKF in which inference rules belong to one of two phases of
proof construction depending on which flavor of nondeterminism they invol
ve. We then prove that the cut-rule and the general form of the initial ru
le are admissible in LKF. Finally\, by showing that the rules of inference
for LK are all admissible in LKF\, we can give a completeness proof for L
KF provability with respect to LK provability. We shall also apply these p
roperties of the LKF proof system to establish other meta-theoretic proper
ties of classical logic\, including Herbrand's theorem. This talk is based
on a recent draft paper co-authored with Chuck Liang.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andreas Weiermann (Ghent)
DTSTART:20210317T090000Z
DTEND:20210317T100000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/11
DESCRIPTION:Title: Goodstein sequences and notation systems for natural numbers\nby A
ndreas Weiermann (Ghent) as part of Proof Theory Virtual Seminar\n\n\nAbst
ract\nTermination theorems for Goodstein sequences provide canonical examp
les for the Gödel incompleteness of systems of arithmetic and set theory.
The original Goodstein sequence is based on canonical notations for natur
al numbers using addition and exponentiation. In our exposition we conside
r more general forms of notations which are based on the Ackermann functio
n and related functions and we use them to define Goodstein sequences. The
resulting termination theorems will be independent of relatively strong s
ystems of arithmetic. We prove some general results about the notation sys
tems for natural numbers and try to explain how these results might be con
nected to the problem of canonical well orderings and to comparison theore
ms between the slow and fast growing hierarchies. The exposition is aimed
at a general audience.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Greg Restall (Melbourne)
DTSTART:20210421T090000Z
DTEND:20210421T100000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/12
DESCRIPTION:Title: Comparing Rules for Identity in Sequent Systems and Natural Deduction<
/a>\nby Greg Restall (Melbourne) as part of Proof Theory Virtual Seminar\n
\n\nAbstract\nIt is straightforward to treat the identity predicate in mod
els for first order predicate logic. Truth conditions for identity formula
s are straightforward. On the other hand\, finding appropriate rules for i
dentity in a sequent system or in natural deduction leaves many questions
open. Identity could be treated with introduction and elimination rules in
natural deduction\, or left and right rules\, in a sequent calculus\, as
is standard for familiar logical concepts. On the other hand\, since ident
ity is a predicate and identity formulas are atomic\, it is possible to tr
eat identity by way of axiomatic sequents\, rather than inference rules. I
n this talk\, I will describe this phenomenon\, and explore the relationsh
ips between different formulations of rules for the identity predicate\, a
nd attempt to account for some of the distinctive virtues of each differen
t formulation.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Antonina Kolokolova (Newfoundland)
DTSTART:20210630T170000Z
DTEND:20210630T180000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/14
DESCRIPTION:Title: Learning from Bounded Arithmetic\nby Antonina Kolokolova (Newfound
land) as part of Proof Theory Virtual Seminar\n\n\nAbstract\nThe central q
uestion of complexity theory -- what can (and cannot) be feasibly computed
-- has a corresponding logical meta-question: what can (and cannot) be fe
asibly proven. While complexity theory studies the former\, bounded arithm
etic is one of the main approaches to the meta-question. There is a tight
relation between theories of bounded arithmetic and corresponding complexi
ty classes\, allowing one to study what can be proven in\, for example\, "
polynomial-time reasoning" and what power is needed to resolve complexity
questions\, with a number of both positive and negative provability result
s.
\n \nHere\, we focus on the complexity of another meta-problem:
learning to solve problems such as Boolean satisfiability. There is a rang
e of ways to define "solving problems"\, with one extreme\, the uniform se
tting\, being an existence of a fast algorithm (potentially randomized)\,
and another of a potentially non-computable family of small Boolean circui
ts\, one for each problem size. The complexity of learning can be recast a
s the complexity of finding a procedure to generate Boolean circuits solvi
ng the problem of a given size\, if it (and such a family of circuits) exi
sts.
\n \nFirst\, inspired by the KPT witnessing theorem\, a specia
l case of Herbrand's theorem in bounded arithmetic\, we develop an interme
diate notion of uniformity that we call LEARN-uniformity. While non-unifor
m lower bounds are notoriously difficult\, we can prove several unconditio
nal lower bounds for this weaker notion of uniformity. Then\, returning to
the world of bounded arithmetic and using that notion of uniformity as a
tool\, we show unprovability of several complexity upper bounds for both d
eterministic and randomized complexity classes\, in particular giving simp
ler proofs that the theory of polynomial-time reasoning PV does not prove
that all of P is computable by circuits of a specific polynomial size\, an
d the theory V^1\, a second-order counterpart to the classic Buss' theory
S^1_2\, does not prove the same statement with NP instead of P.
\n
\nFinally\, we leverage these ideas to show that bounded arithmetic "has t
rouble differentiating" between uniform and non-uniform frameworks: more s
pecifically\, we show that theories for polynomial-time and randomized pol
ynomial-time reasoning cannot prove both a uniform lower bound and a non-u
niform upper bound for NP. In particular\, while it is possible that NP!=P
yet all of NP is computable by families of polynomial-size circuits\, thi
s cannot be proven feasibly.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Revantha Ramanayake (Groningen)
DTSTART:20210505T170000Z
DTEND:20210505T180000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/15
DESCRIPTION:Title: Up and Down the Lambek Calculus\nby Revantha Ramanayake (Groningen
) as part of Proof Theory Virtual Seminar\n\n\nAbstract\nI will present re
cent results using proof theory that establish decidability and complexity
for many substructural logics. Specifically: for infinitely many axiomati
c extensions of the commutative Full Lambek calculus with contraction/weak
ening\, including the prominent fuzzy logic MTL. This work can be seen as
extending Kripke’s decidability argument for FLec (1959). I aim to isola
te some of the proof-theoretic motifs that feature in this type of work. T
hese include: refinement of backward and forward proof search\, cut-free p
roof systems via structural rule extension\, absorption of contraction rul
es\, and upper bounding proof search via controlled bad sequences.\n \nJoi
nt work with A.R. Balasubramanian and Timo Lang.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hugo Herbelin (INRIA Paris)
DTSTART:20210616T090000Z
DTEND:20210616T100000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/16
DESCRIPTION:Title: On the logical structure of choice and bar induction principles\nb
y Hugo Herbelin (INRIA Paris) as part of Proof Theory Virtual Seminar\n\n\
nAbstract\nWe present an alternative equivalent generalised formulation GD
C(A\,B\,T) of the axiom of choice (for T a predicate filtering the finite
approximations of functions from A to B)\, of the form "coinductive T-appr
oximability implies T-compatible choice function" such that:
\n \n-
GDC(ℕ\,B\,T) is essentially the axiom of dependent choices
\n- GDC(A
\,Bool\,T) is essentially the statement of the Boolean prime filter theore
m
\n- GDC(ℕ\,Bool\,T) reduces to their common intersection\, namely e
ssentially weak König's lemma
\n- GDC(A\,B\,R⁺)\, for R⁺ some spec
ific filtering predicate defined from a relation R on A and B\, is the sta
tement of the general axiom of choice
\n \nIts syntactic contraposi
tive GBI(A\,B\,T) "T is barred implies T is inductively barred" is such th
at:
\n \n- GBI(ℕ\,B\,T) is essentially bar induction\, and close
also to countable Zorn's lemma
\n- GBI(A\,Bool\,T) is essentially the s
tatement of Tarski completeness theorem in the form validity implies prova
bility for Scott's entailment relations
\n- GBI(ℕ\,Bool\,T) reduces t
o their common intersection\, namely essentially the weak fan theorem
<
br>\n \nWe will also present further explorations aiming at integrating th
e full version of Zorn's lemma in the picture. Note that all equivalences
will be considered under the eyes both of constructive and linear logic.
\n \nThis is joint work with Nuria Brede.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lutz Straßburger (INRIA & LIX Paris)
DTSTART:20210602T170000Z
DTEND:20210602T180000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/17
DESCRIPTION:Title: Towards a Combinatorial Proof Identity\nby Lutz Straßburger (INRI
A & LIX Paris) as part of Proof Theory Virtual Seminar\n\n\nAbstract\nIn t
his talk I will explore the relationship between combinatorial proofs for
first-order logic and a deep inference proof system for first-order logic.
In particular\, I will discuss the decomposition of a proof into a linear
part and a resource management part. Based on this\, I will argue that co
mbinatorial proofs can serve as way to define a universal notion of proof
identity.
\nThis talk is based on a joint work with Dominic Hughes and
Jui-Hsuan Wu (to be presented at LICS 2021).\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jeremy Avigad
DTSTART:20211006T170000Z
DTEND:20211006T180000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/18
DESCRIPTION:Title: The conservativity of weak König's lemma (a proof from the book)\
nby Jeremy Avigad as part of Proof Theory Virtual Seminar\n\n\nAbstract\nA
celebrated result by Harvey Friedman is that WKL$_0$\, a subsystem of sec
ond-order arithmetic based on Weak König's Lemma\, is conservative over p
rimitive recursive arithmetic (aka PRA) for $\\Pi_2$ sentences. Leo Harrin
gton showed that it is conservative over RCA$_0$ for $\\Pi^1_1$ sentences\
, from which Friedman's result follows. It is known that in the worst case
there is an iterated exponential increase in length when translating proo
fs from RCA$_0$ to PRA\, and hence from WKL$_0$ to PRA. But Hajek and I in
dependently showed that proofs can be translated from WKL$_0$ to RCA$_0$ w
ithout a dramatic increase in length. In this talk\, I'll sketch the relev
ant background and present the nicest proof of this last result that I kno
w of.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fedor Pakhomov
DTSTART:20211020T090000Z
DTEND:20211020T100000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/19
DESCRIPTION:Title: Fast growing hierarchies\, ordinal collapsing\, and Π¹₁-CA₀\
nby Fedor Pakhomov as part of Proof Theory Virtual Seminar\n\n\nAbstract\n
This is a joint work with Juan Pablo Aguilera and Andreas Weiermann. \n\nW
eakly finite dilators are functions F from naturals to naturals for which
we have a fixed extension to a dilator F:On->On. We show that for a large
class of natural ordinal notation systems α the fast growing function F_
α naturally could be treated as a weakly finite dilator. More precisely o
ur construction works when α=D(ω)\, for a weakly finite dilator D. Thus
we have an operator that maps a weakly finite dilator D to the weakly fini
te dilator F_{D(ω)}. We show that F_{D(ω)} could be naturally identified
with the ordinal denotation system based on a variant of collapsing funct
ion ψ\, collapsing D(Ω). We show that the fact that this operator maps w
eakly finite dilators to weakly finite dilators is equivalent to Π¹₁-C
A₀.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wilfried Sieg
DTSTART:20211103T170000Z
DTEND:20211103T180000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/20
DESCRIPTION:Title: Proofs as objects\nby Wilfried Sieg as part of Proof Theory Virtua
l Seminar\n\n\nAbstract\nIn his recently discovered Twenty-Fourth Problem\
, Hilbert suggested \ninvestigating mathematical proofs and called in 1918
for a “theory of the specifically \nmathematical proof”. Gentzen ins
isted in 1936 that “the objects of proof theory shall be \nthe proofs ca
rried out in mathematics proper”. He viewed derivations in his natural
\ndeduction calculi as “formal images [Abbilder]” of such proofs. Cle
arly\, these formal \nimages were to represent significant structural feat
ures of the proofs from ordinary \nmathematical practice. The thorough for
malization of mathematics encouraged in Mac \nLane the idea that formal de
rivations could be the starting-points for a theory of \nmathematical proo
fs.
\nThese ideas for a theory of mathematical proofs have been reawake
ned by a \nconfluence of investigations on natural reasoning (in the tradi
tion of Gentzen and \nPrawitz)\, interactive verifications of theorems\, a
nd implementations of mechanisms that \nsearch for proofs. At this interse
ction of proof theory with interactive and automated \nproof construction\
, one finds a promising avenue for exploring the structure of \nmathematic
al proofs. I will detail steps down this avenue: the formal representation
of \nproofs in appropriate logical frames is akin to the representation o
f physical phenomena \nin mathematical theories\; an important dynamic asp
ect is captured through the \narticulation of bi-directional and strategic
ally guided procedures for constructing \n(normal) proofs.
\n \nRef
erences.
\nGentzen G (1936) Die Widerspruchsfreiheit der reinen Zahlent
heorie. Mathematische Annalen 112(1): \n493-565.
\nHilbert D (1918) Axi
omatisches Denken. Mathematische Annalen 78:405-415.
\nMac Lane S (1934
) Abgekürzte Beweise im Logikkalkul. Dissertation\, Georg-August-Universi
tät \nGöttingen.
\nMac Lane S (1935) A logical analysis of mathematic
al structure. The Monist 45(1):118-130.
\nThiele R (2003) Hilbert's tw
enty-fourth problem. The American Mathematical Monthly 110(1):1-24.\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alexis Saurin
DTSTART:20211117T090000Z
DTEND:20211117T100000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/21
DESCRIPTION:by Alexis Saurin as part of Proof Theory Virtual Seminar\n\nAb
stract: TBA\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alessio Guglielmi
DTSTART:20211215T090000Z
DTEND:20211215T100000Z
DTSTAMP:20260315T024457Z
UID:PT-Seminar/22
DESCRIPTION:by Alessio Guglielmi as part of Proof Theory Virtual Seminar\n
\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/PT-Seminar/22/
END:VEVENT
END:VCALENDAR