Ulrich Schmid (Mar 01 2022 at 16:43): Ulrich Schmid (Mar 01 2022 at 16:43):Hello,
I do not work with Isabelle yet and therefore still need some basic information. I am interested in statements (wff's) of axiomatic set theory (based on ZFC), such as A:≅ "∀a∀b∃c∃d (c∈d∧(¬c=a∨¬d=b)∨c=a∧d=b∧¬c∈d)". The statement A is true in ZFC and is just to give a simple example.
What result does Isabelle return in this case:
1) statement A is true in ZFC and
2) chain of evidence for the truth of this statement?
Many thanks in advance for your feedback.
Jonathan Julian Huerta y Munive (Mar 01 2022 at 17:28):Hi, when typing in Isabelle/HOL lemma "∀a b. ∃c d. ((c∈d ∧ (¬c=a ∨¬d=b)) ∨ (c=a ∧ d=b ∧ ¬c∈d))", Isabelle immediately outputs a counterexample:
Auto Quickcheck found a counterexample:
a = a1
b = {a1}
The reason is because in Isabelle/HOL, a and b above have types a::'a and b::'a set respectively and Isabelle cannot guarantee that type 'a has an element other than a. Nevertheless, I assume this is not the case for someone using Isabelle/ZFC which I have not learned to run. On the other hand, the following theorem is true in Isabelle/HOL:
lemma "CARD('a) ≥ 2 ⟹ ∀a::'a. ∀b::'a set. ∃c d. ((c∈d ∧ (¬c=a ∨¬d=b)) ∨ (c=a ∧ d=b ∧ ¬c∈d))"
by (metis (full_types) UNIV_I card.empty card_Suc_eq empty_iff
insertCI lessI linorder_not_less numeral_2_eq_2)
Here, Isabelle's Sledgehammer tool automatically found a proof calling the theorem prover metis and we are only assuming that the type 'a has cardinality greater than 2.
Ulrich Schmid (Mar 02 2022 at 09:11):Thanks a lot for the quick response.
The opposite of A is
¬A:≅ ∃ab∀cd (c∈d ⇔ c=a ∧ d=b), hence the counterexample given by the Auto Quickcheck is correct only for one direction:
⇐: c=a ∧ d={a} implies c∈d, but the other direction (⇒) of the counterexample for A is not true in ZFC.
But the second result from Isabelle's Sledgehammer is close to the truth in ZFC, even if the constraint "a has cardinality greater than 2" is not necessary.
I suspect that in Isabelle/ZFC the result will be complete including chain of evidence.
Some further questions:
a) is Isabelle/ZFC available?
b) is there a chain of evidence in the second example, or does Sledgehammer just provide true/false?
Mathias Fleury (Mar 02 2022 at 09:22):a) Yes just run Isabelle by selecting ZF as base session (isabelle jedit -l ZF)
b) auto proves your goal automatically.
c) Sledghemmar is not available for ZF.
Mathias Fleury (Mar 02 2022 at 09:23):Oh and auto does not prove detailled information how it proved the goal
Mathias Fleury (Mar 02 2022 at 09:23):Remark that a large majority of people (including me!) have never used Isabelle/ZF.
Ulrich Schmid (Mar 14 2022 at 14:42):Hello,
I have now successfully installed Isabelle on my computer (hopefully) and would like to start with a small and simple example. For me it is first important to get familiar with the way Isabelle works. Therefore, I would like to have an automatic proof for statement A in ZFC where
A= "∃xn∀t∃u (t∈x ⇒ n∈t∧t∈u∧u∈x)"
I have some questions:
i) what could be the easiest program to run here in Isabelle?
ii) how do I start the created program?
iii) Where do I find the result "A is false" or "A is true" after running the program?
Thanks a lot in advance
Wolfgang Jeltsch (Mar 14 2022 at 22:55):I suggest two things:
prog-prove tutorial available from the IDE and the website, as it is by far the best way to get into Isabelle. Sławomir Kołodyńaski (Mar 16 2022 at 08:04):There may be some misunderstanding here on what Isabelle is for and what it can do. You don't run programs in Isabelle, at least not in Isabelle/ZF. The main function of Isabelle is to formally verify proofs you provide. It can fill small gaps in your proofs, but it will not serve as an oracle where you provide a statement and it tells you if it is true or not with a generated proof ("chain of evidence"). The way it works is that you provide Isabelle/ZF a statement with a proof written in a formal proof language and Isabelle tells you if your proof is correct. Things may be somewhat different in Isabelle/HOL, but I never used it so I do not know the details.
Wolfgang Jeltsch (Mar 16 2022 at 16:26):At least with Isabelle/HOL, you can also extract code, meaning you can turn certain computable parts of your development into program code in one of the major functional programming languages (ML, Haskell, Scala, at least). As a result, you can essentially write executable code whose correctness you’ve checked fully or partially.
Ulrich Schmid (Mar 19 2022 at 09:49):Thank you for the feedback.
I would like to explain my ideas more precisely.
It is about transforming statements which are described in the language of axiomatic set theory (FOL) as wff, into other statements. The new statement (wff) should be less complicated but equivalent to the original one, within the framework of some given ZFC axioms (union, foundation, replacement). Here is a simple example.
We define statements A and B as follows:
A= "∃xn∀t∃u (t∈x ⇒ n∈t∧t∈u∧u∈x)"
B= "∃x∀t∃u (t∈x ⇒ t∈u∧u∈x)"
Now here the statement A shall be replaced by the simpler B. It is obvious that B follows directly from A (A-->B), but proving the opposite direction is already harder (B-->A). At exactly this point I see the use of Isabelle/HOL (possibly involving Sledgehammer) or Isabelle/ZFC. It is not primarily about getting a chain of evidence from Isabelle, but only a hint that A is derivable from B, under certain assumptions, or not. With such a hint, it then makes sense to search for a chain of evidence, if it is not found automatically. The search for a chain of evidence can be very time-consuming and the knowledge whether (B-->A) or ¬(B-->A) holds would facilitate the work in this context extremely, since in each case the opposite can be excluded (if the problem is decideable). In the present example a helpful result from Isabelle would be the confirmation that (B-->A) holds.
Wolfgang Jeltsch (Mar 19 2022 at 13:02):Do I get this correctly that you are looking for automated proving or disproving of such implications or at least simplifications of the problem? There are certainly automated provers in Isabelle, but only few of them are capable of simplifying goals (most will either prove them completely or fail). The only example of a prover that can also simplify and at the same time should work with ZF is simp, but I’m not sure how useful it is for doing what you want to do.
Sławomir Kołodyńaski (Mar 20 2022 at 10:38):Somewhat surprisingly, for this particular example Isabelle/ZF auto method confirms the implication in both directions, theory file attached Scratch.thy . I would not count on that happening on nontrivial statements though.
Wolfgang Jeltsch (Mar 20 2022 at 14:24):Oh, I didn’t know that auto works for Isabelle/ZF. I think blast only works for Isabelle/HOL. Is that correct?
Sławomir Kołodyńaski (Mar 20 2022 at 15:46):simp, auto, blast and fast work for Isabelle/ZF.
Wolfgang Jeltsch (Mar 20 2022 at 15:53):Ah, I think blast is presented in the reference manual as a classical reasoner, and probably I translated that erroneously as “works only with Isabelle/HOL” instead of “works perhaps also with Isabelle/FOL and Isabelle/ZF but not with Isabelle/CTT”. :smile:
Ulrich Schmid (Mar 20 2022 at 19:58):The fact that Isabelle/ZF auto method confirms both directions sounds optimistic to me especially since only one direction is trivial. For the other direction, several ZFC axioms are already needed, some of which I mentioned above, and some formal effort is already required (for B-->A).
The important thing is not so much to get a chain of evidence, but rather the hint that it is possible to find one. With the information that it is possible to find a proof (in the example: Theorem B-->Theorem A), one can then try to construct one. So it would save a lot of effort, because in the negative case one would not try to find a proof by oneself.
Ulrich Schmid (Mar 21 2022 at 08:02):The small program example Scratch.thy seems to be exactly what I am looking for in general.
I just saw that for the theorems A and B I forgot to require that x should be not equal to the empty set (x≠⌀), since in the case x=⌀ both sides always hold, so this means that
A= "∃xn∀t∃u (t∈x ⇒ n∈t∧t∈u∧u∈x)∧x≠⌀" and B= "∃x∀t∃u (t∈x ⇒ t∈u∧u∈x)∧x≠⌀"
Under this change, does Isabelle/ZF auto method also confirm both directions?
Sławomir Kołodyńaski (Mar 21 2022 at 08:37):After adding the x nonempty condition A --> B is accepted but B--> A is not.
Ulrich Schmid (Mar 21 2022 at 12:00):Is there a chance that simp, blast, or fast with the example program Scratch.thy find a correct solution? Is sledgehammer available for Isabelle/ZF after all?
Mathias Fleury (Mar 21 2022 at 12:05):By definition, the answer accepted is correct. But there is no guarantee that tactics can prove every provable goal.
Sławomir Kołodyńaski (Mar 22 2022 at 07:13):simp, blast and fast also do not accept B-->A in this example. Sledgehammer is not available for Isabelle/ZF.
Ulrich Schmid (Mar 26 2022 at 08:46):I have a basic question about Isabelle/ZF for a better understanding:
The manual of Isabelle/ZF (Isabelle's Logics: FOL and ZF, Lawrence C. Paulson
Computer Laboratory University of Cambridge, with Contributions by Tobias Nipkow and Markus Wenzel December 12, 2021) says "A tremendous amount of set theory has been formally developed, including the basic properties of relations, functions, ordinals and cardinals. Significant results have been proved, such as the Schröder-Bernstein Theorem, the Wellordering Theorem and a version of Ramsey’s Theorem. ZF provides both the integers and the natural numbers".
What does "The Schröder-Bernstein theorem is proven" mean? Is it just a formal (syntactically) verification of an existing proof for this theorem written in FOL/ZF? Or is it an automatically generated proof of this theorem, or at least some parts of the proof? Or is the output of Isabelle/ZF here: "The Schröder-Bernstein Theorem is true in ZFC", but no chain of evidence or parts of it are generated?
Thank you for a feedback
Kevin Kappelmann (Mar 26 2022 at 08:51):Most (*) proofs in Isabelle are user-guided proofs with some holes completed by algorithms.
(*) actually, loads of proofs are automatically generated whenever you, for example, define a data type. But I am talking about the proofs users actually write down in a theory file.
Ulrich Schmid (Mar 26 2022 at 15:34):How could the concrete proof step B --> A (see above) be automatically generated in Isabelle? I am mainly interested in Isabelle/ZF determining "B --> A is true" and not so much in a chain of proof, which I can search for myself if I know that such a chain exists. The statements A and B were defined in our example as follows:
A= "∃xn∀t∃u (t∈x ⇒ n∈t∧t∈u∧u∈x)∧x≠⌀"
and
B= "∃x∀t∃u (t∈x ⇒ t∈u∧u∈x)∧x≠⌀".
B --> A can be proven with the help of the ZFC-axioms of foundation, replacement and union. I chose this example to become familiar with Isabelle and see if it could be used for my ideas.
The proof is not too difficult, so Isabelle/ZF should actually be able to conclude that B-->A is true.
What further tools can be used in Isabelle for this example?
Wolfgang Jeltsch (Mar 27 2022 at 10:06):Ulrich Schmid schrieb:
Or is the output of Isabelle/ZF here: "The Schröder-Bernstein Theorem is true in ZFC", but no chain of evidence or parts of it are generated?
I don’t know exactly what you would consider a “chain of evidence”. Usually, when Isabelle proves something, it derives the result from known facts by logical deduction steps whose correctness it checks. By default, Isabelle doesn’t construct a proof term, which you could inspect afterwards to convince yourself that there is indeed a proof. However, the Isabelle software is constructed such that every deduction it performs has to pass a correctness check. Therefore, it’s as good as if Isabelle would construct a proof term, as long as you trust the small core component that checks for the correctness of deduction steps.
Sławomir Kołodyńaski (Mar 27 2022 at 16:35):"The Schröder-Bernstein theorem is proven" means that someone has formulated the theorem and written its proof in Isabelle formal proof language (Isar) which was then verified by Isabelle as correct. It also means that you can reference this theorem when you are writing a proof of another theorem. Except for very simple cases the output of Isabelle/ZF is more like "the proof provided is correct" rather than "this is true in ZFC".
Ulrich Schmid (Mar 28 2022 at 08:17):I would like to question again an essential point at the example B --> A which can occur as a partial step in a longer proof of a corresponding theorem. If the whole proof is written in Isar, then sooner or later Isabelle comes to exactly this point and now has to check if it can be verified. In the present case Isabelle would not accept the present theorem. How does it continue at this point and how often does this occur?
Mathias Fleury (Mar 28 2022 at 13:06):Here is the theorem https://isabelle.in.tum.de/library/ZF/ZF/Cardinal.html#Cardinal.schroeder_bernstein|fact. All you other questions require that you start a tutorial on Isabelle (Isabelle/HOL is define). This will clarify what Isabelle is and what it can do.
Wolfgang Jeltsch (Mar 28 2022 at 16:02):I can only second this. Even if you’re going to work in Isabelle/ZF, studying the Isabelle/HOL tutorial called prog-prove will be extremely valuable. It’s the one accessible introduction to Isabelle I know. Switching from Isabelle/HOL to Isabelle/ZF shouldn’t be difficult: it only means switching the underlying logic and learning which of the automated provers don’t work for ZF. :smile:
Ulrich Schmid (Mar 29 2022 at 08:44):Thanks for the information, I will look into it.
Ulrich Schmid (May 07 2022 at 16:02):I've dug into the documentation a bit and created a small example. For this I have oriented myself on the above Cardinal Theory:
https://isabelle.in.tum.de/library/ZF/ZF/Cardinal.html#Cardinal.schroeder_bernstein|fact
and used this as a template. The definitions "eqpoll" and "finite" I have taken over to prove the lemma abc (see attachment):
Let A be a infinite set ==> A ≈ A ∪ {A}.
But Isabelle does not accept my program and brings the message: Bad theory import "Draft.OrderType", bad theory import "Draft.finite",....
Thank you for a feedback
Exercise1.pdf
Sławomir Kołodyńaski (May 07 2022 at 18:48):A couple of things: you need to qualify the imports with "ZF" when importing from Isabelle/ZF. There is no need to provide type specifications. The symbol \<approx> and the word "Finite" are already used by your imports, so you cannot reuse them. The lemma is too complicated to be proven by auto. I attach the file that works (except for the proof of the lemma of course). You may want to check IsarMathLib's Cardinal_ZF theory on various results on cardinals that are not in the standard Isabelle distribution.
Exercise1.thy
Roland Coghetto (May 08 2022 at 08:34):Small error of retranscription (Exercise1.thy) :wink:
I think you should read:
definition eqpoll (infix "≅" 70) where "A≅B ≡ ∃f. f∈bij(A,B)"
rather
definition eqpoll (infix "≅" 70) where "A≅B ≡ ∃f. f∈A"
Ulrich Schmid (May 08 2022 at 12:11):yes thank you, that is correct. I have now changed this in the program.
The proof for lemma abc can be written as follows:
A is infinite ==> there is an uncountably infinite subset I of A with I = {i1, i2, i3,.....}.
Now we can define a bijective function f: I -> I ∪ {A} by
f(i1) = A,
f(i2) = i1,
f(i3) = i2,
and so on......
With the help of f we can define a bijective function g: A -> A ∪ {A} as follows
g(x) = f(x) if x is an element of I and g(x) = x otherwise.
Maybe there is a shorter proof, but my question is, how can this proof be integrated into the program "Exercise1.thy" in a way that Isabelle can verify it?
Sławomir Kołodyńaski (May 08 2022 at 15:05):@Roland Coghetto , thanks.
As for the first step (A is infinite ==>...) I suggest to focus on that and try to prove as a separate lemma. The first step would be to formulate it so that it has a chance of being true (uncountably infinite?) , then try to formally express what you mean by the notation {i1,i2,...} (probably a subset of A that is bijective with natural numbers).
Ulrich Schmid (May 08 2022 at 18:49):sorry, this is a spelling mistake, correct is "a countably infinite subset I".
I will try to implement your suggestion and describe each individual step as transparently as possible.
Ulrich Schmid (May 14 2022 at 07:57):I constructed a proof in ZFC (see appendix page 1) with 3 lemmas and in a second step tried to translate the result into Isabelle (see page 2). Proof of lemma1 and lemma2 "by auto" and lemma3 using the first two, but the following error messages occur in Isabelle:
Lukas Stevens (May 14 2022 at 12:24):It would be easier if you would format code directly in Zulip using Markdown. See here how to do that https://zulip.com/help/format-your-message-using-markdown#code. Alternatively, you can attach the theory file to the message.
Lukas Stevens (May 14 2022 at 12:28):Your problem is that the term ℕ is not defined.
Lukas Stevens (May 14 2022 at 12:31):If I understand it correctly, the set of natural numbers is just called nat in ZF.
Sławomir Kołodyńaski (May 14 2022 at 19:13):There are a couple of problems.
FiniteSet(A), but then in the lemma ad1 you reference finite(A), and in lemma ad3 you reference Finite(A). I guess they all should be FiniteSet(A), or perhaps (better) Finite(A) as this is defined in one of the imported theories.nat in Isabelle/ZF \<not> in Isabelle/ZF, not "~"lemma ad1: assumes "\<not>FiniteSet(A)" shows "\<exists>B. B\<subseteq>A \<and> B\<cong>nat" sorry
(consider using Finite(A) instead of FiniteSet(A) and \<approx> instead of \<cong> here as those are defined in the imports and there are lemmas there about these notions that you may want to reference in your proofs). So better:
lemma ad1: assumes "\<not>Finite(A)" shows "\<exists>B. B\<subseteq>A \<and> B\<approx>nat" sorry
Similarly the remaining lemmas can be
lemma ad2: assumes "B\<approx>nat" shows "\<exists>g. g \<in> bij(B,B\<union>{A})" sorry
lemma ad3: assumes "\<not>Finite(A)" shows "A \<approx> (A \<union> {A})" sorry
Now you can put the line proof - after the statement of lemma ad1 and try to express the first line of the informal proof (A is not empty, hence we can pick an element that belongs to A). Note the empty set is denoted 0 in Isabelle/ZF. The first line of the proof of this lemma might help you with the syntax you need.
Sławomir Kołodyńaski (May 15 2022 at 12:35):Small correction: ~ can indeed be used as a shorthand for \<not>.
Ulrich Schmid (May 15 2022 at 18:35):thanks a lot for the suggestions. I will go through them and then try again
Ulrich Schmid (May 22 2022 at 13:20):I have 3 further questions:
1) I made a copy of a program in Isabelle which works (see appendix Scratch.thy). But in the copy Isabelle does not give any feedback (see appendix Scratch1). The color of the font in the copy appears in pink. What could be the reason here?
Bildschirmfoto-2022-05-22-um-14.56.22.png Bildschirmfoto-2022-05-22-um-14.56.41.png
2)How can I find the best proving method for a given lemma (auto, blast, simp,...)?
3) There is a notation with pointed bracket for example:
lemma ad1: assumes "\<not>Finite(A)" shows "\<exists>B. B\<subseteq>A \<and> B\<approx>nat"
Isabelle makes a transformation without pointed brackets in:
lemma ad1: assumes "~Finite(A)" shows "∃B. B⊆A ∧ B≈nat" by blast
What does this mean and what is the best way to enter source code in Isabelle?
thanks for a feedback
Sławomir Kołodyńaski (May 22 2022 at 19:46):1) I don't know. It is good to set ISABELLE_LOGIC=ZF in the etc/settings file, but I am not sure if it is related to this. If you attach the Scratch1.thy file here I can check if it loads in my setup.
2) There are just a couple of them, the best one is the one that works. If several work, choose them in the order simp, blast, auto. Blast and auto are more capable than simp, but slower. There are assertions that blast accepts but auto does not and vice versa. Again it is very rare that a lemma can be proven just by "using assms by auto" or similar, usually you have to write a proof.
3) The notation with pointed brackets is what is in the source text i.e. in the file on disk. You can see that by looking at the file (like your Scratch.thy) with a word editor like Notepad. When isabelle loads such file it displays the markup as symbols. For example if it sees "\<exists>" it displays "∃". The "Predefined Isabelle symbols" section in Appendix of the Isabelle/Isar Reference Manual provides a list of symbols and the pointed bracket strings that correspond to them. When I want to enter such symbol in Isabelle/jEdit interface I type a couple of letters like \<ex and then wait a second or two for Isabelle to show a list of hints, from which I choose (with arrows and TAB) the symbol I want.
Ulrich Schmid (May 23 2022 at 17:47):here a the files Scratch.thy and Scratch1.thy
Scratch.thy
Scratch.thy
Scratch1.thy
Scratch1.thy
Ulrich Schmid (May 23 2022 at 17:53):Scratch is verified by Isabelle, but with Scratch1 there is no reaction. It is in both cases the same source code (Sratch1 is a copy of Scratch, "copy and paste").
Ulrich Schmid (May 23 2022 at 17:59):This problem has occurred several times with other files as well. It also happens sometimes that after a restart of Isabelle the files work again in Isabelle.
Sławomir Kołodyńaski (May 23 2022 at 18:17):Both files work fine in my setup (Linux). They are not identical: for example you have \<longrightarrow> t\<in>u \<and> u\<in>x in Sratch.thy and \<longrightarrow> (t\<in>u \<and> u\<in>x) in Scratch1.thy.
Ulrich Schmid (May 24 2022 at 10:55):Yes, obviously I changed something in the meantime in one of the two files with the attempt to get Scratch1 running. But if you compare both printscreans above the source code is identical.
My main question is the following: What can I do if a program does not run in Isabelle (in the example Scratch1, printscrean see above). Can this be due to the source code or rather to the system settings or hardware- system (MacBook Air)? You have mentioned "ISABELLE_LOGIC=ZF" in the etc/settings-file. How can I get access to this file?
Here is another example of this kind (Skratch2), where Isabell shows no reaction:
Scratch2.thy
Scratch2.thy
thankyou
Sławomir Kołodyńaski (May 24 2022 at 14:57):I am pretty sure the contents of the file is not the reason this happens. I only use Isabelle on Linux and I have not seen this, maybe such things happen on other platforms. In my setup the etc/settings file is in the directory where I unpacked the Isabelle2021-1_linux.tar.gz file that I downloaded from the Isabelle site. This can be any directory on Linux. I don't know where this file might be on MacBook Air.
Ulrich Schmid (May 26 2022 at 15:36):I noticed that after a restart Isabelle always processes only the first program. If I call further programs afterwards, these are not processed, i.e. Isabelle remains inactive. However, I can always call the first program again and edit it, and Isabelle reacts immediately.
I am of your opinion that this is due to the settings or the operating system, or the low capacity of my laptop. Is there something like a technical support for Isabelle?
Sławomir Kołodyńaski (May 26 2022 at 17:40):The Isabelle mailing list is the best approximation of that that I know of.
Ulrich Schmid (May 28 2022 at 19:15):I had an appointment with apple technical support today. It turned out that my system requirements are too weak for Isabelle. Therefore I will get a stronger system, which I had already planned independently. After that I will continue to work with Isabelle. Thank you very much for your support so far.
Ulrich Schmid (May 31 2022 at 19:06):I intend to buy a new laptop. Are there any differences between Microsoft and Macintosh regarding Isabelle, or are both operating systems equally suitable for it (performance, technical problems,...)?
Manuel Eberl (May 31 2022 at 19:10):I think both should be fine. I think most "power users" in the community user either Linux or Mac, but not due to any problems with Isabelle under Windows, and Makarius does make sure that all of these are equally well-maintained. (I for one have only ever used it in Linux).
I did hear, however, that the new ARM-based Macbooks do provide very good performance with Isabelle. But I for one think that you should just make your decision based on general personal preference.
Ulrich Schmid (Jun 30 2022 at 06:29):I received an error message when working in Isabelle (see attachment). What can I do?
Bildschirmfoto-2022-06-30-um-08.14.25.png
Mathias Fleury (Jun 30 2022 at 07:15):there is no error message, it just means that Isabelle is compiling HOL-Library. You have to wait until that finishes (compiling should happen only once)
Mathias Fleury (Jun 30 2022 at 07:16):I am just wondering how you triggered that because HOL-Library has nothing to do with ZF
Mathias Fleury (Jun 30 2022 at 07:17):You probably changed the base session in the theories panel (right on the screenshot: you have set HOL-Codegenator_Test). Just set it back.
Ulrich Schmid (Jun 30 2022 at 08:45):Thanks, obviously I accidentally clicked that.
Ulrich Schmid (Jul 06 2022 at 05:32):After a short break, I am now continuing to familiarize myself with Isabelle. Therefore I start with very simple examples. In the Scratch5 file I have formulated two lemmas (hyp0 and hyp1, see attachement). The first lemma is true and follows directly from the axiom of infinity. The second lemma, however, is false in ZFC, since it contains the expression "y∈y", which contradicts the axiom of foundation. However, both lemmas are verified by Isabelle. I suspect the reason is that Isabelle/ZF considers each entity as a class. My first question now is whether I am guessing correctly here and my second is how to tell Isabelle to consider all entities in my theory file as sets (y∈V).
Scratch5.thy
Manuel Eberl (Jul 06 2022 at 06:42):When I run this, neither of the two are proven. Note that as long as the by blast bit is purple, the corresponding proof method is still running and the theorem is not to be considered proven yet.
This is because Isabelle forks proofs into separate threads in the background to make processing faster, and to allow for more convenient interactive editing. If you were to try to build this theory in batch mode, you would get an error (or rather, the build process would run forever).
Manuel Eberl (Jul 06 2022 at 06:48):Here is a proof for your first theorem and a proof of the opposite of your second theorem.
lemma hyp1: "∃y. ¬Finite(y)"
using nat_not_Finite by blast
lemma hyp2: "y ∉ y"
using mem_not_refl by blast
I don't know anything about Isabelle/ZF, but I found the relevant lemmas with find_theorems (you can also use the "Find Theorems" panel in Isabelle/jEdit).
Manuel Eberl (Jul 06 2022 at 06:48):Unfortunately, Isabelle/ZF doesn't have sledgehammer. Otherwise I'm sure sledgehammer could have found those easily.
Manuel Eberl (Jul 06 2022 at 06:49):Unless your goal is specifically to do something with ZF(C), you should really look at Isabelle/HOL instead. Even if your goal is ZF(C), it might make sense to do some Isabelle/HOL first.
But I don't know what you're trying to do exactly, so I cannot say for certain.
Ulrich Schmid (Jul 12 2022 at 08:23):I am mainly interested in set theoretic statements in ZFC, so called wff's (well formed formulas).
For example A:="∀n∃x∀t∃u (t∈x ⇒ n∈t∧t∈u∧u∈x)"
The statement A here says that for every set n there is an infinite set x with n∩x = ⌀.
On the one hand, the focus is on simplifying such wff's equivalently (e.g., fewer variables or logical connectives). On the other hand, it is also about showing that two wff's represent the same content (A <=> B).
My hope is that I can use Isabelle to support this.
Ulrich Schmid (Aug 07 2022 at 07:28):Since a few months I have a new MacBook Pro with 16 GB memory and 10 CPU cores. The battery usually lasts a long time, but when I work with Isabelle, the computer gets very hot after a short time and the battery indicator goes down quickly. I have the impression that Isabelle is constantly working intensively in the background with large amounts of data. What can I do here?
Lawrence Paulson (Aug 14 2022 at 17:28):Isabelle certainly makes your computer work hard, so you don't have to. However, if you are doing nothing, it should also be doing nothing. If you've loaded dozens of large theories, things might get sluggish. Also if a proof above the point your looking at is in a loop.
Ulrich Schmid (Aug 18 2022 at 19:54):Thanks for your feedback.
I would like to prove simple statements in Isabelle using the ZF axioms. I also succeeded with the statements basic1, ... ,basic4 (see below). All four statements are direct consequences of the axiom of foundation and are accepted by Isabelle with "using foundation by blast". But the statement basic5 is not accepted, although the proof in ZF is quite analogous to the other statements. What could be the reason for this, or what must be added here?
theory Scratch2
imports ZF
begin
lemma basic1: "∀x. x∉x"
using foundation by blast
lemma basic2: "∀x y. x∈y⟶y∉x"
using foundation by blast
lemma basic3: "∀x y. x∈y⟶x≠y"
using foundation by blast
lemma basic4: "∀x y z. x∈y∧y∈z⟶x≠z"
using foundation by blast
lemma basic5: "∀x y z. x∈y∧y∈z⟶z∉x"
using foundation by blast
end
Sławomir Kołodyńaski (Aug 19 2022 at 17:02):The reason is that the statement exceeds Isabelle's "blast" method capabilities for automatic proof search. The only way to fix this is to write a more detailed proof (assuming the assertion is true). If you were to explain to someone how the basic5 assertion follows from the foundation and perhaps some other axioms, what would you say?
Ulrich Schmid (Aug 19 2022 at 18:05):The proof is not very difficult (indirect):
Assuming z∈x holds under the condition x∈y∈z, we consider the set A={x,y,z} (analogous to the proof of lemma basic2, with A={x,y,}). Case analysis for x, y, and z yields a contradiction to the axiom of foundation, for all three cases. The set
A={x,y,z} always exists for any three sets x,y und z. This fact follows from the axiom of replacement. Or alternatively, with the help of the axioms of pairing and union.
Tanks a lot for your feedback
Sławomir Kołodyńaski (Aug 20 2022 at 07:34):Probably the part with considering A={x,y,z} has a bit of creativity in it that blast is too weak for. The following works:
theory Scratch3
imports ZF
begin
lemma basic5a: assumes "x∈y" and "y∈z" shows "z∉x"
proof -
let ?A = "{x,y,z}"
have "?A≠0" by auto
with assms show "z∉x" using foundation by blast
qed
lemma basic5: shows "∀x y z. x∈y ∧ y∈z ⟶ z∉x" using basic5a by blast
end
Yes, now it works, thanks.
Is there a possibility to prove statements like basic5 without isar, e.g. only with a suitable tactic (blast, auto, best, simp,...) involving suitable lemmas? This could also prove certain generalizations of statements like basic5, for example, "∀x y z u. x∈y ∧ y∈z ∧ z∈u⟶ u∉x" etc, without having to change the proof ( in this case A ={x,y,z,u}).
This aspect would be very interesting, since it would then be possible to prove or disprove statements (wff`s) that are in a similar context, even without having a proof idea in advance. In the case that Isabelle confirms the truth of a statement one can then try to find a proof (if Isabelle does not deliver one). Also to simplify statements this would be a great help.
Sławomir Kołodyńaski (Aug 20 2022 at 17:37):It is possible to put a each step of a proof into a lemma so that the keyword "proof" is never used. In the above case it would look like this:
theory Scratch4
imports ZF
begin
lemma basic5a: shows "{x,y,z} ≠ 0" by auto
lemma basic5b: assumes "x∈y" and "y∈z" shows "z∉x"
using assms basic5a foundation by blast
lemma basic5: shows "∀x y z. x∈y ∧ y∈z ⟶ z∉x" using basic5b by blast
end
However, formulating such lemmas is like writing proofs, except with more typing and less clear structure for longer proofs. The only advantage of such style that I can see is that each proof step has a name, so you can reference it while proving something else. Isabelle is only designed to verify proofs you know in advance. It does not work well as an oracle telling you if a given assertion is true or false. Isabelle/ZF can tell you that something is true if it is simple enough but it cannot disprove a statement, it can only fail to accept it.
Ulrich Schmid (Sep 02 2022 at 11:02):Since Sledgehammer is not available in Isabelle/ZF, I would like to transform some questions from ZF (including all ZF axioms) to Isabelle/HOL to prove them there. For this purpose, a two-digit predicate P(a,b) is defined for the element relation. For a∈b in ZF we write P(a,b) in HOL. The ZF axioms are defined as properties of P in HOL. For example, the axiom of the empty set in ZF (∃x∀t ¬t∈x) provides the first property for P in HOL: ∃x∀t ¬P(t,x). Thus, all ZF axioms can be transformed to HOL very easily. In this way, very special questions within set theory can then be transferred to HOL in order to prove them there. Is this procedure in principle reasonable and possible?
Mathias Fleury (Sep 02 2022 at 11:16):I did remember that correctly, but deleted the message: what you describe is done in HOL-ZF right? https://isabelle.in.tum.de/dist/library/HOL/HOL-ZF/index.html
Ulrich Schmid (Sep 03 2022 at 12:36):If in HOLZF all contents from Isabelle/ZF can be described, then it corresponds to my idea. The inversion does not apply of course. I will look at the whole thing and try to understand the main points, which are interesting for me.
Ciarán Dunne (Sep 09 2022 at 21:31):Paulson's ZFC in HOL is good too. Very powerful!
https://www.isa-afp.org/entries/ZFC_in_HOL.html
Last updated: Dec 21 2024 at 16:20 UTC