Kalish & Montague (1964) in Prolog?

Lets say we want to build a little web site. And present a THINKER
that helps us in finding propositional proofs or even FOL proofs,
just like here (not same meaning of heuristic as in A* search):

Heuristic Theorem Proving
Pelletier & Wilson, 1983
https://www.sfu.ca/~jeffpell/papers/PellWilsonThinker83.pdf

How would one go about it and solve this problem in Prolog?

1 Like

Ok lets try this here:

Difference to the paper we don’t render “show” statements
at the top of a Fitch box, we render the formula at the
bottom of a Fitch box.

Besides that, it might be also not strictly Kalish & Montague in
terms of the used proof figures. If you don’t mind a
little ASCII art:

:- show((((p=>q)=>p)=>p)).

image

Its an itch shorter than this proof here from The Logic Book
found on https://carnap.io/ because I don’t show
Repetition (R) steps:

a65199db814659289deee62718185db850c5ea11

I just noticed that there is a defect in your Fitch style proof that should be corrected because there is something unsound in the expression of introduction rule:

image

The trouble is that line 6 does not show that assumption 1 is discharged. It means that a vertical bar should be before assumption 1 and another one before assumption 2, because these two assumptions are discharged. We should see:

  1. | d(a) [assume]
  2. | | [assume]
  3. | |
  4. | |
  5. | ← discharge of assumption 2.
  6. d(a) → … [imp(1-5)] ← discharge of assumption 1: block 1-5 is a sequent from conditional 6 is inferred…

Even if flags are not used, but only vertical bars, discharges must be expressed clearly, that is one of the most obvious merits of Fitch’s style, in comparison of Gentzen’s. You can check my claim in reading Richard Kaye’s excellent book, The Mathematics of Logic, CUP, 2007. This point also explains the distinction in carnap.io between Premiss (notation " :PR ") and Assumption (notation " :AS " ): the latter is discharged, the former not : https://forallx.openlogicproject.org/html/Ch17.html#S4

As far as I know, genuine Fitch style correspond to your variant 2: discharge is expressed by a step back, and it is nice.

The result is nice, indeed. Can you explain why (![N-X]:A) and (?[N-X]:A) lead to enter ![ x ]: and ?[ x ] : as input respectively ?

Does exist a book where lambda calculus and related topics are explained in a simple and pedagogical way? As soon as I see the symbolism of lambda calculus, I do not even try to understand because it is too much abstract for me…

(post deleted by author)

Thanks for sharing. I’ll make test and I’ll share feedbacks.

(post deleted by author)