Gustavo Bandeira (Mar 17 2024 at 08:52): Gustavo Bandeira (Mar 17 2024 at 08:52):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:
Yong Kiam (Mar 17 2024 at 13:44):I don't have that textbook, but since that exercise says to use "Isabelle/HOL", I guess what it means is for you to define a deep embedding of the relevant logic in Isabelle and prove it in that embedding
or the simpler interpretation is to just prove it using whatever Isabelle tactics were introduced in the textbook so far
Gustavo Bandeira (Mar 17 2024 at 16:40):Yong Kiam said:
I don't have that textbook, but since that exercise says to use "Isabelle/HOL", I guess what it means is for you to define a deep embedding of the relevant logic in Isabelle and prove it in that embedding
or the simpler interpretation is to just prove it using whatever Isabelle tactics were introduced in the textbook so far
How do I do that? I guess the second choice is just making Isabelle prove it without concern for what it's using, but I'm not sure how to do the first one.
Yong Kiam (Mar 17 2024 at 16:42):one way: define the syntax of formulas in the relevant logic as a datatype, define a relation over it that corresponds to derivability in the logic, and show that your particular formula (written as an element of the datatype ) is in the relation
Gustavo Bandeira (Mar 17 2024 at 16:43):What is the meaning of "relevant logic"? Is it "logic + the axioms in each system"?
Mathias Fleury (Mar 17 2024 at 16:45):There are various examples in the AFP, like https://www.isa-afp.org/sessions/paraconsistency/#Paraconsistency
Gustavo Bandeira (Mar 17 2024 at 16:57):Mathias Fleury said:
There are various examples in the AFP, like https://www.isa-afp.org/sessions/paraconsistency/#Paraconsistency
Ah. I see. I know next to nothing about logic but I don't think this problem has to do with paraconsistency, I guess I should just prove it using the recommended axiom systems.
Mathias Fleury (Mar 17 2024 at 17:14):… no it has nothing to do with paraconsistency. But defining the logic will be similar
Gustavo Bandeira (Mar 18 2024 at 02:32):Mathias Fleury said:
… no it has nothing to do with paraconsistency. But defining the logic will be similar
How do I do that? I don't know what to do just by looking at the webpage you mentioned. (I know next to nothing about Isabelle/HOL).
Yong Kiam (Mar 18 2024 at 04:03):in that case, it might be better to consider reading the prog-provetutorial, specifically you'll need to know how to write a datatype and how to define an inductive relation over it
(again, I don't know the context of the book, so this might be overkill, and it might really just be asking you to do option 2)
Gustavo Bandeira (Mar 18 2024 at 04:46):Yeah, thanks. I'll just do that for now:
I guess it's this, right?
Yong Kiam (Mar 18 2024 at 04:52):sure, I suppose
Mathias Fleury (Mar 18 2024 at 06:02):Somehow I doubt it, because this is not a proof in Hilbert's logic.
Mathias Fleury (Mar 18 2024 at 06:03):But as long as this is good enough for you, then it is fine
Gustavo Bandeira (Mar 18 2024 at 06:04):Mathias Fleury said:
Somehow I doubt it, because this is not a proof in Hilbert's logic.
Interesting, how can we know it?
Mathias Fleury (Mar 18 2024 at 06:10):Well technically you do not know what simp did (although you could check with supply [[simp_trace]]). But this is the point
Mathias Fleury (Mar 18 2024 at 06:11):Also both versions holds in intuitionistic logic (I think), while Isabelle uses classical logic. So unprovable intuitionistic goals can be proven by simp…
Gustavo Bandeira (Mar 18 2024 at 06:12):Mathias Fleury said:
Somehow I doubt it, because this is not a proof in Hilbert's logic.
Can't we do it like this:
We assume A is true and use the following Hilbert Axiom: A->(B->A) with A=B and modus ponens, then we get A->A?
Mathias Fleury (Mar 18 2024 at 06:15):I am not saying that the statements do not hold (as you wrote they do)
Mathias Fleury (Mar 18 2024 at 06:15):I am saying that you should produce a valid proof in the axiom system you are considering
Gustavo Bandeira (Mar 18 2024 at 06:18):Mathias Fleury said:
Well technically you do not know what simp did (although you could check with
supply [[simp_trace]]). But this is the point
This is really nice. At the moment, it's not to clear to me what is a "proof" in Isabelle. I just type a formula and use simp, and it seems that if no bugs appears, it's proved? It wasn't too clear what is happening under the hood when I use simp. I guess you kinda answered one of my doubts.
Mathias Fleury (Mar 18 2024 at 06:23):Maybe I interpreted the questions wrong actually. I read the last as "prove A->A using Hilbert's axiomatic system in Isabelle", but maybe it was just intended as "prove A->A in Isabelle using the built-in axiomatic system" (which is what you are doing)
Gustavo Bandeira said:
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:
Mathias Fleury (Mar 18 2024 at 06:23):Gustavo Bandeira said:
Mathias Fleury said:
Well technically you do not know what simp did (although you could check with
supply [[simp_trace]]). But this is the pointThis is really nice. At the moment, it's not to clear to me what is a "proof" in Isabelle. I just type a formula and use simp, and it seems that if no bugs appears, it's proved? It wasn't too clear what is happening under the hood when I use simp. I guess you kinda answered one of my doubts.
It is a correct proof and it is perfectly fine
Mathias Fleury (Mar 18 2024 at 06:24):… it is just a proof in HOL
Yong Kiam (Mar 18 2024 at 06:59):indeed, I think if you want to do the first thing that Mathias listed (prove A->A using Hilbert's system), then you'll need to get much more familiar with Isabelle...
Gustavo Bandeira (Mar 18 2024 at 15:09):Mathias Fleury said:
Well technically you do not know what simp did (although you could check with
supply [[simp_trace]]). But this is the point
Where do I see the output of simp_trace? I wrote this:
lemma "A ⟶(¬A ⟶B)"
supply [[simp_trace]]
apply simp
done
But am not seeing anything different.
Mathias Fleury (Mar 18 2024 at 15:17):Put the cursor on simp
Gustavo Bandeira (Mar 18 2024 at 16:31):Mathias Fleury said:
Put the cursor on simp
It shows only this:
Mathias Fleury (Mar 18 2024 at 16:49):you need the output panel
Mathias Fleury (Mar 18 2024 at 16:49):Plugins > Isabelle > output panel
Last updated: Apr 28 2024 at 12:28 UTC