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):

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:

| d(a) [assume]

| | [assume]

| |

| |

| ā discharge of assumption 2.

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

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ā¦