Keywords

1 Introduction

With the proof assistant Isabelle/HOL [10] we can create canonical reference documents for logics and their metatheory. The formal language of Isabelle/HOL, namely higher-order logic, is precise and unambiguous. This means every proof can be mechanically checked. We consider here two (functionally complete) fragments of propositional logic and various axiomatic systems for these fragments. Table 1 gives an overview of the systems and fragments. Our focus is mostly syntactic and we showcase the benefits of doing this work in Isabelle. We write down both the syntax and semantics of our languages, with infix syntax and abbreviations as desired. Furthermore we specify various inference systems by their rules and axioms. The systems here are all axiomatic but the techniques work for proof systems in general.

This sets the stage for our investigations. We can easily verify that the proof systems are sound with respect to the semantics, with Isabelle doing almost all the work. We can verify completeness by adapting a formalization for a similar system or by finding derivations for the axioms of one system in the other one (and similarly for the rules). Here, Isabelle helps out: instead of painstakingly writing down each derivation, a sometimes daunting task in an axiomatic system, we can let one of its sophisticated proof methods prove its existence for us. We can even let Isabelle find the right proof method and a suitable collection of needed axioms and previously derived formulas for us with its Sledgehammer technology. With these tools at hand we can verify historical claims such as how some axiom can be omitted because it follows from the others.

Table 1. The formalized axiomatic systems. The first three are formalized in the theory System-W and use \( \bot , \rightarrow \) as primitive symbols. The last three are formalized in the theory System-R and use \( \lnot , \bigvee \) as primitives, with the abbreviation \( p \rightarrow q \equiv \lnot p \bigvee q \).
Full size table

As an example we formalize Łukasiewicz’s shortest axiom for implicational propositional logic and provide, in full, his derivation of Wajsberg’s axioms, for which we have formalized completeness. In this example we also show how to seamlessly use his notation in Isabelle and have the proof assistant translate it to the more familiar one. As another example we consider the exchangeability of two axioms.

We reproduce parts of our formalizations in the paper. The full Isabelle/HOL formalizations, 669 lines (535 sloc, source lines of code, not counting blank lines) in file and 631 lines (510 sloc) in file , are available here:

https://github.com/logic-tools/axiom

The paper strives to be self-contained so consulting the formalizations is optional. However, the availability enables the reader to investigate the formalizations on their own and, if curious, to look up anything we have omitted for reasons of space. The files can also be extended with other proof systems or taken as inspiration for different fragments of propositional logic or expansions to other logic. To verify properties of some new axiomatic system, it could be shown equivalent to one formalized here, so that soundness and completeness can be carried over. All of this with automation available to aid the process and a trusted kernel that guarantees correctness.

We modify our existing work [5] to formalize completeness of the axiomatic systems we consider. The existing completeness proof uses Henkin’s synthetic technique based on maximal consistent sets of formulas to build a model for underivable formulas. We have adapted this proof to two representatives of the fragments we consider in this paper (the two systems dubbed Axiomatics in Table 1). A lot of this work involves showing that the proof system can derive certain formulas that are used in the completeness proof. Similarly, to reuse the completeness result for the other axiomatic systems for the same fragment, we show that certain formulas can be derived using their axioms. In short, much of this work is about proving that specific formulas can be derived. The classic book by Church [3] has been an excellent source for relevant formulas and instead of fiddling with instantiating the axioms ourselves and finding the right sequence of rule applications, we call upon Isabelle’s tool Sledgehammer [2]. Often the built-in provers meson and metis can assemble the pieces for us.

Unfortunately, we are not always lucky enough to find a proof in the first attempt and Sledgehammer simply times out. We are then faced with a choice: either make a manual attempt to derive the formula or take a guess that some other formula should be derived first. We generally prefer the latter approach since it lets the proof assistant do more of the menial work for us, while leaving the more creative role of finding the right stepping stones to us.

In cases where we need to derive more than one formula to aid us, we typically mark each one of them with sorry before trying to prove them. This fake proof is accepted by Isabelle, so that Sledgehammer will pick up the lemma as usable in further derivations, but provides no guarantee that the formula can actually be derived. It saves time because we can make sure that the formulas marked by sorry are actually useful for our derivation before we try to find derivations for them in turn.

The paper is organized as follows. We continue with a discussion of the closest related work (Sect. 2). We move on to formalize the first three systems (Sect. 3) including the completeness of Łukasiewicz’s single shortest axiom. We follow up by formalizing the remaining three systems (Sect. 4) for our other fragment of propositional logic and discuss historical concerns about the independence of certain axioms. Finally we describe the main challenges and benefits of using the proof assistant Isabelle/HOL (Sect. 5) and we conclude (Sect. 6) by placing our work in the context of the IsaFoL (Isabelle Formalization of Logic) project.

2 Related Work

We see two main pieces of related work explained below: that of Michaelis and Nipkow [9] and of Fitelson and Wos [4, 13]. We distinguish ourselves by considering completeness of a number of systems based on different primitives using the same approach.

  • Michaelis and Nipkow [9] formalized a number of proof systems for propositional logic in Isabelle/HOL: resolution, natural deduction, sequent calculus and an axiomatic system. They used a much larger syntax with falsity, negation, conjunction, disjunction and implication. They both gave a syntactic completeness proof for the sequent calculus and showed completeness of the other systems by translations, but also showed completeness of the sequent calculus and axiomatic system with a Henkin-style [5] proof akin to ours. They only considered an axiomatic system similar to the Wajsberg axioms from 1939, where we consider the range of systems in Table 1. Their larger scope also means they go into fewer details than us, especially regarding the role of Isabelle in deriving formulas.

  • Fitelson and Wos [4, 13] used the OTTER theorem prover to find axiomatic proofs for a range of formulas, similar to our use of Isabelle. They start from a clause with the disjunction of the negated Wajsberg 1937 axioms and a clause consisting of the Łukasiewicz 1948 axiom. Then they ask OTTER to derive the empty clause, causing it to derive each of the Wajsberg axioms along the way. We take a different approach and verify the correctness of the inference steps given by Łukasiewicz directly in Isabelle. Moreover, we show how to use Łukasiewicz’s notation directly, instead of translating it into the clausal form of OTTER. Finally, Isabelle allows us to formalize semantics as well as proof systems.

We have recently [5] presented the details of a direct Henkin-style completeness proof for the Wajsberg axioms from 1939. In the present paper we elaborate on our use of derivations and equivalences instead of describing the Henkin-style completeness proof. We have used preliminary versions of our formalizations in the files and in our course on automated reasoning in 2020 and 2021 with, respectively, 27 and 37 MSc computer science students. The focus of the exercises was on our approach to formalization of syntax, semantics and axiomatic systems using Isabelle/HOL. As an introductory example we included a very brief description of the approach in our paper [6] about our main Isabelle/HOL tools for teaching logic, namely the Natural Deduction Assistant (NaDeA) and the Sequent Calculus Verifier (SeCaV), both much larger developments for first-order logic with functions.

3 Implication and Falsity

We start by considering Wajsberg’s axioms for the fragment of propositional logic built from propositional symbols, implication and falsity.

3.1 Language

The following datatype form embeds our syntax into Isabelle:

figure e

Vertical bars separate the three constructors. The first one introduces \( \bot \) as a primitive, the next one propositional symbols with natural numbers as identifiers and the final one is implication between two formulas, with the infix symbol \( \rightarrow \).

Besides these primitive connectives, Isabelle allows us to introduce abbreviations as we would do with pen and paper. Here for the trivially true formula and for negation:

figure f

To give our syntax meaning, we write a primitive recursion function in higher-order logic that uses an interpretation of the propositional symbols to map a formula into a truth value:

figure g

We use Isabelle’s if-then-else to interpret implication but we could also use the built-in higher-order logic implication ( ).

We can define what it means for a formula to be valid by quantifying over all interpretations:

figure i

3.2 Wajsberg 1937

Consider first Wajsberg’s proof system from 1937 [3, p. 159]:

figure j

The predicate holds for a given formula if it can be derived from the specified rule and axioms. Notably, the axioms are schemas, where p and q can be instantiated for any formula. The only rule, here and later, is modus ponens (MP). The first axiom (Imp1) corresponds to the K combinator, the second (Tran) expresses transitivity of implication and the third (Clas), Peirce’s law, implies the law of the excluded middle. Finally we have the principle of explosion (Expl).

As an example, we can derive from this last axiom:

figure m

Isabelle automatically instantiates the given axiom correctly.

Since we have specified the meaning of our formulas in Isabelle, we can verify the soundness of the proof system:

figure n

The proof works by induction over the proof system, an induction principle that Isabelle automatically provides. The proof method auto discharges each of the resulting proof obligations. Such checks are cheap and easy in Isabelle, helping to prevent typos or other mistakes.

Completeness follows the synthetic recipe due to Henkin and, together with soundness, results in the following theorem:

figure o

The proof is shown in its entirety to showcase features of the Isabelle syntax.

3.3 Wajsberg 1939

Consider a later proof system by Wajsberg with different axioms [3, p. 163]:

figure p

We still have the Imp1 axiom corresponding to the K combinator, but as second axiom we now have a correspondence to the S combinator (both axioms used by Frege). Finally, with the abbreviation for Neg, we see that this last axiom eliminates a double negation.

We can now verify that the two systems prove the same formulas:

figure q

As part of the proof we find derivations for the transitivity principle (Tran) and Peirce’s law in the latter system.

3.4 Shortest Axiom

Considering the fragment of classical logic with implication but without a symbol for falsity, Łukasiewicz found a shortest single axiom from which you can derive the rest [12].

To obtain completeness for our fragment with a symbol for falsity, we also need the principle of explosion [3, p. 159]:

figure r

Łukasiewicz writes \( C\ p\ q \) for \( p \rightarrow q \). This prefix notation allows him to avoid parentheses. We can use it in Isabelle via the following specification:

figure s

We set the symbol \( C \) up with the mixfix specification \( [0, 0],\ 1 \), giving the two arguments higher precedence (0) than the full expression (1). This means that e.g. \( C\ C\ p\ q\ r \) is parsed correctly into \( (p \rightarrow q) \rightarrow r \). Since we specified the abbreviation as input only, any Isabelle output will display the formulas in the conventional \( \rightarrow \)-notation.

Łukasiewicz shows in 29 lines how to derive the Wajsberg axioms (Axiomatics above). With our abbreviation we reproduce his derivations almost verbatim in Figs. 1 and 2 on pages 14 and 15. The formalization follows the original faithfully: each line is only derived from the specified lines and modus ponens as passed to the meson prover. Łukasiewicz carefully describes how to instantiate each previous formula in order to arrive at the current formula but we leave this to Isabelle to figure out. While Łukasiewicz’s paper must be hand-checked to ensure there are no errors, Isabelle instantly verifies the correctness of our formalization. Given those derivations we can prove equivalence between this proof system and the first Wajsberg axioms:

figure t
Fig. 1.
figure 1

Lines 1–15 of Łukasiewicz’s derivation.

Full size image
Fig. 2.
figure 2

Lines 16–29 of Łukasiewicz’s derivation.

Full size image

We use the completeness of the Wajsberg axioms to show that Łukasiewicz’s formula can be derived. In the other direction we use the formulas in lines 27–29 of Fig. 2.

4 Disjunction and Negation

We now wipe the slate clean and consider Rasiowa’s axioms for a different fragment of propositional logic built from propositional symbols, negation (\( \lnot \)) and disjunction (\( \bigvee \)).

4.1 Language

Again we specify the syntax as a datatype in Isabelle:

figure u

We regain implication through its classical interpretation:

figure v

We again define the trivially true formula, this time more abstractly since we no longer have available (in Isabelle/HOL, by formulation, each type has one designated value that is undefined but we do not know which value it is):

figure x

Given , however, defining becomes simple:

figure aa

We specify the semantics similarly to before:

figure ab

4.2 Rasiowa 1949

Consider the following proof system by Rasiowa [3, p. 157]:

figure ac

To aid readability we write the rules using the abbreviation for implication introduced above ( ), but we recall that it is not a primitive. If we expand the abbreviation for the modus ponens rule (MP), it infers \( \vdash q \) from \( \vdash p \) and .

The first axiom (Idem) expresses idempotence of disjunction. The second (AddR) builds a disjunction from a given formula by adding an arbitrary formula on the right-hand side. Finally, the last axiom (Swap) does two things: it replaces the formula on right-hand side of the disjunction with an implied formula and then it swaps the two sides of the disjunction.

The principle of explosion is not a built-in axiom but Isabelle can quickly find a derivation:

figure af

We can just as quickly verify the soundness:

figure ag

The axiom AddR forms a disjunction with the given formula on the left and an arbitrary one on the right. We might wonder if this is essential or whether we could add the arbitrary formula on the left instead (i.e. AddL). Isabelle can help answer this question:

figure ah

We see that AddR can be derived from AddL (in Isabelle given after if and referred to as that) alongside the remaining proof system. Note that AddR is not made available to metis.

Likewise, we can derive AddL from the full proof system:

figure ai

Thus, we can quickly answer questions about different variants of the axioms.

A notable derivable formula is the following that substitutes a formula on the right-hand side of a disjunction with an implied formula:

figure aj

Again, we can prove the completeness of the system:

figure ak

4.3 Russell 1908 and Bernays 1926

Consider now another proof system over the same fragment [3, p. 157]:

figure al

Here we have first Idem and AddL, then a permutation or commutativity principle for disjunction (Perm) and finally SubR. We only need the derived SubR to show equivalence:

figure am

4.4 Whitehead and Russell 1910

Consider next the system for propositional logic that appears in the first volume of the three-volume Principia Mathematica (often abbreviated PM):

figure an

Here we have Idem, AddL, Perm, a distributivity principle and SubR. We can easily show that we can derive at least as many formulas when we have the extra axiom:

figure ao

To show the equivalence in both directions, we use the completeness of RB to prove the existence of a derivation for the extra axiom:

figure ap

5 Challenges and Benefits

Isabelle helped enormously in adapting the completeness proof to each of the two fragments, since it is easy to define abbreviations for non-primitive connectives and the proof assistant gives an error everywhere something needs to be changed. What the proof assistant cannot tell us, is what sub-derivations are needed to derive a key formula. This proved a particular challenge for the Rasiowa axioms for the fragment \( \lnot , \bigvee \). Those axioms are concerned with these two operators but we usually think in terms of implication, \( \rightarrow \), and want to derive formulas like the Wajsberg 1937/1939 axioms (cf. Table 1). However, the starting point does not give us much help. For instance, to derive the following transitivity of implication, a useful lemma for further derivations, we must first derive several other formulas:

figure aq

One of the formulas we found useful is the following, somewhat unintuitive, SwapAnte lemma:

figure ar

Luckily, Isabelle makes it easy to quickly derive a range of formulas (or pretend to derive them with sorry) and figure out which ones are useful after the fact. As we have shown throughout the paper, this allows us to quickly investigate connections between various proof systems, with Isabelle keeping track of the details for us.

6 Conclusion

We have seen two languages and a range of axiomatic proof systems with various derivations and equivalences. To our knowledge, most of the systems have been formalized here for the first time with soundness and completeness proofs.

Our work is part of the IsaFoL (Isabelle Formalization of Logic) project [1] which aims at developing formalizations in Isabelle/HOL of logics, proof systems, and automatic/interactive provers. Other work in the same line includes completeness of epistemic [7] and hybrid [8] logic and an ordered resolution prover for first-order logic [11]. The project collects formalizations such as ours that can be used as reference documents to verify historical claims, in teaching logic, or to aid in the formalization of other logics and potentially executable provers. Our own formalization could serve as starting point for a student project to formalize the completeness of some other axiomatic proof system.

A notable thing about our approach is that while we show that several formulas are derivable in one system or another, we do not give the derivation itself. Instead, we let an automated prover like metis or meson find it. This allows us to move quickly and at a higher level than if we spelled out each step in full: faced with a formula that is hard to derive we can experiment with simpler formulas that the automation can handle and try to piece things together afterwards. As mentioned, this was exactly how we worked to derive many of the formulas. However, it also means that even if we prove that a formula can be derived, we have no derivation to inspect; we must simply trust Isabelle that it exists. Meanwhile, we argue that Isabelle is at least as trustworthy as a human author whose work we might not check in the first place. If we do wish to spell out the derivation, Isabelle can help us do so, by proving that derivations exist for our stepping stones.

The ability to introduce abbreviations can provide interesting perspectives on formulas. Consider the usual axiom for disjunction elimination:

figure as

We might think of it as “if both \( p \) and \( q \) imply \( r \), then if we know either then we know \( r \).” In the language with disjunction and negation, the implication is an abbreviation and expanding the inner ones gives us:

figure at

This has another natural reading: “either \( p \) is false or \( r \) holds, and either \( q \) is false or \( r \) holds, but either \( p \) or \( q \) is in fact true, so \( r \) must hold.” An interactive system like Isabelle makes it simple to hide away details like the abbreviation for implication but also to peek at them if we want to.