What is the Normal Form of Proofs in Intuitionist Logic?

I came across the concept of a normal form of proofs in Neil Tennant's A New Unified Account of Truth and Paradox (2015). I did a quick scan on SEP, and it seems to be a concept specific to his intuitionist logic, Core Logic, although I'm not sure if this is the case.

Questions:

1. What is the normal form of proofs in intuitionist logic?
2. What is the general difference between a proof in normal form vs a proof not in normal form? What is its logical significance (why does it matter, to a logician, if a proof is in normal form)?
3. What is the philosophical significance?

Tennant seem to say that a canonical proof must be in normal form (or normalizable) for the proof to warrant assertion (by my paraphrasing: "for the conclusion to be True (given the premises)", although this might not be accurate).

I'll expand on (3) by giving a brief argument Tennant gave in his paper (although I still feel like there is something wrong with the argument, hence why I asked (1) and (2)). Tennant says that a proof of ⊥ given the Liar sentence is not in normal form, so the Liar sentence does not pose any problem in his theory of truth. Here is the argument:

First, consider these two reductions:
¬-Reduction:
Avoiding Prolixity:

Now, regarding the Liar sentence, consider these two derivations (note that l here is a sentence name, not a proposition):
⊢ ¬Tl

¬Tl ⊢ ⊥

Because Π proves ¬Tl, we should be able to insert it in relevant places in Σ to get a derivation of just ⊢⊥ (so to avoid using cut). Hence we have:
abbreviated as

Looking at the last line of Π, we see that it matches the left side in ¬-Reduction. The right side of ¬-Reduction matches the subtree starting with Ω. So we can perform the reduction and get:

But Ω contains Π in a way that we can perform Avoiding Prolixity reduction, so we get:

Hence it has no normal form.

I'm still quite puzzled if the reduction are applied correctly, and I have this intuition that if we get rid of abbreviations, the proof should be in normal form.

• This was answered on Math SE. Normal form goes back to Gentzen, who proved that intuitionistic proofs can always be put into normal form, i.e. rid of so-called detours with redundant introduction/elimination steps. Its significance to studying complexity of proofs is discussed in SEP. Commented Apr 4 at 1:59
• @Conifold thanks for the link! Commented Apr 4 at 3:40
• A normalized proof is also closely related to the concept of a cut-free proof in natural deduction. Commented Apr 4 at 14:12
• @Bumble That makes sense with the liar proof! Commented Apr 4 at 14:53

@conifolds linked answer is good. Let me provide a complementary perspective. By the curry-howard correspondence,

1. a normal form is a lambda term that can no longer be reduced. if we associate lambda terms with programs, a normal form is a program that we have finished running. (See Troelestra Basic Proof theory, ch1)

2. terms/proofs in normal form may admit nice properties, or nice theorems. The simply typed lambda calculus is strongly normalizing, that is, all terms normalize. This implies that STLC is not turing complete. for ND normal form proofs (without disjunction), assumptions are followed by elimination rules are followed by intro rules.

3. this special structure of intuitionistics ND proofs is closed related to dummett's "fundamental assumption", which features in his project on proof-theoretic semantics. (See IEP or SEP on Dummett, or proof-theoretic semantics)

As for your problem: the reductions are fine, the abbreviations do no work. We are always able to apply a reduction rule, abbreviation or not, hence the proof can never be in nf. In the lambda calculus, the liar paradox is "the" Y-combinator, perhaps it will help to google why Y- combinator has no normal form.

• thanks for the answer! I think I follow the parts about lambda calculus. Why is the Liar paradox the Y-combinator in lambda calculus? I get that it has no normal form. Is that the only reason? Commented Apr 4 at 3:51
• its informal, but the y combinator applies itself to itself, somewhat like the liar. its reduction sequence is such that it reduces to itself, much like what you have above. thats mostly it Commented Apr 4 at 4:07
• Hmm, well from the CH correspondence, seems like we could have a type (probably in CoC?) corresponding to the liar sentence where its inhabitant has no normal form. I’m curious what that type and program is, exactly Commented Apr 4 at 4:34
• Coc should also be strongly normalizing so probably no consistent type assignment for same reason as stlc. The program would be straightforward to obtain if tennants logic is nice under the ch correspondence Commented Apr 4 at 4:40
• lambda calculus is the implicational fragment of ND by CH. For a fuller ND under CH, look at Troelestra BPT, I think he sketches it out with quantifiers as well. Of course, the correspondence is not as "nice", or "natural". so, (again, I'm not familiar with Tennant's work), if Tennant does everything in the usual manner, proofs/derivations will correspond to terms Commented Apr 4 at 16:42