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 consisten cy or conservation proofs. Indeed\, one may see that forcing is a generali zation of a relative interpretation by means of the Kripke semantics.
\n \n
Moreover\, such an interpretation usually provides a feasible (polyn omial) proof transformation as digested in [2]. In this talk\, we will ove rview such ideas and show that many conservation theorems for systems of s econd-order arithmetic can be converted to non-speedup theorems.
\n \n[1
] J. Avigad\, Forcing in proof theory. Bull. Symbolic Logic 10 (2004)\, no
. 3\, 305-333.
\n[2] J. Avigad\, Formalizing forcing arguments in subsy
stems of second-order arithmetic. Ann. Pure Appl. Logic 82 (1996)\, no. 2\
, 165-191.
\n[3] L. A. Kolodziejczyk\, T. L. Wong and K. Yokoyama\, Ram
sey's theorem for pairs\, collection\, and proof size\, submitted.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dale Miller (Inria & IP Paris)
DTSTART:20210303T170000Z
DTEND:20210303T180000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/10
DESCRIPTION:Title: Focusing Gentzen's LK proof system\nby Dale Miller (Inria &
IP Paris) as part of Proof Theory Virtual Seminar\n\n\nAbstract\nGentzen'
s sequent calculi LK and LJ are landmark proof systems. They identify the
structural rules of weakening and contraction as notable inference rules\,
and they allow for an elegant statement and proof of both cut-elimination
and consistency for classical and intuitionistic logics. Among the undesi
rable features of those sequent calculi is the fact that their inferences
rules are very low-level and that they frequently permute over each other.
As a result\, large-scale structures within sequent calculus proofs are h
ard to identify. In this paper\, we present a different approach to design
ing a sequent calculus for classical logic. Starting with Gentzen's LK pro
of system\, we first examine the proof search meaning of his inference rul
es and classify those rules as involving either don't care nondeterminism
or don't know nondeterminism. Based on that classification\, we design the
focused proof system LKF in which inference rules belong to one of two ph
ases of proof construction depending on which flavor of nondeterminism the
y involve. We then prove that the cut-rule and the general form of the ini
tial rule are admissible in LKF. Finally\, by showing that the rules of in
ference for LK are all admissible in LKF\, we can give a completeness proo
f for LKF provability with respect to LK provability. We shall also apply
these properties of the LKF proof system to establish other meta-theoretic
properties of classical logic\, including Herbrand's theorem. This talk i
s based on a recent draft paper co-authored with Chuck Liang.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andreas Weiermann (Ghent)
DTSTART:20210317T090000Z
DTEND:20210317T100000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/11
DESCRIPTION:Title: Goodstein sequences and notation systems for natural numbers\nby Andreas Weiermann (Ghent) as part of Proof Theory Virtual Seminar\n\
n\nAbstract\nTermination theorems for Goodstein sequences provide canonica
l examples for the Gödel incompleteness of systems of arithmetic and set
theory. The original Goodstein sequence is based on canonical notations fo
r natural numbers using addition and exponentiation. In our exposition we
consider more general forms of notations which are based on the Ackermann
function and related functions and we use them to define Goodstein sequenc
es. The resulting termination theorems will be independent of relatively s
trong systems of arithmetic. We prove some general results about the notat
ion systems for natural numbers and try to explain how these results might
be connected to the problem of canonical well orderings and to comparison
theorems between the slow and fast growing hierarchies. The exposition is
aimed at a general audience.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Greg Restall (Melbourne)
DTSTART:20210421T090000Z
DTEND:20210421T100000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/12
DESCRIPTION:Title: Comparing Rules for Identity in Sequent Systems and Natural Ded
uction\nby Greg Restall (Melbourne) as part of Proof Theory Virtual Se
minar\n\n\nAbstract\nIt is straightforward to treat the identity predicate
in models for first order predicate logic. Truth conditions for identity
formulas are straightforward. On the other hand\, finding appropriate rule
s for identity in a sequent system or in natural deduction leaves many que
stions open. Identity could be treated with introduction and elimination r
ules in natural deduction\, or left and right rules\, in a sequent calculu
s\, as is standard for familiar logical concepts. On the other hand\, sinc
e identity is a predicate and identity formulas are atomic\, it is possibl
e to treat identity by way of axiomatic sequents\, rather than inference r
ules. In this talk\, I will describe this phenomenon\, and explore the rel
ationships between different formulations of rules for the identity predic
ate\, and attempt to account for some of the distinctive virtues of each d
ifferent formulation.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Antonina Kolokolova (Newfoundland)
DTSTART:20210630T170000Z
DTEND:20210630T180000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/14
DESCRIPTION:Title: Learning from Bounded Arithmetic\nby Antonina Kolokolova (N
ewfoundland) as part of Proof Theory Virtual Seminar\n\n\nAbstract\nThe ce
ntral question of complexity theory -- what can (and cannot) be feasibly c
omputed -- has a corresponding logical meta-question: what can (and cannot
) be feasibly proven. While complexity theory studies the former\, bounded
arithmetic is one of the main approaches to the meta-question. There is a
tight relation between theories of bounded arithmetic and corresponding c
omplexity classes\, allowing one to study what can be proven in\, for exam
ple\, "polynomial-time reasoning" and what power is needed to resolve comp
lexity questions\, with a number of both positive and negative provability
results.
\n \nHere\, we focus on the complexity of another meta-pr
oblem: learning to solve problems such as Boolean satisfiability. There is
a range of ways to define "solving problems"\, with one extreme\, the uni
form setting\, being an existence of a fast algorithm (potentially randomi
zed)\, and another of a potentially non-computable family of small Boolean
circuits\, one for each problem size. The complexity of learning can be r
ecast as the complexity of finding a procedure to generate Boolean circuit
s solving the problem of a given size\, if it (and such a family of circui
ts) exists.
\n \nFirst\, inspired by the KPT witnessing theorem\, a
special case of Herbrand's theorem in bounded arithmetic\, we develop an
intermediate notion of uniformity that we call LEARN-uniformity. While non
-uniform lower bounds are notoriously difficult\, we can prove several unc
onditional lower bounds for this weaker notion of uniformity. Then\, retur
ning to the world of bounded arithmetic and using that notion of uniformit
y as a tool\, we show unprovability of several complexity upper bounds for
both deterministic and randomized complexity classes\, in particular givi
ng simpler proofs that the theory of polynomial-time reasoning PV does not
prove that all of P is computable by circuits of a specific polynomial si
ze\, and 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 trouble differentiating" between uniform and non-uniform frameworks:
more specifically\, we show that theories for polynomial-time and randomi
zed polynomial-time reasoning cannot prove both a uniform lower bound and
a non-uniform upper bound for NP. In particular\, while it is possible tha
t NP!=P yet all of NP is computable by families of polynomial-size circuit
s\, this cannot be proven feasibly.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Revantha Ramanayake (Groningen)
DTSTART:20210505T170000Z
DTEND:20210505T180000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/15
DESCRIPTION:Title: Up and Down the Lambek Calculus\nby Revantha Ramanayake (Gr
oningen) as part of Proof Theory Virtual Seminar\n\n\nAbstract\nI will pre
sent recent results using proof theory that establish decidability and com
plexity for many substructural logics. Specifically: for infinitely many a
xiomatic extensions of the commutative Full Lambek calculus with contracti
on/weakening\, including the prominent fuzzy logic MTL. This work can be s
een as extending Kripke’s decidability argument for FLec (1959). I aim t
o isolate some of the proof-theoretic motifs that feature in this type of
work. These include: refinement of backward and forward proof search\, cut
-free proof systems via structural rule extension\, absorption of contract
ion rules\, and upper bounding proof search via controlled bad sequences.\
n \nJoint work with A.R. Balasubramanian and Timo Lang.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hugo Herbelin (INRIA Paris)
DTSTART:20210616T090000Z
DTEND:20210616T100000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/16
DESCRIPTION:Title: On the logical structure of choice and bar induction principles
\nby Hugo Herbelin (INRIA Paris) as part of Proof Theory Virtual Semin
ar\n\n\nAbstract\nWe present an alternative equivalent generalised formula
tion GDC(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-approximability 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
theorem
\n- GDC(ℕ\,Bool\,T) reduces to their common intersection\, n
amely essentially weak König's lemma
\n- GDC(A\,B\,R⁺)\, for R⁺ so
me specific filtering predicate defined from a relation R on A and B\, is
the statement of the general axiom of choice
\n \nIts syntactic con
trapositive GBI(A\,B\,T) "T is barred implies T is inductively barred" is
such that:
\n \n- GBI(ℕ\,B\,T) is essentially bar induction\, and
close also to countable Zorn's lemma
\n- GBI(A\,Bool\,T) is essentiall
y the statement of Tarski completeness theorem in the form validity implie
s provability for Scott's entailment relations
\n- GBI(ℕ\,Bool\,T) re
duces to their common intersection\, namely essentially the weak fan theor
em
\n \nWe will also present further explorations aiming at integra
ting the full version of Zorn's lemma in the picture. Note that all equiva
lences will be considered under the eyes both of constructive and linear l
ogic.
\n \nThis is joint work with Nuria Brede.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lutz Straßburger (INRIA & LIX Paris)
DTSTART:20210602T170000Z
DTEND:20210602T180000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/17
DESCRIPTION:Title: Towards a Combinatorial Proof Identity\nby Lutz Straßburge
r (INRIA & LIX Paris) as part of Proof Theory Virtual Seminar\n\n\nAbstrac
t\nIn this talk I will explore the relationship between combinatorial proo
fs 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 combinatorial proofs can serve as way to define a universal notion of
proof identity.
\nThis talk is based on a joint work with Dominic Hugh
es and Jui-Hsuan Wu (to be presented at LICS 2021).\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jeremy Avigad
DTSTART:20211006T170000Z
DTEND:20211006T180000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/18
DESCRIPTION:Title: The conservativity of weak König's lemma (a proof from the boo
k)\nby Jeremy Avigad as part of Proof Theory Virtual Seminar\n\n\nAbst
ract\nA celebrated result by Harvey Friedman is that WKL$_0$\, a subsystem
of second-order arithmetic based on Weak König's Lemma\, is conservative
over primitive recursive arithmetic (aka PRA) for $\\Pi_2$ sentences. Leo
Harrington showed that it is conservative over RCA$_0$ for $\\Pi^1_1$ sen
tences\, from which Friedman's result follows. It is known that in the wor
st case there is an iterated exponential increase in length when translati
ng proofs from RCA$_0$ to PRA\, and hence from WKL$_0$ to PRA. But Hajek a
nd I independently showed that proofs can be translated from WKL$_0$ to RC
A$_0$ without a dramatic increase in length. In this talk\, I'll sketch th
e relevant background and present the nicest proof of this last result tha
t I know of.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fedor Pakhomov
DTSTART:20211020T090000Z
DTEND:20211020T100000Z
DTSTAMP:20260404T111244Z
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\nAb
stract\nThis is a joint work with Juan Pablo Aguilera and Andreas Weierman
n. \n\nWeakly finite dilators are functions F from naturals to naturals fo
r 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 fun
ction F_α naturally could be treated as a weakly finite dilator. More pre
cisely our construction works when α=D(ω)\, for a weakly finite dilator
D. Thus we have an operator that maps a weakly finite dilator D to the wea
kly finite dilator F_{D(ω)}. We show that F_{D(ω)} could be naturally id
entified with the ordinal denotation system based on a variant of collapsi
ng function ψ\, collapsing D(Ω). We show that the fact that this operato
r maps weakly finite dilators to weakly finite dilators is equivalent to
Π¹₁-CA₀.\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wilfried Sieg
DTSTART:20211103T170000Z
DTEND:20211103T180000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/20
DESCRIPTION:Title: Proofs as objects\nby Wilfried Sieg as part of Proof Theory
Virtual Seminar\n\n\nAbstract\nIn his recently discovered Twenty-Fourth P
roblem\, Hilbert suggested \ninvestigating mathematical proofs and called
in 1918 for a “theory of the specifically \nmathematical proof”. Gent
zen insisted in 1936 that “the objects of proof theory shall be \nthe pr
oofs carried out in mathematics proper”. He viewed derivations in his n
atural \ndeduction calculi as “formal images [Abbilder]” of such proof
s. Clearly\, these formal \nimages were to represent significant structur
al features of the proofs from ordinary \nmathematical practice. The thoro
ugh formalization of mathematics encouraged in Mac \nLane the idea that fo
rmal derivations could be the starting-points for a theory of \nmathematic
al proofs.
\nThese ideas for a theory of mathematical proofs have been
reawakened by a \nconfluence of investigations on natural reasoning (in th
e tradition of Gentzen and \nPrawitz)\, interactive verifications of theor
ems\, and implementations of mechanisms that \nsearch for proofs. At this
intersection of proof theory with interactive and automated \nproof constr
uction\, one finds a promising avenue for exploring the structure of \nmat
hematical proofs. I will detail steps down this avenue: the formal represe
ntation of \nproofs in appropriate logical frames is akin to the represent
ation of physical phenomena \nin mathematical theories\; an important dyna
mic aspect is captured through the \narticulation of bi-directional and st
rategically guided procedures for constructing \n(normal) proofs.
\
n \nReferences.
\nGentzen G (1936) Die Widerspruchsfreiheit der reinen
Zahlentheorie. Mathematische Annalen 112(1): \n493-565.
\nHilbert D (19
18) Axiomatisches Denken. Mathematische Annalen 78:405-415.
\nMac Lane
S (1934) Abgekürzte Beweise im Logikkalkul. Dissertation\, Georg-August-U
niversität \nGöttingen.
\nMac Lane S (1935) A logical analysis of mat
hematical structure. The Monist 45(1):118-130.
\nThiele R (2003) Hilbe
rt's twenty-fourth problem. The American Mathematical Monthly 110(1):1-24.
\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alexis Saurin
DTSTART:20211117T090000Z
DTEND:20211117T100000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/21
DESCRIPTION:by Alexis Saurin as part of Proof Theory Virtual Seminar\n\nAb
stract: TBA\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alessio Guglielmi
DTSTART:20211215T090000Z
DTEND:20211215T100000Z
DTSTAMP:20260404T111244Z
UID:PT-Seminar/22
DESCRIPTION:by Alessio Guglielmi as part of Proof Theory Virtual Seminar\n
\nAbstract: TBA\n
LOCATION:https://stable.researchseminars.org/talk/PT-Seminar/22/
END:VEVENT
END:VCALENDAR