2
$\begingroup$

This might have been asked before, but certainly I don't find any source. Even in the literature I've consulted, there is no such proof so far.

Context

In the context of the simply typed lambda calculus (say with just one base type $\iota)$ there are judgments of the form $$ \Gamma \vdash t : \sigma $$ denoting $t$ has type $\sigma$ under the environment (or context) $\Gamma$. Via proposition-as-types, this can also be read as $\sigma$ (as a implicational first-order formula) follows from the assumptions $\Gamma$.

In this sense, simply typed lambda calculus is a calculus for (the implicational fraction of) first-order logic. But not for the classical but for intuitionistic logic.

This especially means that Peirce's law is not a theorem. So, for any types $\sigma, \tau$ it is not the case that there is term $t$ such that $$ \vdash t : ((\sigma \to \tau)\to \sigma)\to\sigma $$

Question

In short: How to prove this? The point is, I've found a few proofs which involve models for $\lambda$-calculus or intuitionistic logic -- which is fine, but I'm rather interested in a proof by syntactic means. Peirce's law shouldn't hold syntactically either, or?

The proof might involve confluence, subject-reduction, normalisation even... any ideas?

Thanks in advance!

$\endgroup$
  • 1
    $\begingroup$ Yes; usually a proof of "underivability" uses semantics. The calculus (e.g. that for intuitionsitic logic) is sound and complete for the corresponding semantics : e.g.BHK-interpretation and Kripke's semantics. Peirce's law is not valid : a semantical counter-example is produced. Therefore, it is not derivable. $\endgroup$ – Mauro ALLEGRANZA Mar 21 at 8:09
  • 2
    $\begingroup$ Okay, but do you know of a proof which does not involve semantics? $\endgroup$ – aphorisme Mar 21 at 9:21
3
$\begingroup$

You are right in your intuition that proving that a derivation does not exist is somewhat cumbersome. Soundness and completeness of formal proof systems provide us with an interesting duality:

$\vDash \phi \Leftrightarrow$ all models satisfy $\phi$ $\Leftrightarrow$ there exists no model that does not satisfy $\phi$
(soundness) $\Leftarrow$ $\Rightarrow$ (completeness)
$\vdash \phi \Leftrightarrow$ there exists a derivation that proves $\phi$

$\not \vDash \phi \Leftrightarrow$ not all models satisfy $\phi$ $\Leftrightarrow$ there exists a model that does not satisfy $\phi$
(completeness) $\Leftarrow$ $\Rightarrow$ (soundness)
$\not \vdash \phi \Leftrightarrow$ there exists no derivation that proves $\phi$ $\Leftrightarrow$ all potential derivations can not prove $\phi$

Proving a universally quantified statement ("all") is often an awkward thing to do because you need to make an argument that any entity from a possibly infinite domain (such as any structure or any possible derivation) has the desired property (such as (not) satisfying or (not) proving a formula), while proving an existentially quantified statement ("there is") is very easy, because it suffices to just provide one example (one counter-model/one proof) and you're done.

So if you are supposed to show $\vDash$, rather than making a possibly cumbersome semantic argument about validity in all models, soundness and completeness allow as to show $\vdash$, i.e. provide one syntactic derivation that proves the desired formula.
One the other hand, showing $\not \vdash$, i.e. arguing that there can be no derivation can be annoying, but soundness and completeness enable us to just show that $\not \vDash$ holds by providing one counter-model and you're done.

So the easier way to show that $\not \vdash t: ((\sigma \to \tau) \to \sigma) \to \sigma)$ would be to provide a semantic argument that shows that there are models of typed $\lambda$-calculus/intuitionistic logic in which the formula $((\sigma \to \tau) \to \sigma) \to \sigma)$ does not hold. A semantics for intuitionistic logic is e.g. Kripke semantics.
If you are, however, interested in syntactic proof, you need to make an argument that no syntactic derivation is possible, i.e. any attempt to prove the formula will eventually lead to a dead-end where it is not possible to continue the proof, and you need to reason why.


So let's attempt to build up a derivation tree:

enter image description here

The only reasonable way to start (bottom-up) is to first (un-)do an implication introduction to get rid of $((\sigma \to \tau) \to \sigma)$: Implication elimination would require an even larger major premise and a suitable minor premise$^1$, and introducing a new variable is not an option because the set of assumptions (the left-hand-side of the sequent) has to be empty in the conclusion formula.
The next reasonable step after $(\to I)$ is to make use of $x: ((\sigma \to \tau) \to \sigma)$ - which can in turn be derived by one application of the identity rule - to show $x(\lambda y.M): \sigma$ by an application of $(\to E)$, which requries a proof of the antecedent, $\lambda y.M: (\sigma \to \tau)$.
With a similar argument as in the first step, the only useful continutation for the latter node is another $(\to I)$, which adds $y: \sigma$ as a new assumption, and we now have to prove $M: \tau$. This is the point were we get stuck.

The first observation is that we can't use $(\to I)$ anymore because $\tau$ is not a function type.
Simply adding $\tau$ to the context, i.e. introducing a new variable $z$ which has the type $\tau$, and closing the branch with $(Id)$ is not an option either, because we would need to carry this additional assumption down the tree, and end up with the sequent $z: \tau \vdash \lambda x.(x(\lambda y.z)): ((\sigma \to \tau) \to \sigma) \to \sigma$, with a context containing $z: \tau$ instead of being empty. So we would not have a proof (= a derivation of the form $\vdash t: \alpha$, with no assumptions on the left-hand side of the sequent), but instead the derivability of the type would depend on the stipulation of some variable $z$ being declared to have the type $\tau$. But then our term would contain a free variable, which does not solve the type inhabitation problem: That for any type $\alpha$, we could find a trivial "inhabitation" of the form $x:\alpha \vdash x:\alpha$ is uninteresting - instead, type inhabitation asks about the existence of a closed term.
So alternatively, we could attempt to introduce new declarations of the form $... \to \tau$ to the context, and continue the tree by an application of elimination rules; however this would merely shift the problem upwards the tree:
If we chose $\ldots \vdash \sigma \to \tau$ as the major premise with $\ldots \vdash \sigma$ (derived by an application of the $(Id)$ rule) as the minor premise to the $(\to E)$ rule, an endless loop would occur, since a similar rule application is already used one step lower in the tree. The fact that the context now in addition contains $\sigma$ does not make a difference in this case.
If we chose $\vdash \tau \to \tau$ as the major premise to the $(\to E)$ rule, another endless loop would occur, since the other branch (the minor premise) would need to contain $\vdash \tau$ with the same context again. And introducing new type variables different from $\sigma$ and $\tau$ wouldn't help either, but only leave us with even more to prove.

So there is no way to continue the upper right branch of the derivation tree, and at no point could we have made a smarter choice by selecting a different rule.
Since the tree can not be resolved, the type is not inhabited.

As you see, proving that a formula is not derivable can be rather cumbersome, because you need to make sure that every way of trying to build up a tree will eventually fail - I hope my proof was comprehensive enough in this respect.


Another thing you might find interesting w.r.t. to the correspondence to the $\{\to\}$-fragment of intuitionistic logic: The formula $(((((\sigma \to \tau) \to \sigma) \to \sigma) \to \tau) \to \tau)$, i.e. the above formula with two succedents $\tau$ appended, is deriavable/inhabited. This formula represents the double negation of Peirce's law (under the assumption that $\tau$ stands for $\bot$, and $\neg \neg \phi$ is seen as an abbreviation of $(\phi \to \bot) \to \bot$). This formula can be derived in intuitionistic logic, and in particular in the $\{\to\}$-fragment, i.e. in positive implication logic.$^2$ Thus, the type $(((((\sigma \to \tau) \to \sigma) \to \sigma) \to \tau) \to \tau)$ is inhabited (take $\alpha$ for $\sigma$ and $\beta$ for $\tau$):

enter image description here

An inhabitant (a $\lambda$-term) corresponding to this type (formula) would be $\lambda x.(x(\lambda y.(\lambda z.x(\lambda y.z)))$. You see that the part $\lambda x.(x(\lambda y.M))$ is the same as before, except that now $M$ can be resolved.


Some more words on Peirce from a proof-theoretic perspective:
A derivation of Peirce's law in classical logic requires an application of the reductio ad absurdum rule (or something equivalent, like double negation eliminiation): An assumption $\neg \alpha$ is made from which $\bot$ is derived, then $\alpha$ is concluded while discharging the assumption $\neg \alpha$. Again, you would need to argue why RAA is necessary, i.o.w., why there can be no derivation without this step.
RAA/DNE is part of/admissible in natural deduction for classical logic, but not intuitionistic logic: In IL, only ex falso quodlibet sequitur available, which allows to conclude anything from $\bot$ but does not allow to discharge assumptions for the form $\neg \alpha$. In fact, from a proof-theoretic perspective, the presence or absence of RAA/DNE is exactly what tells the two systems apart; the remaining set of rules is the same; so IL is basically CL with RAA/EFQL+DNE replaced by the weaker EFQL rule.
Since RAA/DNE is necesssary for the proof but this rule is not available in IL, Peirce is not derivable in ND (or any other system) for IL, and in turn not for positive implcation logic, the $\{\to\}$-fragment of IL.


$^1$ In a formal proof, major premise = the premise with the formula that contains the occurrence of the operator to be eliminated by the rule, minor premises = the other premises. In the $(\to E)$ rule, with a conclusion is of the form $\Gamma \vdash \beta$ and two premises, the major premise is the premise of the form $\Gamma \vdash \alpha \to \beta$, and the minor premise is the one of the form $\Gamma \vdash \alpha$.

$^2$ In fact, it can be shown that for any formula which is only valid classically but not in IL, its double negation can be derived in IL. Other than in classical logic, in IL, $\neg \neg \phi$ is not equivalent to $\phi$: it is a weaker propositions, so $\phi$ implies $\neg \neg \phi$, but not necessarily the other way round.

$\endgroup$
  • 1
    $\begingroup$ The strong normalizability of the STLC is what helps you be confident you cover "all" bases. You switch from trying to find a term that inhabits the type to finding a normal form term that inhabits the types. This rules out adding "extra" assumptions as those would eventually need to be discharged and you'd get non-normal subterms like $(\lambda f:\tau\to\tau.M)N$. We can only apply $\to E$ where the left argument is a variable applied to a series of normal form terms (e.g. $x$ as in your derivation, or $x(\lambda y.y)$ for another example). $\endgroup$ – Derek Elkins Mar 31 at 19:41
3
$\begingroup$

Gentzen designed his logic to be normalizable. So for example, if a proof has $\land\text{-intro}$ followed by $\land\text{-elim}$ of the same introduced subexpression, then the proof can be simplified by removing those 2 steps.

Type theoretic proofs are represented as typed lambda expressions. The normalization corresponds to simplifying the lambda expression by following the usual evaluation rules. So a proof containing $\land\text{-intro}$ followed by $\land\text{-elim}$ would be represented by a lambda expression containing a pair $(x, y)$ (cons in lisp terms) and a request for the the first or second value of that expression (car or cdr in lisp terms), so the simplification amounts to converting part of the proof from (car (cons x y)) to just x.

Some of the consequences of this design are

(a) all (gentzen style intuitionistic postive partial fragment of propositional logic) proofs can be normalized

(b) all normalized proofs only contain rules pertaining to the operators used in them (a theorem without a $\lor$ in it won't contain $\lor\text{-elim}$ in the proof, for example)

(c) all normalized proofs only contain sub expressions of the theorem to be proven (and assumptions if those aren't eliminated)

So to prove there is no proof of $((p \to q) \to p) \to p$ you only need to check if there is a normalized proof or not (a). And to do that you only need to work backwards from the final statement, for this statement only needing to check $\to\text{-into}$ and $\to\text{-elim}$ since only $\to$ is present in the theorem (b). And you only need to check instances of the inference that come from sub expressions, 5 of them in this case (c). So...

$$((p \to q) \to p) \to p$$

Can only be a result of $\to\text{-intro}$, so

$$\begin{array} {ll} \quad (p \to q) \to p & \text{assumption} \\ \quad \vdots \\ \quad p \\ ((p \to q) \to p) \to p & \to\text{-intro} \end{array}$$

The only sub expressions that allows $p$ to be constructed are $(p \to q) \to p$ with modus ponens, so

$$\begin{array} {ll} \quad (p \to q) \to p & \text{assumption} \\ \quad \vdots \\ \quad p \to q \\ \quad p & \to\text{-elim} \\ ((p \to q) \to p) \to p & \to\text{-intro} \end{array}$$

And the only way to construct $p \to q$ is

$$\begin{array} {ll} \quad (p \to q) \to p & \text{assumption} \\ \quad \quad p & \text{assumption} \\ \quad \quad \vdots \\ \quad \quad q \\ \quad p \to q & \to\text{intro} \\ \quad p & \to\text{-elim} \\ ((p \to q) \to p) \to p & \to\text{-intro} \end{array}$$

And as there are no sub expressions left to allow for the inference of $q$, this is an unprovable statement. This process could be automated with a (multi-)graph algorithm, using sub expressions as vertices and inferences as edges.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.