Small Workshop on PTS - CFvW Center, University of Tübingen

[antpic...@gmail.com]

Dear all,

A small workshop on proof-theoretic semantics will take place at the Carl Friedrich von Weizsäcker Center of the University of Tübingen from 10 am to 1 pm, September 10th. The event is part of the activities of the Carl Friedrich von Weizsäcker Colloquium, organised by Reinhard Kahle and Thomas Piecha, as well as of the WIP Seminar, organised by Balthasar Grabmayr. It will consist of two talks:

• Ryo Takemura (Nihon University)
  
  Title - A completeness theorem in proof-theoretic semantics
  
  Abstract - We investigate the completeness of intuitionistic propositional logic with respect to Prawitz's proof-theoretic validity. By developing the phase semantics with proof-terms introduced by Okada & Takemura (2007), we construct a special phase model whose domain consists solely of closed terms. Building on the correspondence between this special phase model and proof-theoretic semantics, we prove the completeness of intuitionistic propositional logic with respect to non-monotonic elimination-based proof-theoretic semantics. We further discuss some possible extensions of our results.
  
  
• Antonio Piccolomini d'Aragona (University of Tübingen)
  
  Title - Uniform incompleteness in proof-theoretic semantics: consistent bases and weakly classical meta-logic
  
  Abstract -  I prove incompleteness of intuitionistic logic over monotonic and non-monotonic proof-theoretic validity (mPtV and nPtV), two kinds of proof-theoretic semantics due to Dag Prawitz. Although intuitionistic logic is already known to be incomplete over both these frameworks (Piccolomini d'Aragona 2026, Piccolomini d'Aragona & Prawitz 2026), I will provide proofs that refine the existing ones in two ways. First, the proof for mPtV has a requirement of consistency on atomic bases - while the proof of (Piccolomini d'Aragona 2026) works only if atomic bases are allowed to be inconsistent (while containing all the atomic instances of ex falso). This is important since, as highlighted by (Barroso-Nascimento, Pereira & Pimentel 2025), the requirement of consistency on atomic bases seems to play a relevant role in monotonic approaches to PTS. Second, the proof for nPtV uses a less than classical (but still non-constructive) meta-logic - while the proof of (Piccolomini d'Aragona & Prawitz 2026) uses excluded middle in the meta-language. This is important since, although a classical proof of incompleteness is enough for ruling out the existence of a constructive proof of completeness, finding a constructive proof of incompleteness would be valuable, so a proof whose meta-logic is less than classical might be looked at as an improvement towards this goal.

For further information, visit this link. Remote attendance is available by using this link.

Best
Antonio Piccolomini d'Aragona