Lambda calculus combined with first order logic notation (quantifiers, propositional connectives, and set notation)

I understand that Lambda Calculus does not traditionally admit the notation of first-order logic and set-theory, such as the quantifiers $\forall$ and $\exists$, the propositional connectives $\vee, \implies,...$, and set notation, such as $x \in S$. However, as a working mathematician, it is only natural to want to combine these formalisms into statements such as

$$\forall x:\mathbb{N} \left(f(x) \in S\right)$$ where $f = \lambda z:\mathbb{N}. 2z$ , and $S = \{n:\mathbb{N}\mid\ 2 | n\}$ .

Is there some studied logic system in which statements like the one above can be formalized naturally?

• The links in this post have references that address your question: math.stackexchange.com/questions/2486170/… – DanielV Oct 29 '17 at 7:52
• Universal quantification is defined in the obvious way, $$(\forall x. Px) \iff (P = \lambda y.\top)$$ defining $\top$ and the other operators is actually the demanding part. – DanielV Oct 29 '17 at 7:53
• @DanielV: What about set notation? – Evan Aad Oct 29 '17 at 7:57
• A set is just a unary relation. Honestly I'm not the person to ask. Look at who was active on the other question, and @ping them to let them know you have a similar question. – DanielV Oct 29 '17 at 8:05
• @DanielV: and propositional connectives? – Evan Aad Oct 29 '17 at 8:06

Using a HOL-like approach as described in the link given by DanielV, subsets given by the axiom of specification are just modeled as predicates. Your whole expression becomes $\forall(\lambda x\!:\!\mathbb{N}.S(f(x)))$ (or more compactly: $\forall (S\circ f)$) where $S\equiv\lambda n\!:\!\mathbb{N}.(2|n)$. You can look at the systems HOL4, HOL Light, and Isabelle/HOL for mechanized proof assistants for this approach.
In this case, we might have a type like $\prod_{x:\mathbb{N}}S(f(x))$. $S$ would look the same except now $2|n$ would need to stand for a type. There are a variety of ways of accomplishing this. For example, we could have an (explicitly defined) function (i.e. an algorithm) $\mathtt{divides} : \mathbb{N}\times\mathbb{N}\to\mathbb{B}$ where $\mathbb{B}$ is the type of Booleans with values $\mathtt{True}$ and $\mathtt{False}$. Then $(m|n)\equiv(\mathtt{divides}(m,n)=_\mathbb{B}\mathtt{True})$. Actually proving that $\prod_{x:\mathbb{N}}S(f(x))$ holds would mean actually providing a lambda term of that type. It may be as simple as $\lambda x\!:\!\mathbb{N}.\mathtt{refl}_\mathtt{True}$ depending on the exact definition of $\mathtt{divides}$, but it could easily require more equational reasoning than this. ($\mathtt{refl}_x$ is the value that "proves", in the above sense, that $x=x$.)