Closed Jean-Luc-Picard-2021 closed 1 year ago
Or maybe fork the web site to start a set theory branch?
A model finder could generate finite set theory models, like Ackerman encoding or whatever. And some ZFC without the axiom of infinity, could parallel it by proof search,
but this proof search might be difficult to implement? I guess already the model search for FOL is not complete, since FOL is not decidable, so the approach would be the same.
The GNU license would allow some forking right? I am not saying I have the resources to do it, just curious. Also I don't have a clear picture how to deal with the conflicting
situation that quickly a few axiom of set theory already force an infinite model. Possibly I would first start experimenting with a Peano model finder, where some infinite models
are sought that can be finitely represented.
These are natural ideas, but I don't think I will ever tackle them. The textbook-style tree format that my prover tries to generate is inefficient for reasoning within substantive theories like ZFC or PA. For this kind of task, it is better to use more powerful provers like E or Prover9, or (even more powerful) proof assistants like Isabelle or Lean.
Currently I am using your tree tool, by just adding instances of ZFC axioms in the premisses, thus helping the tool a little. I do the guess of the formula in the axiom of separation
and axiom of replacement, and your tool does the rest. Works pretty well so far for small scale problems. It works well when generating a proof,
but counter models naturally don't look so good. There is monotonity what is a proof from IN (some instances of ZFC axioms) is also proof from ZFC. But for counter models
this doesn't work, quite a dilemma. E and Prover9 are only provers. Mace4 would be a model finder. Isabelle has Nitpick and some successors, which are also model finders. These tools
don't come as a websites where you can share links.
Somehow I still miss the ∈ operator. It would allow me to more easily compare your tree tool with what I am currently backing. For example I get:
/* Problem from Set Theory */
?- time(prove0('∀p∀q(∀x(x∈p⇔x∈q)⇒p=q) ∧ \
∀x(x∈u⇔r(x)) ∧ \
∀x(x∈v⇔r(x)) ⇒ \
u=v', 6, unicode)), !.
% Wall 4902 ms, gc 7 ms, 1830308 lips
The same works also in your tree tool when I encode x∈y as Exy. Thats quite interesting that the above theorem is agnostic to any further backround set theory and is purely logical:
(∀p∀q(∀x(Exp <=> Exq) => p=q) & (∀x(Exu <=> rx) & ∀x(Exv <=> rx))) => u=v is valid. https://www.umsu.de/trees/#~6p~6q(~6x(Exp~4Exq)~5p=q)~1~6x(Exu~4r(x))~1~6x(Exv~4r(x))~5u=v~1~6x(Exu~4r(x))~1~6x(Exv~4r(x))~5u=v)
I agree that having at least a few infix operators (e.g. +, -, *, >, maybe even ∈) would be convenient for some kinds of queries.
Since yesterday I have a new prover of my own running with ∈ syntax. But it will not produce a tableaux proof, rather a natural deduction proof:
/* Drinker Paradox, formulate with Sets */
17 ¬ ∀x: ¬ (x ∈ d ⊃ ∀y:(y ∈ d))
▶ Conclusion 1,16
https://qiita.com/j4n_bur53/items/55b5678826ee74e05bff
Should I close this ticket? I was wondering whether I could fork your tool, and add ∈. But then I saw it needs PHP. Is this required? Is there some server roundtrip?
The above thingy needs no server, works completely in the browser. But it features not yet a model finder, only a proof finder for FOL. Disclaime: I don't endorse
Drinker Paradox formulated with Sets, it rather skews the Drinker Paradox a little bit.
Nice work.
I use PHP to minify the source (on the fly) and to turn debugging options on and off.
Would it be possible to have more infix operators? Recently the tool introduced = , which gave it a nice boost, since its also supported by the
proof search and the model finder. I wonder whether it would be possible to also introduce an infix operator ∈, so that one can write x∈y.
I am currently writing Exy. Unfortunately I don't know how to extend the proof search and the model finder, many things work already with the existing
proof search and model finder, for example FOL is already able to derive a lot of theorems that talk about x∈y without invoking anything from a set theory such
as for example ZFC. So the syntax would be already useful only on the surface, without adding something to FOL.