Logic List Mailing Archive

Announcement: ExtenDD Seminar Series

Comment by the Moderator of the LOGIC List:
The list does only announce the announcement of a new series
or the re-announcement of an annual series and not all their talks.
So to keep being informed you need to subscribe to their list
(See below)

***

Dear List Members,


the next instalment of the ExtenDD Seminar Series is starting again next we
ek with a talk by PI Andrzej Indrzejczak:

09/10/24 Andrzej Indrzejczak: Strict form of stratified set theories NF and
 NFU in the setting of sequent calculus

Abstract: Quine's NF provides original approach to set theory based on stra
tified form of Comprehension Axiom, which may be seen as a liberalization o
f simple type theory. NFU (NF with urelements), the weaker form of NF propo
sed by Jensen, was proved to be consistent, in contrast to NF for which thi
s question is still open. So far, with the exception of Crabbe's work on NF
 without extensionality, these theories were not investigated in the settin
g of proof theory. We propose a stricter form of both theories, where set a
bstracts can be formed only from stratified formulae. It seems that this re
striction saves the essential features of NF and NFU but make them more acc
urate for proof-theoretic investigation. Two sequent calculi GSNF, GSNFU fo
r both theories are provided which are cut free, moreover, cut elimination 
yields strictly syntactical proof of consistency for GSNFU. Both theories c
an be also formulated on the intuitionistic basis still satisfying the resu
lts which hold for their classical variant.


The rest of the schedule for this semester is the following:

23/10/24 Bartosz Wieckowski: Incomplete descriptions and qualified definite
ness

06/11/24 tbc

20/11/24 Matthieu Fontaine: Abstract Artefacts in a Modal Framework

04/12/24 tbc

18/12/24 Elaine Pimentel: From axioms to synthetic inference rules via focu
sing

08/01/25 Christoph Benzmller: Utilizing proof assistant systems and the 
LogiKEy methodology for experiments on free logic in HOL

22/01/25 Ji Raclavsk: tba

If you wish to participate, please email Yaroslav Petrukhin (yaroslav.petru
khin@gmail.com<mailto:yaroslav.petrukhin@gmail.com>) to register your inter
est. You'll then receive a link to the Teams Meeting and regular updates on
 the seminar series.

The seminar Series is part of Prof. Andrzej Indrzejczak's ERC Advanced Gran
t ExtenDD: Coming to Terms (project number: 101054714) held at the Universi
ty of Lodz, Poland, on the proof theory of definite descriptions and other 
term forming operators. Additional Information is here https://www.uni.lodz
.pl/extendd and in the PS below.

Very best wishes,

Nils

PS. Some more information about the Project ExtenDD

The project is concerned with two areas which so far have rarely come toget
her: complex terms and proof theory. ExtenDD focuses on definite descriptio
ns as the most important and troublesome singular terms and on sequent calc
ulus and its generalisations as the most important tools of modern proof th
eory.
Since Russell's 'On Denoting', regarded as a paradigm of analytic philosoph
y, definite descriptions occupy a central place in philosophical research a
nd many deep and detailed studies have been carried out. The second half of
 the 20th century saw the development of new approaches to this phenomenon 
based on non-classical logics, in particular free logic in which, contrary 
to Frege's and Russell's classical logic, it is not assumed that every term
 refers. Yet despite the long history of research into definite description
s, a paradigm of formal logic has so far rarely been applied to them: proof
 theory. The methods developed by Gentzen, in particular those relating to 
his sequent calculus, provide the means for the deepest study of proofs and
 their properties. Yet only a small effort has so far been put into the ade
quate treatment of definite descriptions in this framework. The same counts
 for other complex singular terms such as set abstracts and number operator
s. ExtenDD fills this important gap in research.
Applying the methods of proof theory to definite descriptions is profitable
 to both sides. Competing theories of definite descriptions and complex ter
ms in general, their advantages and shortcomings, are shown in a new light.
 The behaviour of complex terms needs subtle syntactical analysis and requi
res enriching the toolkit of proof theory. ExtenDD deals with both challeng
es: it develops formal theories of definite descriptions and modifies the m
achinery of proof theory to cover new areas of application. The realisation
 of ExtenDD affects significantly the field of proof theory, automated dedu
ction and philosophy of language.
--
[LOGIC] mailing list, provided by DLMPST
More information (including information about subscription management) can
be found here: http://dlmpst.org/pages/logic-list.php