ProofTools: development update of 2019-02-09

• << The ProofTools homepage
• >> The ProofTools manual
• >> The ProofTools background and technical addendum page
• >> The feature comparison of free proof tree software

Wow. It has a been a long time between ProofTools releases, and even a long time between updates to the ProofTools home page - the last one was a bit over four years ago! I have been prompted to get back to work on the code though due to a recent bug report on what I am going to refer to as the "branching modal logic with necessity" bug. This is in addition to the "infinite branch detection" bug whose first announcement goes back to 2014.

Because these bug descriptions will be removed from the main page once they are fixed, I am copying here their descriptions from that main page:

1. The "infinite branch detection" bug

   The infinite branch detection algorithm (see also its documentation in the manual) that Emil and I developed for ProofTools is flawed: it gives the wrong results in certain cases. The simplest example of which I'm aware is the formula (entered as a premise) ∀x(∃y(Ry∧¬Rx)). The proof tree built from this formula should close, however, ProofTools incorrectly marks it as infinite. Because predicate logic is considered to be undecidable due to the separate efforts of Alonzo Church and Alan Turing in solving the Entscheidungsproblem - a fact I learnt only after developing our algorithm - a perfect infinite branch detection algorithm for it does not exist. I also learnt through the author, Graham Priest, of the text on which ProofTools is based though that predicate logic with monadic predicates is decidable, so, potentially this algorithm can be fixed such that it works on, and is applied solely in the case of, monadic predicates. That, however, remains on the TODO list. Also on the TODO list is researching any other limited areas of predicate/modal logic upon which infinite loops can be detected mechanically.

   What this bug means for you: If ProofTools marks any branch as infinite, ProofTools might be wrong, and the branch might actually close. Thus, any formula (conclusion) / argument deemed by ProofTools to be NOT a logical truth / valid argument due to infinite branches might in fact BE a logical truth / valid argument. If, however, ProofTools doesn't mark any branches as infinite, then this bug does not apply, and as far as we know the results that ProofTools gives can be trusted other than for the next bug listed below.

2. The "branching modal logic with necessity" bug

   Some modal trees give the wrong result. A known example is when □(P∧Q) is entered as a premise, and □P∧□Q as the conclusion: ProofTools determines this argument to be not valid when it is actually valid. The semi-technical details: This bug is essentially due to certain data being maintained on a universal (per-tree) basis when they should be maintained on a per-branch basis. Those data are the list for each "necessity node" of world numbers for which the necessity rule has already been applied to that node. Because world numbers are reused across different branches (i.e., world number "1" could appear, but refer to a different "world", in both branch one and branch two), this means that sometimes the necessity rule is not applied in other than the first branch for a given world number even though it should be applied on subsequent branches. The working fix in the development code: As for constants (in predicate logic), ensure that world numbers are unique across the entire tree, rather than only per-branch. In other words, ensure that, other than for the original/default world number "0", world numbers are not reused across branches.

   What this bug means for you: If ProofTools marks any tree containing branching modal logic and one or more necessity operators as not valid, or as non-closing, ProofTools might be wrong, and the tree might actually BE valid or close. This bug does not affect trees which do not contain modal logic operators (necessity, □, and possibility, ◊). It also does not affect trees which, whilst containing modal logic operators, either do not branch or do not contain necessity operators (or both).

As indicated, the second bug is already fixed in development code. I had written some plans for addressing the first bug back in 2014, which involved first confirming for myself the results of Church and Turing in solving the Entscheidungsproblem, then investigating carefully the extent to which predicate and modal logic are undecidable, and following from that the scope within which they are decidable, from which a genuinely reliable detection algorithm could be based - where it was possible to apply it. I have not, however, undertaken that confirmation and investigation, and it does not seem likely that I will do so any time soon. Thus, my plans for the next release with respect to that original bug, slightly revised from the original 2014 plans, are to disable infinite branch detection entirely, and, instead, to offer the user two means of avoiding infinite loops:

1. Augment the existing "Step" button with an integer input to stipulate the number of rule applications to apply at each step, defaulting to one.
2. Show a box/window upon clicking "Show Proof" or "Step" which indicates progress (total number of nodes in the tree so far) as well as providing a "Stop" button to halt decomposition of the tree at the point at which it is at. Also shown will be a toggle box labelled "Stop on first open branch (i.e., first branch with a counter-model)".

Because I am currently away from home with limited access to power points in which to plug my laptop's power cord, and because I am without the convenience of my home dual-monitor + external keyboard & mouse setup, I might not be able to get all of this sorted before returning home, which I hope but can't be sure will be within the next fortnight. I can't, then, commit to a date for the next release, but it will hopefully be well within a month. [Update of 2019-02-16: it turned out to be a little under a week. ProofTools version 0.6 can now be downloaded from the home page.] Whilst it won't fix any of the various limitations of the code currently listed on the project's home page, it will fix the two serious bugs and at least one out of the two minor bugs currently listed (those bugs being an incorrect tooltip (popup hint) for the "T" shortcut button - fixed in development code - and the bug by which extraneous parentheses are sometimes added under parentheses normalisation - which probably won't be fixed for the next release).

I hope that this provides some useful information for those who in turn find ProofTools to be a useful piece of software. Please feel free to contact me about ProofTools to share any feedback that you might have, and especially to report bugs.