https://lawrencecpaulson.github.io/2022/07/13/Isabelle_influences.html

[utterances-bot]

How Isabelle emerged from the trends of the 1980s

https://lawrencecpaulson.github.io/2022/07/13/Isabelle_influences.html

[phlegmaticprogrammer]

I am confused, doesn't Isabelle clearly show that Natural Deduction is just a special case of a Hilbert style axiomatic system? I never understood why people make such a big deal out of natural deduction. I like the simple form of natural deduction written as axioms, but they are just axioms, nevertheless.

Edit: Thinking about this a little bit longer, you DO need natural deduction to set up Isabelle's metalogic M. Abstraction Logic (AL) (https://arxiv.org/abs/2207.05610) instead is Hilbert-style from the ground up, and natural deduction appears just in form of some of the axioms. Of course, the ability to consider context locally, and to be able to transfer axioms/theorems between contexts, is essential: This is why the axioms in AL's "deduction logic" look like they do.

[lawrencecpaulson]

The crucial innovation of natural deduction is the idea of a local context of assumptions and (in effect) bound variables. The advantages over a Hilbert system are not simply a matter of style. If we look at the system given on Wikipedia, a standard one, derivations can be exponentially longer than proofs of the same theorems in a natural deduction system. The proofs in the Wikipedia article speak for themselves.

[phlegmaticprogrammer]

But in practice everybody uses the deduction theorem for Hilbert systems to get proofs that are as short as natural deduction. Abstraction logic has a deduction theorem for both local variables and local assumptions. So would you say then that (Hilbert system) + (metarule for applying deduction theorem(s) in one step) = (Natural Deduction) ? Note that this equation then also clearly states that every rule corresponding to one symbol is not really relevant for something to be called natural deduction.

Edit: Above equation doesn't make sense as Natural Deduction has already a fixed meaning, I guess. What I really want to express is more like this: If we set D = (Hilbert system) + (metarule for applying deduction theorem(s) in one step), then D covers all uses cases of natural deduction.

[lawrencecpaulson]

If your setup allows you to derive a natural deduction system from a Hilbert system, that's fine. Something like that happens in my formalisation of the incompleteness theorems.