# How to choose an axiom system in Isabelle/HOL?

First of all, sorry if my question is too nonsensical and naive, I'm just getting started with Isabelle/HOL. I am reading Hou's "Fundamentals of Logic and Computation: With Practical Automated Reasoning and Verification". I have the following problems to do using Isabelle/HOL:

How do I make Isabelle/HOL prove this assuming only Hilbert's or Lukasiewicz's axiom system? I've done an example in the book but I'm not sure which axioms were used to prove it:

• It seems that it is part of the prerequisites of the exercise either to implement the different axiom systems or to use only the relevant rules by hand. Automated methods will invoke everything they can in order to reach the goal, so they cannot be trusted this kind of work. Please provide the example in order to get which way things go here. Commented Mar 17 at 11:23
• @PedroSánchezTerraf How do I do that? BTW: Examples of what? I'm confused. Commented Mar 17 at 16:35
• If you are getting these instructions from a public source, it would really help to share a link (and chapter/page number if needed). (I think that is what @PedroSánchezTerraf meant by “example”.) If these are homework, then it would be good to ask your teacher. But I think 1.7 and 1.8 likely mean to prove it with pen and paper. (Although Isabelle is a meta logic so it is possible it instead means to implement that axiom system in Isabelle. If it means that, then there would likely be an example in the text you referenced of how to do that.) Commented Mar 17 at 20:05
• Exactly what Jason said (thanks!); I was trying to convey his last sentence. Commented Mar 17 at 20:18
• I see you included the book title. The chapter is here, but behind a paywall: link.springer.com/chapter/10.1007/978-3-030-87882-5_1 Given that the footnote to 1.9 tells you where to download Isabelle, and that Isabelle/HOL refers to Isabelle with the HOL axiom-system (the most standard way to use Isabelle), I am even more sure the book is not suggesting you implement Hilbert's or Łukasiewicz's axioms in Isabelle, but just do the problem via pen and paper, and then use Isabelle/HOL's built-in tactics to prove the same result (exactly the sort of thing you are doing in the screenshot). Commented Mar 18 at 1:56

If one wants to be really sure that one is not using any of Isabelle/HOL's facts, an alternative to my main answer would be to really start with a blank slate, only building on Isabelle/Pure (i.e. the meta logic).

In this case, one needs to define one's own object logic with its own truth judgement and axiom system:

theory Scratch
imports
Pure (* not HOL! *)
begin

typedecl hilbert_bool

judgment Trueprop :: ‹hilbert_bool ⇒ prop›  (‹(_)› 5)

axiomatization
implies :: ‹hilbert_bool ⇒ hilbert_bool ⇒ hilbert_bool› (infixr ‹⟶› 6)
where
axiom_1: ‹A ⟶ (B ⟶ A)› and
axiom_2: ‹(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))› and
(* let's ignore negation for simplicity. *)
mp: ‹A ⟶ B ⟹ A ⟹ B›


After this, exactly the same proof as in the other answer is possible:

lemma ‹A ⟶ A›
proof -
from axiom_1 have F01:
‹A ⟶ (A ⟶ A)› .
from axiom_1 have F02:
‹A ⟶ (A ⟶ A) ⟶ A› .
from axiom_2 have F03:
‹(A ⟶ ((A ⟶ A) ⟶ A)) ⟶ ((A ⟶ (A ⟶ A)) ⟶ (A ⟶ A))› .
from mp F03 F02 have F04:
‹(A ⟶ (A ⟶ A)) ⟶ (A ⟶ A)› .
from mp F04 F01 show F05:
‹A ⟶ A› .
qed

end


In Isabelle/Pure, only the vanilla Isar proof methods are available—so no auto, blast etc..

Usually, one does not want to do this, as it's easy to come up with unsound theories once one uses the axiomatization command .

Usually, Isabelle/HOL's proof methods will get most of propositional and predicate logic out of the way immediately. (Otherwise, by blast will solve them reliably.) But it is possible to emulate Hilbert-style deductions in Isar quite nicely.

To show the point, I'll just redress the proof of $$A \rightarrow A$$ from https://math.stackexchange.com/questions/2923329/how-to-prove-vdash-p-to-p-using-hilbert-axioms in Isar. (It uses a slightly more convenient axiom set than the textbook in the question, I think.)

First, we'll establish that the axioms used in the example are also facts of Isabelle/HOL (phew!).

theory Scratch
imports HOL.HOL
begin

proposition hilberts_axioms:
‹A ⟶ (B ⟶ A)›
‹(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))›
‹(¬B ⟶ ¬A) ⟶ (A ⟶ B)›
by blast+


If we can use only these (and modus ponens mp) to derive a fact, then this is equivalent to a Hilbert calculus deduction. In order to be sure, we'll only use the most trivial proof method ..

lemma ‹A ⟶ A›
proof -
from hilberts_axioms(1) have F01:
‹A ⟶ (A ⟶ A)› .
from hilberts_axioms(1) have F02:
‹A ⟶ (A ⟶ A) ⟶ A› .
from hilberts_axioms(2) have F03:
‹(A ⟶ ((A ⟶ A) ⟶ A)) ⟶ ((A ⟶ (A ⟶ A)) ⟶ (A ⟶ A))› .
from mp F03 F02 have F04:
‹(A ⟶ (A ⟶ A)) ⟶ (A ⟶ A)› .
from mp F04 F01 show F05:
‹A ⟶ A› .
qed


Discharging a proof step by . (or equivalently by by this), is equivalent to saying: Take the first supplied fact as a deduction rule and instantiate its premises with the other listed from-facts exactly in this order.

Thus, we're sure that the proof has been performed by this specific deduction and not by any fancy Isabelle magic.