Proof systems for institutional logic (abstract)
- Institutions with proof-theoretic structure, here called
`institutions with proofs', introduced by What is a Logic?,
provide a complete formal notion for the intuitive notion of
logic, including both the model and the proof theoretic
sides.
This paper introduces a concept of proof rules for institutions and
argues that the proof systems of the actual institutions with proofs
are freely generated by their presentations as systems of proof
rules.
We also show that proof-theoretic quantification, an institutional
refinement of the (meta-)rule of Generalization from classical logic,
can also be added freely to any proof system.
By applying these universal properties, we are able to provide some
general compactness results for proof systems and some general
soundness results for institutions with proofs.
We also discuss several open problems and further research directions.
back to Selected Publications