We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for rst-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry \First-Order Logic According to Fitting" by Berghofer in the Archive of Formal Proofs (AFP). The calculi and proof techniques are taken from Ben-Ari's textbook Mathematical Logic for Computer Science (Springer 2012). We thereby demonstrate that Berghofer's approach works not only for natural deduction but constitutes a framework for mechanically-checked completeness proofs for a range of proof systems.
We formalize in the proof assistant Isabelle/HOL [
IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL.
At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools.
Along with the resolution calculus, the sequent calculus is a central topic in automated reasoning but we do not present an automatic prover. We follow the soundness and completeness proofs in the textbook on mathematical logic ? Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
by Ben-Ari [
In recent years we have used our formalization for teaching logic in computer science and described this use in a number of papers [11{13]. These report on teaching logic for hundreds of students but this is not the topic of our present paper. Also, these papers focus on derivations in the sequent calculus and how Isabelle/HOL veri es these derivations of rst-order formulas. That is, unlike the present paper, none of these papers detail the formalization of the soundness and completeness proofs for the sequent calculus or the tableau calculus.
We nd that for teaching, the one-sided sequent calculus is a good starting point, especially if the students have previously worked with tableau calculi; the traditional two-sided sequent calculus can be covered afterwards if necessary. Without a formalization, students and researchers have to manually recheck the soundness and completeness proofs if they experiment with adding or removing rules of the calculus. With our work, they can instead let Isabelle/HOL show which proofs need to be changed in order to account for the new set of rules and use Isabelle/HOL to help them with updating these proofs.
Our formalization approach is slightly unusual in that we have started from
the formalization of natural deduction by Berghofer (4000+ lines) [
We start by discussing related work on formalizing sequent calculi in Section 2. Then we brie y review Berghofer's formalization of natural deduction in Section 3 and our extension to open formulas in Section 4. In Section 5 we prove soundness and completeness of our tableau calculus and continue with open formulas in Section 6. We prove soundness and completeness of our sequent calculus in Section 7, using the completeness result for our tableau calculus. Lastly, we conclude with thoughts about future work in Section 8. 2
There are other formalizations of sequent calculi in proof assistants, all of which di er from the one we present. We discuss them here.
One is in the supplementary work of a paper by Blanchette and Popescu [
Another formalization of a sequent calculus is by Ridge and Margetson [
Braselmann and Koepke [
A more exotic result is Ilik's formalization [
Our point of departure is Berghofer's formalization of natural deduction [
Our formalization uses the same de nition of rst-order logic's syntax and semantics, and we also use the model existence theorem to prove completeness. We therefore brie y review Berghofer's formalization in this section. 3.1
Berghofer formalizes terms using a simple datatype with one constructor, Var, for variables and one, App, for composite terms: datatype 0a term = Var nat j App 0a h 0a term list i Variables are represented by natural numbers because Berghofer is using the so-called de Bruijn notation. In the de Bruijn notation the idea is that a variable Var i exists in the scope of a number of quanti ers. Of these quanti ers, Var i is bound by the one that has the ith innermost of these scopes, counting from 0. In case no such scope exists, the variable is considered free.
Berghofer formalizes formulas as a datatype: datatype ( 0a; 0b) form = FF j TT j Pred 0b h 0a term list i j And h( 0a; 0b) formi h( 0a; 0b) formi j Or h( 0a; 0b) formi h( 0a; 0b) formi j Impl h( 0a; 0b) formi h( 0a; 0b) formi j Neg h( 0a; 0b) formi j Forall h( 0a; 0b) formi j Exists h( 0a; 0b) formi FF represents ? (falsity), TT represents > (truth), Pred p ts represents the predicate p(ts1 ; : : : ; tsn ), And represents ^ (conjunction), Or represents _ (disjunction), Impl represents ! (implication), Neg represents : (negation), Forall represents 8 (universal quanti cation) and Exists represents 9 (existential quanti cation). Notice that the quanti ers contain a subformula but no explicit binding of a variable symbol { this is because with the de Bruijn notation an explicit binding would not be meaningful.
Berghofer de nes the semantics of terms and lists of terms by mutual recursion on these: primrec evalt :: h(nat ) 0c) ) ( 0a ) 0c list ) 0c) ) 0a term ) 0ci and evalts :: h(nat ) 0c) ) ( 0a ) 0c list ) 0c) ) 0a term list ) 0c list i where hevalt e f (Var n) = e ni j hevalt e f (App a ts) = f a (evalts e f ts)i j hevalts e f [] = []i j hevalts e f (t # ts) = evalt e f t # evalts e f tsi Here, e is a variable denotation and f is a function denotation.
Berghofer de nes the semantics of formulas by recursion on the formula datatype: primrec eval :: h(nat ) 0c) ) ( 0a ) 0c list ) 0c) ) ( 0b ) 0c list ) bool ) ) ( 0a; 0b) form ) bool i where heval e f g FF = Falsei j heval e f g TT = Truei j heval e f g (Pred a ts) = g a (evalts e f ts)i j heval e f g (And p q) = ((eval e f g p) ^ (eval e f g q))i j heval e f g (Or p q) = ((eval e f g p) _ (eval e f g q))i j heval e f g (Impl p q) = ((eval e f g p) ! (eval e f g q))i j heval e f g (Neg p) = (: (eval e f g p))i j heval e f g (Forall p) = (8 z : eval (eh0 :z i) f g p)i j heval e f g (Exists p) = (9 z : eval (eh0 :z i) f g p)i Here, e is a variable denotation, f is a function denotation and g is a predicate denotation. Since Berghofer is formalizing the object logic FOL in the metalogic HOL, he can use HOL's True, False, ^, _, !, :, 8 and 9 when de ning the semantics of FOL. The notation eh0 : zi represents the variable denotation f0 7! z; 1 7! e 0; 2 7! e 1; : : :g.
Berghofer also formalizes what it means for a formula p to be a consequence of a list of formulas ps with respect to a variable denotation, a function denotation and a predicate denotation: de nition model :: h(nat ) 0c) ) ( 0a ) 0c list ) 0c) ) ( 0b ) 0c list ) bool ) ) ( 0a; 0b) form list ) ( 0a; 0b) form ) bool i (-;-;-;- j= - [50 ;50 ] 50 ) where h(e;f ;g;ps j= p) = (list-all (eval e f g) ps ! eval e f g p)i 3.2
Berghofer formalizes a natural deduction system as an inductive predicate consisting of a number of rules. inductive deriv :: h( 0a; 0b) form list ) ( 0a; 0b) form ) bool i (- ` - [50 ;50 ] 50 ) where
Assum: ha 2 set G =) G ` ai j TTI : hG ` TT i j FFE : hG ` FF =) G ` ai j NegI : ha # G ` FF =) G ` Neg ai j NegE : hG ` Neg a =) G ` a =) G ` FF i j Class: hNeg a # G ` FF =) G ` ai j AndI : hG ` a =) G ` b =) G ` And a bi For example, the rule ForallI would be the following rule in a more conventional style for writing out proof rules: Here a[n=0] represents substitution of variable 0 with the constant (0-ary composite term) n in a. The rest of the rules are built in a similar way, so we will not write them out here. theorem correctness: hG ` p =) 8 e f g: e;f ;g;G j= pi The proof is by induction on the rules of the proof system. Berghofer's original proof was in apply-style, but the current version of the proof by From is an Isarstyle proof in which all cases are handled by the automation of Isabelle except for ForallI and ExistsE . However, these cases are not too di cult. 3.4
In order to prove model existence, Fitting and Berghofer rst de ne the notion
of what it means for a set of sets of formulas to be a consistency property:
de nition consistency :: h( 0a; 0b) form set set ) bool i where
hconsistency C = (8 S : S 2 C !
(8 p ts: : (Pred p ts 2 S ^ Neg (Pred p ts) 2 S )) ^
FF 2= S ^ Neg TT 2= S ^
(8 Z : Neg (Neg Z ) 2 S ! S [ fZ g 2 C ) ^
(8 A B : And A B 2 S ! S [ fA; B g 2 C ) ^
(8 A B : Neg (Or A B ) 2 S ! S [ fNeg A; Neg B g 2 C ) ^
(8 A B : Or A B 2 S ! S [ fAg 2 C _ S [ fB g 2 C ) ^
(8 A B : Neg (And A B ) 2 S ! S [ fNeg Ag 2 C _ S [ fNeg B g 2 C ) ^
(8 A B : Impl A B 2 S ! S [ fNeg Ag 2 C _ S [ fB g 2 C ) ^
(8 A B : Neg (Impl A B ) 2 S ! S [ fA; Neg B g 2 C ) ^
(8 P t : closedt 0 t ! Forall P 2 S ! S [ fP [t=0 ]g 2 C ) ^
(8 P t : closedt 0 t ! Neg (Exists P ) 2 S ! S [ fNeg (P [t =0 ])g 2 C ) ^
(8 P : Exists P 2 S ! (9 x : S [ fP [App x []=0 ]g 2 C )) ^
(8 P : Neg (Forall P ) 2 S ! (9 x : S [ fNeg (P [App x []=0 ])g 2 C )))i
Fitting and Berghofer's model existence theorem then states the following:
Theorem 1. If C is a consistency property, S 2 C,
has a model.
2 S and
is closed, then
We will not repeat the proof here, and instead refer to Berghofer [
Berghofer shows that the collection (set) of natural deduction consistent sets of formulas is a consistency property and he can therefore obtain the following model existence theorem for natural deduction in particular: Theorem 2. If S is a natural deduction consistent set, then there is a model for the closed formulas in S. 3.5
Proving completeness means showing that if q1; :::; qn j= p then q1; :::; qn ` p. In other words, if a conclusion follows logically from a set of premises then the conclusion can also be proved from the set of premises. Fitting's proof is by contraposition, i.e. he shows that if q1; :::; qn 6` p then q1; :::; qn 6j= p. He therefore assumes that q1; :::; qn 6` p, i.e. there is no natural deduction proof of the conclusion from the premises. Natural deduction allows proof by contradiction, so in particular there is no natural deduction proof by contradiction, i.e. we also know that q1; :::; qn; :p 6` ?. Thus, q1; :::; qn; :p is consistent with respect to natural deduction. The model existence theorem for natural deduction states that if a set of formulas is consistent with respect to natural deduction then it is satis able. We can therefore use it to conclude that natural deduction consistent formulas are satis able, and thus q1; :::; qn; :p has a model. That model is the evidence that q1; :::; qn 6j= p. This concludes the completeness proof by contraposition.
In the following we will see that as soon as we have shown that the model existence theorem can be applied to the tableau calculus then the above completeness argument can largely be repeated to prove the tableau calculus complete. 4
In this section we show how to extend a completeness result for sentences to one
for open formulas. We presented this technique at the Tenth Scandinavian Logic
Symposium in 2018 [
We illustrate the ve-step technique by showing the lemma that combines the steps. The result we prove is the following:
We assume that formula p is valid under assumptions z and want to derive z ` p.
1. We simplify the problem by turning the meta-level assumptions into objectlevel implications (put-imps p (rev z) builds the chain zn ! : : : ! z1 ! p): let ?p = hput-imps p (rev z )i
Importantly, this preserves validity: have : h8 (e :: nat ) nat hterm) f g: eval e f g ?pi
2. Next, we universally close the formula by pre xing it with a su cient number (m) of universal quanti ers and note that this too preserves validity: obtain m where : hclosed 0 (put-unis m ?p)i moreover have h8 (e :: nat ) nat hterm) f g: e; f ; g; [] j= put-unis m ?pi 3. The resulting formula is a valid sentence so we know from the existing completeness result that it can be derived: ultimately have h[] ` put-unis m ?pi
4. By working within the proof system we can then derive the open formula: then have h[] ` ?pi then show hz ` pi
5. And nally we use a deduction theorem to turn the introduced implications back into meta-level assumptions:
Steps 1 through 3 are not particularly di cult so we focus on steps 4 and 5. 4.1
We have a derivation of a formula with m universal quanti ers in front and want a derivation without them. We could use the Uni-E rule to substitute the original variables for the freshly quanti ed ones but this requires some tricky reasoning due to our use of de Bruijn indices. The following example starts from the formula 888p(0; 1; 2) and illustrates how the variables shift when eliminating the quanti ers: (88p(0; 1; 2))[2=0] 8((8p(0; 1; 2))[3=1]) (8p(0; 1; 4))[1=0]
To avoid having to reason about these shifts, we instead eliminate the universal quanti ers with fresh constants. The function subc c s p replaces occurrences of c with s in p, adjusting the variables in s when substituting under a quanti er. It is admissible to perform such a substitution uniformly across the formula and assumptions of a derivation: shows hz ` p =) subcs c s z ` subc c s pi
The proof goes by induction on the derivation and is mechanical, except for the quanti er rules where care must be taken to treat the involved constants correctly. The following renaming result is useful. Here psubst applies a function to every constant/function symbol: shows hz ` p =) map (psubst f ) z ` psubst f pi
When we compose closure elimination (sub) with constant substitution (subc) in the right order we get the following telescoping sequence of substitutions: subc c0 (m-1) (subc c1 (m-2) (. . . (subc cm 1 0 (sub 0 cm 1 . . . )))) Each introduced constant is immediately replaced by the correct variable and since subsequent substitutions are of constants, they do not adjust previously inserted variables. We can then prove our desired result: lemma remove-unis-sentence: assumes inf-params: hin nite ( params p)i
and hclosed 0 (put-unis m p)i h[] ` put-unis m pi shows h[] ` pi 4.2
Step 5 of our technique is to derive z ` p from [] ` put-imps p (rev z ). We do so with the following lemma, which shifts just one formula from an implication to the assumptions: assumes inf-params: hin nite (UNIV :: 0a set )i
and hz ` Impl p qi shows hp # z ` qi
In the proof, we weaken z with p and apply modus ponens (Imp-E ). The weakening is shown by induction over the inference rules: shows hz ` p =) set z
set z 0 =) z 0 ` pi
The proof is trivial except for the cases for Exi-E and Uni-I, where the Skolem constant xed by the induction hypothesis is only new to the smaller set of premises, not necessarily the larger ones. Again, it is necessary to perform renaming using psubst. We can now shift a list of implications: 4.3
In conclusion, we have completeness for any valid formula, open or closed: assumes h8 (e :: nat ) nat hterm) f g: e; f ; g; z j= pi shows hz ` pi
The recipe makes no particular use of natural deduction { in the places where the recipe does derivations, one expects similar derivations to be possible in other calculi. Indeed we will see that the recipe applies to our semantic tableau calculus as well.
The Isabelle theory Tableau contains the tableau formalization. We use this as a stepping stone to show completeness for the sequent calculus since the tableau rules match the consistency property making it almost trivial to show completeness.
A closed tableau should prove unsatis ability of the starting formulas. Since ? is never satis able, BasicFF allows us to close a branch directly if it occurs. More interestingly, the BetaOr rule says that both A # G and B # G have to be unsatis able for Or A B # G to be so. The remaining rules are similar.
If a closing tableau exists for the list of formulas G, then the conjunction of G is unsatis able: every interpretation falsi es some formula p in G.
The proof of TC-soundness is fairly straightforward and goes by induction on the inference rules (for an arbitrary function denotation). It is written in Isar and relies only on existing lemmas introduced by Berghofer. Only two of the inductive cases cannot be proven automatically by Isabelle: DeltaExists and DeltaNegForall. They have similar proofs and we consider the former case here.
We need to show 9 p 2 set (Exi A # G): : eval e f g p and have by the induction hypothesis: 9p 2 set (A [Fun n [] = 0] # G): : eval e ?f g p where n is a new constant and ?f represents any function denotation.
We proceed by contradiction and assume that every formula holds in the given model: (*) 8p 2 set (Exi A # G): eval e f g p. Since Exi A holds, there must be a member of the universe, say, x that satis es A[Fun n [] = 0] when n is interpreted as x: (1) eval e (f (n := w: x)) g p: A [Fun n [] = 0].
By applying the induction hypothesis at the same updated function denotation we know: (2) 9p 2 set (A [Fun n [] = 0] # G): : eval e (f (n := w: x)) g p.
From (2) we have two cases: either A [Fun n [] = 0] is false or G contains the false formula. The rst case contradicts (1) directly. Alternatively, if G contains the false formula, this contradicts our starting assumption (*).
The following abbreviates that p can be proved from assumptions ps: htableauproof ps p
(a Neg p # ps)i
htableauproof ps p =) list-all (eval e f g) ps =) eval e f g pi 5.3
We show completeness of the tableau calculus in the same way as for natural deduction: by proving a consistency property and using the model existence result to contradict the nonexistence of a closing tableau for a valid formula. In natural deduction, the consistent sets are those from which we cannot derive a contradiction (?). In tableau calculi, deriving contradictions is exactly the point, so the consistent sets are simply those without closing tableaux. The statement of our consistency theorem TCd-consistency thus becomes: shows hconsistency fS ::( 0a; 0b) form set : 9 G: S = set G ^ : (a G)gi
Our tableau rules are dual to the de nition of when a set is consistent [
Take the case when :: occurs in a consistent set S, so S [ f g should also be consistent. No closing tableau can exist for S [ f g. If it did, one would also exist for S because we can extend S with by applying the AlphaNegNeg rule to :: 2 S. The corresponding proofs for natural deduction generally require more creativity and more than one rule application.
We obtain the completeness result tableau-completeness' for closed formulas: assumes hclosed 0 pi and hlist-all (closed 0 ) psi and mod : h8 (e :: nat ) nat hterm) f g: list-all (eval e f g) ps shows htableauproof ps pi
We assume that p is valid under assumptions ps (in the universe of Herbrand terms) but that we cannot close the corresponding tableau. Then the set formed by :p and ps is consistent and we have seen that any formula in it has a model. By our validity assumption the same model satis es p, and this leads to a contradiction. 6
We use the same recipe as for natural deduction to extend the tableau completeness result to cover open formulas. However, we employ one simpli cation that would also work for natural deduction but is slightly less intuitive. Instead of closing the formula with universal quanti ers, we close it by substituting fresh constants directly for the free variables. At that point we are still operating semantically, so we only need to show that this preserves validity and doing so is simple. We still make use of the telescoping sequence of substitutions but save the introduction of the universal quanti ers. Our application of this recipe to both natural deduction and a tableau calculus indicate that it can be applied to a wider range of proof systems to strengthen existing completeness results. 7
The Isabelle theory Sequent contains the sequent formalization. 7.1
We de ne the sequent calculus as yet another inductive collection of rules:
lemma SC-soundness: h` G =) 9 p 2 set G: eval e f g pi
If the sequent G has a derivation then the disjunction of G is valid: every interpretation satis es some formula p in G. By taking the sequent with a single formula we get the expected theorem.
Dually to the tableau proof, the only two cases that are not solved automatically by Isabelle are: DeltaForall and DeltaNegExists. Consider the rst one.
We need to show 9p 2 set (Uni A # G): eval e f g p and we can assume the induction hypothesis: 9p 2 set (A [Fun n [] = 0] # G): eval e ?f g p.
When we instantiate the induction hypothesis at the function denotation f (n := w: x) we get that for all witnesses x, some formula holds: 8x: 9p 2 set (A [Fun n [] = 0] # G): eval e (f (n := w: x)) g p
Now there are two cases. Either it is the case that the rst formula holds for all witnesses, i.e. 8x: semantics e f (n := w: x) g (A [Fun n [] = 0]), or it is the case that there exists a witness that makes some formula in G hold, i.e. 9x: 9p 2 set G: semantics e (f (n := w: x)) g p.
The rst case corresponds to the semantics of the universal quanti er, so we know Uni A holds and we are done. In the second case we can recover the unmodi ed function denotation f since n is new in G, and thereby know that something in G holds, so we are done. 7.3
We show completeness of the sequent calculus by proving that for every closed tableau over a list of formulas [p1; : : : ; pn], there exists a sequent calculus derivation of the list of complementary formulas [:p1; : : : ; :pn]. This is stated in Isabelle by mapping the function compl across the list, where compl is de ned as follows: compl (: p) = p, and compl p = : p for any formula p that is not a negation. Thus in Isabelle we want to show a G =) ` map compl G.
The proof goes by induction over the tableau rules with a bit of massaging of each induction hypothesis to make the corresponding sequent calculus rule applicable. Consider for instance the AlphaAnd case where we assume a A # B # G and, inductively, ` map compl (A # B # G) and need to show ` map compl (Con A B # G). We get ` compl A # compl B # map compl G from the induction hypothesis and de nition of map. There are two cases for A (and similarly B ). Either it is of the form A = :A0 or it starts with a di erent connective. In the rst case, compl A = A'. We want to apply AlphaNegAnd which requires a derivation containing :A, so in the rst case we apply AlphaNegNeg rst. We can hereafter derive ` Neg (Con A B) # map compl G using AlphaNegAnd. In the second case compl A = :A, and we need only to apply AlphaNegAnd. Using the de nition of map again we see that it is the goal.
Ben-Ari [
The theorem SC-completeness states the completeness property: theorem SC-completeness:
xes p :: h(nat ; nat ) formi assumes h8 (e :: nat ) nat hterm) f g: list-all (eval e f g) ps shows h` p # map compl psi
Assume p is valid under assumptions ps. Any of the formulas can be open. From completeness for tableau, the tableau for : p # ps closes, so by the equivalence to sequent calculus, p # map compl ps has a sequent calculus derivation. 8
We have shown that the natural deduction system formalized by Berghofer is also complete when considering open formulas. We have also formalized the soundness and a synthetic completeness proof of a one-sided sequent calculus for rst-order logic. This was via a translation from a tableau calculus. Standing on the shoulders of Berghofer, we proved the tableau calculus complete based on his natural deduction formalization. This shows that Berghofer's work is more general than just a natural deduction formalization and can indeed be used as an o set for proving calculi complete.
As future work we envision formalizing the resolution system from Fitting's
book [
With the present paper, detailing our novel formalization in Isabelle/HOL of the soundness and completeness proofs for a sequent calculus and a tableau calculus for rst-order logic with functions, we hope that more people will get inspired and take up the gauntlet to formalize logical systems and build frameworks to aid this task. There are plenty of systems out there waiting to be formalized and plenty of room to build upon the frameworks currently available.
We thank Agnes Moesgard Eschen, Frederik Krogsdal Jacobsen, Alexander Birch Jensen, Simon Tobias Lund, Francois Schwarzentruber and Freek Wiedijk for comments on drafts.