proving tautologies in λP

Stream: new members

[rzeta0]

In order to better understand how proof assistants work, I have been working through Type Theory & Formal Proof (Nederpelt) based on a recommendation here a few months ago.

I am now on Chapter 5, which introduces types depending on terms, λP. The Chapter introduces the idea of simple logical statements being equivalent to λP terms. For example, the implication $A \implies B$ is equivalent to the type $\Pi x:A.B$. To prove the logical statement, we can find an inhabitant of the type.

My question is about proving tautologies. As I understand it, a tautology is always true, regardless of any context. This means that when deriving a judgement (context, term, type) the context must be empty. Is this correct?

In my mind, a tautology doesn't depend on external facts, it is self-contained, self-evidently true (wishy washy language, I know, I'm not a trained mathematician, sorry).

---

I thought I'd illustrate with a minimal example.

We know that $S \implies S$ is a tautology. Let's try to prove it via the above method.

The equivalent λP type that is $\Pi x:S.S$. I can use the derivation rules of λP to derive the following judgement:

$$S:* \quad \vdash \quad \lambda x:S.x \quad : \quad \Pi x.S.S$$

Here the inhabitant is $\lambda x.S.x$, but the context is $S:*$ and is not empty.

---

Where is my error? Is it one of the following?

• The context doesn't need to be empty. In fact it is needed to establish the types of the symbols used in the logical proposition.
• The context for a tautology should be empty, and I've made a derivation algebra error.

---

I've also asked here (link).

[Aaron Liu]

You can't state "$S \implies S$ is a tautology" without knowing what $S$ is

[Aaron Liu]

this is reflected in your λP derivation: you have to have $S:*$ in context for the derivation

[Aaron Liu]

what this actually means is, "forall propositions $S$, the statement $S \implies S$ is true"

[Aaron Liu]

this corresponds to $\Pi S:*.\Pi x:S.S$, which is well-formed in the empty context

[Aaron Liu]

this is a valid type in λP2

[rzeta0]

Thanks @Aaron Liu this is helpful and actually makes sense to me.

I will look again at the textbook as my (beginner) brain thinks the author isn't doing what you're doing. See attached snippet from them book below.

Screenshot 2025-08-07 at 21.50.08.png

Here the author appears not to include $\Pi S:*$ in the type to be inhabited, yet the actual judgement has it.

---

Can I double check that the context should be empty for tautologies. I think I read your last sentence as confirming that.

[Aaron Liu]

there are many ways you can think of tautologies

[Aaron Liu]

this is the way I think of them

[rzeta0]

someone has an interesting reply in the linked stack exchange which suggests you can't have an outer $\Pi S:*$

https://cs.stackexchange.com/questions/173350/question-about-proving-a-tautology-via-λp-empty-context

looking at the derivation rules (see below) I can see that they don't allow the formation of a $\Pi S:*$, but only a $\Pi x:A$ where $x$ is a term ( of type $A$ which itself is of type *)

hmm

rules.png

[Aaron Liu]

yes

[Aaron Liu]

you need to upgrade from λP to λP2 to allow that

[Aaron Liu]

same as when you upgraded from λ→ to λ2 before

[rzeta0]

ok - I will continue and not worry too much about this for now as you and the other person has said this is a limitation of λP.

the textbook has several such wrinkles for beginners like me, but I haven't found an easier introduction so will persist