Title: Inversion results and base-completeness for two approaches to proof-theoretic validity
The name “proof-theoretic semantics” (PTS) indicates a family of constructive semantics where meaning and validity are explained in terms of the notion of proof. The meaning of the non-logical vocabulary is fixed through sets of rules governing deduction at the atomic level, called “atomic bases”.
PTS stems from Prawitz’s normalisation theorems for Gentzen’s Natural Deduction. In the original formulation, due to Prawitz himself, proofs are conceived of in terms of inferential structures equipped with reduction functions for removing maximal steps of generalised elimination rules. I shall indicate this variant with the expression “reducibility semantics”. In a more recent approach, inferential structures are left aside, and PTS is understood as a theory of consequence for formulas over atomic bases. This variant of PTS is nowadays referred to as “base(-extension)-semantics”.
Both reducibility semantics and base-semantics are expected to be semantics for intuitionistic, or at least constructive logics, and many completeness or incompleteness results for these logics have been obtained so far.
In my talk, I prove some general results on the relation between reducibility semantics and base-semantics which, when suitable conditions are met, permit one to shift from one approach to the other. From these results I then draw some consequences, relative to the issue of completeness of (recursive) logical systems. This will finally lead me to focus on a notion of base-completeness, which, to conclude, I discuss with reference to known (in)completeness results for intuitionistic logic.
The talk will be online; people are welcome to join us physically at FMI Hall 214 “Google”.
Google Meet link: https://meet.google.com/ack-sxkj-xyj