Email Gateway (Aug 22 2022 at 12:25): Email Gateway (Aug 22 2022 at 12:25):From: Joachim Breitner <breitner@kit.edu>
Dear List,
I’m searching for a formal description of natural deduction, preferably
formalized in Isabelle.
What I found was for example this theory
https://github.com/logic-tools/nadea/blob/master/Isabelle/NaDeA.thy
(part of https://nadea.compute.dtu.dk/ by Jørgen Villadsen)
but it hard-codes the terms and inference rules; I’m interested in
something more general, where the terms (or at least the connectives)
are abstract, and also the set of inference rules is not fixed.
In other words: I’m looking for a data type that can describe arbitrary
terms (with binders), inference rules and derivation tree using them,
and can determine whether the derivation tree is valid (terms match,
only the given inference rules are used, scoping of variables is
correct).
Do you know of such a thing?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 12:26):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Joachim,
here are some related references (none of which has all you need):
Similar to Jørgen Villadsen’s theory it hard-codes formulas and natural deduction inference rules. It has a notion of valid trees and used de Bruijn indices for variables. The entry proves soundness and completeness of FOL.
Another formalization of FOL soundness and completeness (+Löwenheim-Skolem) for a natural deduction calculus. No derivation trees though (Stefan follows a semantic approach, which does not require them).
This one has abstract (syntax-independent) notions of valid proof trees. It aims at formulating the completeness property as abstractly as possible. (The journal version also shows abstract soundness for classic FOL and extensions; the archive attachment
http://people.inf.ethz.ch/trayteld/compl-journal-devel.tgz <http://people.inf.ethz.ch/trayteld/compl-journal-devel.tgz> contains the formalizations of these extensions). In the AFP there is only a toy instantiation of the abstract machinery with propositional logic.
There is also a sophisticated instantiation with many-sorted FOL by and a natural deduction proof system Andrei and Jasmin (for their Mechanization of Sledgehammer’s metatheory) that uses Andrei’s theory of Syntax with Bindings. All of this is not in the AFP but available separately, http://www21.in.tum.de/~traytel/compl_devel.zip <http://www21.in.tum.de/~traytel/compl_devel.zip>, tested with Isabelle2013-2 ;-) ; see readme.txt there.
It has the most developed formalization of first-order terms (including matching, unification, and what not).
Formalizes logical calculi (ongoing work, so far with a focus on resolution and superposition, not so much on natural deduction).
I’m not sure what your precise application is (formalization of the incredible proof machine?, what do you want to prove there?). If you aim for soundness and completeness, building on top of 3 and 4 might be a way to go.
Hope that helps,
Dmitriy
Email Gateway (Aug 22 2022 at 12:26):From: Joachim Breitner <breitner@kit.edu>
Hi,
thanks for the overview, especially for the comments!
good guess :-)
I want to show that proof graphs, as they are used by the Incredible
Proof Machines, correspond to “normal” natural deduction trees, by
giving a mapping from proof blocks to inference rules and from graphs
to derivation trees, and at least show soundness, preferably also
completeness.
Greetings,
Joachim
signature.asc
Last updated: May 06 2024 at 12:29 UTC