Erratic behaviour for first order formula

[mereolog]

First, great work - really enjoyed it.

But sometimes the online tool behaves erratically. For example, when I ran it for ¬(∀x¬R(x, x) ∧ ∀x∀y∀z(R(x, y) ∧ R(y, z) → R(x, z))∧ ∀x∃yR(x, y)), the first result says, incorrectly, that is a valid formula and starts a tree for it. Only when you run for the second time, the generator seems to get into an infinite process, as it should.

[wo]

strange! Thanks, need to investigate.

[eggleaves]

I was intrigued by this result because there have been two or three times in the last four or five months when I thought my elderly eyes were playing tricks on me or perhaps my clumsy use of an android tablet seemed to have produced inconsistent behaviour.

Pawal’s example reminded me of inconsistent compiler behaviour to do with memory initialisation that was a common mainframe problem 40 to 50 years ago.

I am too feeble to debug this much JavaScript so I hope you won’t waste time on my comments. But just in case below is a screenshot of a first iteration on an iPad which did not indicate a valid formula, rather a countermodel. However it is not reproducible or at least not easily so far. Unlike my usual habit of using an android tablet this time I also tried a chrome OS tablet and an iPad iOS tablet. In one case the iPad produced a valid conclusion on the first iteration but with 6 lines above the “save as png” text rather than two. Stupidly, I didn’t take a screenshot.

There is a chance I am wasting your time by mentioning this so apologies if that is so. I can’t help but wonder whether the traditional JavaScript behaviour which has somewhat been alleviated in the last few years might be involved, where are the value of some variable is not initialized in a local code block but is obtained from global storage, giving seemingly random behaviour.

Anyway, here is the screenshot:

Just out of curiosity

On Wed, Oct 21, 2020 at 2:11 PM Wolfgang Schwarz notifications@github.com wrote:

strange! Thanks, need to investigate.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/wo/tpg/issues/4#issuecomment-713879751, or unsubscribe https://github.com/notifications/unsubscribe-auth/AQFR67E6A3O2O4YFSLLRI63SL5E7JANCNFSM4S2CFA3A .

[wo]

Thanks @eggleaves -- this does sound relevant. Unfortunately I can't see your screenshot. Can you try attaching it again?

[eggleaves]

Sorry, trying iPad attach again...

On Thu, Oct 22, 2020 at 12:30 AM Wolfgang Schwarz notifications@github.com wrote:

Thanks @eggleaves https://github.com/eggleaves -- this does sound relevant. Unfortunately I can't see your screenshot. Can you try attaching it again?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/wo/tpg/issues/4#issuecomment-714292821, or unsubscribe https://github.com/notifications/unsubscribe-auth/AQFR67AOJSVX7UFAAPID6DLSL7NQFANCNFSM4S2CFA3A .

[eggleaves]

(Trying attach again without ipad image attach)

[feggleaves]

[feggleaves]

Now that I have figured out how to paste a screenshot to github, here is one that shows a putative proof that Pawel’s formula is “valid”. It seems to be reproducible with the following steps:1) load umsu.de/trees 2) paste the formula into the input area 3) backspace over the leading negation symbol, deleting it 4) Run giving an “invalid” conclusion 5) insert the deleted negation, giving the original formula 6) Run.

[wo]

Great, very interesting. I'm currently too busy with teaching and marking to dive into this, but I'll get to it soon.