0
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ The links in this post have references that address your question: math.stackexchange.com/questions/2486170/… $\endgroup$ – DanielV Oct 29 '17 at 7:52
  • $\begingroup$ 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. $\endgroup$ – DanielV Oct 29 '17 at 7:53
  • $\begingroup$ @DanielV: What about set notation? $\endgroup$ – Evan Aad Oct 29 '17 at 7:57
  • $\begingroup$ 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. $\endgroup$ – DanielV Oct 29 '17 at 8:05
  • $\begingroup$ @DanielV: and propositional connectives? $\endgroup$ – Evan Aad Oct 29 '17 at 8:06
1
$\begingroup$

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.

An alternative approach mentioned in the other question but not elaborated on there is a propositions-as-types approach. This approach is usually used in a constructive setting with a dependently typed lambda calculus. In this approach, we model a statement by a type, and the proof of the statement is witnessed by providing a value of that type. This is the approach used by mechanized proof assistants like Coq, Agda, or LEAN.

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$.)

To address one of your comments, both approaches above have been extensively used in practice as you can see from the applications of the proof assistants mentioned. This is a personal opinion, but I would go so far to say that even using either of these approaches by hand is more natural and feasible that (formally!) using set theory. Of course, the latter approach is, as I said, usually used as a constructive type theory which makes a profound difference including making some results much harder to prove (and, of course, making some results impossible to prove). (Classical) HOL is definitely much closer (in fact very close to) "standard" math/set theory.

$\endgroup$
  • $\begingroup$ Could you please add a link (links) to some of the relevant literature, specifically, (Classical) HOL? $\endgroup$ – Evan Aad Oct 29 '17 at 9:40
  • 1
    $\begingroup$ I added a link (among others) to The Seven Virtues of Simple Type Theory which is the paper mentioned in the other question. It is referenced by the HOL4 documentation. You can look at its references for more details; it's more of an introduction and not super-formal meta-theoretically. Of course, any of the implementations I linked to (or there are a few others) also have tutorials, documentation, and complete and unambiguous descriptions of the languages they implement and how things like connectives are derived. $\endgroup$ – Derek Elkins Oct 29 '17 at 10:06
  • $\begingroup$ Are all those systems you referenced actually based on the typed lambda calculus the poster is describing, or are they actually based on curry-howard style type systems? $\endgroup$ – DanielV Oct 29 '17 at 12:24
  • $\begingroup$ @DanielV The OP isn't really specific about any particular lambda calculus. It's quite likely (classical) HOL is closest to what the OP would want assuming they want to do more or less "standard" mathematics. All the "HOL" systems are examples of this. The other systems "Agda, Coq, LEAN" are constructive type theories and are explicitly alternative approaches. The answer is a bit heavy on describing these systems since they work in a less familiar way. While the constructive type theory approach is probably not what the OP wants, it also allows a natural formulation of the given statement. $\endgroup$ – Derek Elkins Oct 29 '17 at 12:37

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.