adamdejl / pithosnd Goto Github PK

Hi Adam,

First, thanks for making this. It's the only open source Fitch style proof-checker I found with support for both function symbols and equality.

I seem to have found a problem with substitution when function symbols are involved. There is no way to complete the proof

1. m = n  given
2. <empty line>
3. f(m) = f(n) goal

Selecting =sub results in an error message. I have tried introducing f(m) = f(m) using refl in order to have the necessary number of lines for =sub, but apparently the system doesn't recognize that f(m) actually has an m in it...

Best wishes,
Cezar

Hi,

When trying to apply ⊥I, I get the message "The justification formulas are not a formula and its negation.". For instance, in the following proof

I was selecting lines 2, 5, and 7. After clicking "OK" I tried again, with the same lines, and it worked. Same story then after introducing P ∨ ¬P in line 9. First it doesn't work, then it does.

Sometimes I needed to repeat the selection several times before it worked, and other times it didn't work at all, although all cases were of a formula and its negation.

Many thanks for your help!

Best wishes,
Cezar

Dear Adam,

I'm having problems with the universal introduction form. For example, I'm trying to prove ∀xQ(x) from the premiss ∀x(P(x) ∧ Q(x)). When I select the goal and click on ∀I, I get a box with "x" as the goal, instead of ∀xQ(x) (see attached image). I am then unable to prove "x".

Any suggestions for how to deal with this? Many thanks for your help!

Best wishes,
Cezar.

Dear Adam,

I can't seem to get vE to work. For example:

1                A ∨ B                given                              
2                B → A               given                              
3                <empty line>                                              
4                A                       <goal>

Selecting 1 and 3, and entering "A" as the intended goal, doesn't produce anything. The two lines remain selected, as does the vE rule. Selecting 1 and 4 results in the error message "No target (goal or empty) line has been selected.", which is strange, since 4 is obviously a goal line.

Trying an even simpler example:

1     A ∨ A             given
2     <empty line>                                              
3     A                   <goal>

Selecting lines 1 and 2 results in the following:

An error occured during application of the rule ∨E:

Processing of the proof failed in an unexpected way. Please contact the developer stating the actions that you performed. Sorry... Cause: Failed to extract selected proof line(s).

Please let me know if you need additional information. Thanks for your help!

Best wishes,
Cezar