2
$\begingroup$

I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent example here https://www.isa-afp.org/entries/GoedelGod.html (as encoded for Isabelle/HOL).

This embedding has embedding for Leibniz equality for individuals:

abbreviation mLeibeq :: "μ ⇒ μ ⇒ σ" (infixr "mL=" 90) where "x mL= y ≡ ∀(λφ. (φ x m→ φ y))"

and this type of euqality is used for the first axiom already:

A1a: "[∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))]"

which can be written without lambdas as:

A1a: ∀φ[P(¬φ)↔¬P(φ)]

My question is - how to understand the expression ∀(λφ. (φ x m→ φ y)), because usually we have ∀x.P(x)? I.e. universal quantifier expects the argument (x) and the predicate (P(x)), but this expression contains noone know what? is entire (λφ. (φ x m→ φ y)) and argument x or Predicate P(x)? What can be omitted here, what is the convention used here?

$\endgroup$
8
$\begingroup$

The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over.

Let us compare the situation to the definite integral, for concretness just from $0$ to $1$. Here is an example: $$\int_0^1 x^2 + 3 x \, dx$$ This is a very archaic way of writing mathematical expressions that mathematicians like to stick to. In general (and ignoring details about non-integrable functions) the definite integral is itself a function: it takes a function $f$ as an argument, such as $f(x) = x^2 + 3x$ and returns a number (the area under the curve). So we could simply write $I$ for "integrate from $0$ to $1$" and then the integral of $f$ is simply $$I(f)$$ (Or if you want to keep the integration bounds visible write $I_0^1(f)$, but I won't). The argument $f$ need not be a symbol, it can be a complex expression: $$I(x \mapsto x^2 + 3 x)$$ Notice how "$dx$" above changed to "$x \mapsto$". In $\lambda$-calculus notation we would write this as $$I(\lambda x . x^2 + 3 x).$$ In archaic notation people sometimes feel uneasy about writing $$\int_0^1 f$$ and so they end up always displaying $dx$ by writing $$\int_0^1 f(x) \, dx$$ even though there really is no need to do so, because $\int_0^1$ is a higher-order function which maps real-valued functions to real numbers. If you want to make traditional mathematician feel uneasy you should write $$\int_0^1 (x \mapsto x^2 + 3 x)$$ on their whiteboards

If this much is clear, then it should be easy to see that the universal quantifier $\forall$ is like integration, except that it takes a propositional function (one mapping into truth values instead of numbers) and returns a truth value. The archaic notation $$\forall x . (x^2 + 3 x > -3)$$ can be changed, just like for integrals, to $$A(f).$$ Here $A$ is the universal quantifier, and $f$ its argument, which is a function mapping from a set to the truth values. An example of such a function is $f(x) = (x^2 + 3 x > -3)$. And again, we can inline the complex expression to get $$A(\lambda x . (x^2 + 3 x > -3))$$ Now just replace $A$ with $\forall$ for good old times sake: $$\forall(\lambda x . (x^2 + 3 x > -3)).$$ This his how computers like it. The notation is general, so we can write just $\forall f$ instead of $\forall x . f(x)$, and it exposes $\forall$ for what it is: a higher-order function that maps propositional function to truth values.

| cite | improve this answer | |
$\endgroup$
  • 5
    $\begingroup$ "it[the integral] takes a function f as an argument" Not exactly. The integral takes in differential forms. The adherence to the $dx$ notation is not so much to keep a reminder of the quantified variable, even if it also serves that purpose, but to remind that the integrand pulls back (change of variable) as forms, not as functions. Right end goal in the explanation, but unfortunate example used as analogy. $\endgroup$ – plop Aug 14 at 14:18
  • 1
    $\begingroup$ None of the mathematicians I know would react the way you're saying. $\endgroup$ – probably_someone Aug 14 at 15:48
  • $\begingroup$ @plop: I readily concur that there are many ways of viewing the integrals, and that $dx$ plays different roles in different situations. However, we are in the teritorry of pedagogy here. I picked a form of integral that is in direct analogy with the universal quantifiers in terms of higher-order functions. For the purposes of this answer it is much better to view it as a variable binder. $\endgroup$ – Andrej Bauer Aug 14 at 16:56
  • $\begingroup$ @probably_someone: What precisely are you saying? That your mathematician friends habitually write $\int (x \mapsto x^2 + 3 x)$? $\endgroup$ – Andrej Bauer Aug 14 at 16:56
  • $\begingroup$ @AndrejBauer I'm saying that they wouldn't object if you did so, unless the idea that the input of an integral is a differential form is relevant to what you're doing. $\endgroup$ – probably_someone Aug 14 at 16:57

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.