ProofTheory

Popper’s chapter asks whether a conclusion follows from some premises. This chapter asks what the deduction itself is, and when it can be checked.

A proof system fixes a collection of rules. The deductions it allows are the finite trees built from those rules, and its deducibility relation is read off from them: a conclusion follows from some premises exactly when such a tree exists. Every proof system is a basis in Popper’s sense, so nothing established there has to be established again.

Most rules do not care which premises are at hand: they say what each branch may assume on top of them, and leave the rest alone. Such a rule is a schema, standing for one rule per list of premises. Where all the rules are schemata, deductions never need to paste anything: whatever pasting achieves, the rules achieve directly.

Sources: Hiep, New Foundations for Separation Logic (PhD thesis, 2024), appendix A.3; Grabmayer, Relating Proof Systems for Recursive Types (PhD thesis, Vrije Universiteit Amsterdam, 2005), chapter 4.