# 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)).
``````

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:

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:

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)