$\lambda$ calculus how encode A $\leftrightarrow$ B

Question

I am spending days figuring out how can i show A $\leftrightarrow$ B such that A=B=True or A=B=False as $\lambda$ calculus

I know that we can show :

True ≡ λxy.x

False ≡ λxy.y

and ≡ λpq. p q false

or ≡ λpq. p true q

not ≡ λpq. p false true

are these information enough to solve this problem ?

Please help i really appreciate it.

Answer 1

$$[A \iff B] \equiv [(A \land B) \lor \neg (A \lor B)]$$

where:

• $\iff$ denotes "iff"
• $\land$ denotes "and"
• $\neg$ denotes "not"
• $\lor$ denotes "or"

---

In conclusion:

p⟺q := λpq. or (and p q) (not (or p q))

Expanded:

p⟺q := λpq. (p q (λxy. y)) (λxy. x) ((p (λxy. x) q) (λxy. y) (λxy. x))

---

However, there is a shorter equivalent:

p⟺q := λpq. p q (not q)

Fully expanded:

p⟺q := λpq. p q (q (λxy. y) (λxy. x))