Church's definition of "or" in Lambda Calculus

Question

I have been working through Church's Postulates for the foundation of logic. In the paper he has some four definitions that he will then use in order to formulate the later postulates.

If someone could illuminate one of these for me, I am sure I could continue with my excursion.

---

$$ V \rightarrow \lambda\mu\lambda\nu.\sim.\sim\mu .\sim\nu $$

Then $V(\text{P}, \text{Q})$ should be read as "P or Q".

My understanding is that it gets expanded as such then,

$$ \{\{ \lambda\mu\lambda\nu.\sim.\sim\mu .\sim\nu \}\left (\text{P}\right )\}(\text{Q}) $$

Because a function of two variables become a function of one variable whose values are functions of one variable.

My question then is, how do I go forth from here? It is probably an issue of not being able to substitute correctly. Intuitively $\text{P}$ goes into the function to the left, but then that gets a truth value and is no longer a function.

Answer 1

Before I answer the question, let me enumerate an additional definition. I think that this inclusion would help illuminate the conclusion.

$$ (1)~~~V \rightarrow \lambda\mu\lambda\nu.\sim.\sim\mu.\sim\nu $$ $$ (2)~~~U\rightarrow \lambda\mu\lambda\nu.\sim.\mu.\sim\nu $$

$V$ is the function OR, $V(\text{P},\text{Q}) \equiv [\text{P}] \vee [\text{Q}]$. $U$ is the function IMPLIES, $[\text{P}] \Rightarrow [\text{Q}]$. $Q$ is the function for equivalence, $Q(\lambda x.\text{M}, \lambda x.\text{N})$ is read as $[\text{M}] \equiv_x [\text{N}]$.

If we look at the function $\neg(\text{P} \wedge \neg \text{Q})$, note that $\neg \text{X}$ and $\sim\text{X}$ are merely varying notation according to Church's definitions, we can reduce that to $\text{P} \Rightarrow \text{Q}$.
If we now look at the function $\neg (\neg\text{P}\wedge\neg\text{Q})$, we can reduce that to $(\text{P} \vee \text{Q})$.
Both of these propositional functions share form and consequence with (1) and (2) respectively.

The question is then not simply how the function $V$ is reduced in Church's $\lambda$-Calculus, it is how P and Q interact with one another in the function, since $\sim$ is a function that takes only one argument. That argument is therefore then a conjunction of the two arguments, in (1): $(\sim\mu\wedge\sim\nu)$, and in (2): $(\mu\wedge\sim\nu)$.

It is probably an issue of not being able to substitute correctly. Intuitively P goes into the function to the left, but then that gets a truth value and is no longer a function.

$$ \{\{\lambda\mu\lambda\nu.\sim.\sim\mu.\sim\nu\}(\text{P})\}(\text{Q}) $$ $$ \{\lambda\nu.\sim.\sim\text{P}.\sim\nu\}(\text{Q}) $$ $$ \sim[\sim\text{P}][\sim\text{Q}] $$ $$ [\text{P}] \vee [\text{Q}] $$

The penultimate step should perhaps be more correctly expressed as $\sim[\sim\text{P}[\sim\text{Q}]]$, but it does not lend as much understanding I think.

I've spent some time pondering this problem, and I believe that I have come to the correct conclusion. If anyone disagrees with me, I am sure they will make themselves heard.