On Sets of Premises

TL;DR

This paper explores the implications of viewing premises as sets or multisets rather than sequences in proof theory, revealing potential triviality issues and analyzing categorical proof structures related to conjunction.

Contribution

It introduces a categorical perspective on premises as sets or multisets, highlighting how this affects the identity of deductions in proof theory.

Findings

Premises as sets lead to triviality in proof identity.

Categorical analysis links premises to adjunctions involving conjunction.

Implications for classical and intuitionistic logic proof structures.

Abstract

Conceiving of premises as collected into sets or multisets, instead of sequences, may lead to triviality for classical and intuitionistic logic in general proof theory, where we investigate identity of deductions. Any two deductions with the same premises and the same conclusions become equal. In terms of categorial proof theory, this is a consequence of a simple fact concerning adjunction with a full and faithful functor applied to the adjunction between the diagonal functor and the product biendofunctor, which corresponds to the conjunction connective.