How do we translate between Logic and Mathematical English?

Question

Take the statement "Let $a \in \mathbb{R}$ and let $z=ai.$" $(1)$

In English, this means "Let's choose any real $a$ then define $z$ such that $z=ai$ for that particular $a$ we have just chosen". All good there. We might use terms like "arbitrary constant" or "parameter" to describe $a$ too.

How do we write $(1)$ in formal logic?

I know that $\forall a \exists z (z=ai)$ is one option, but is that correct/the only one?

I know that $\forall a \forall z (z=ai)$ is wrong, and that so is $\exists z \forall a (z=ai).$

I know that "let" means to consider a specific real $a$ such that we can assume only that it's a member of $\mathbb{R},$ and $z$ if well-defined for this $a$ is defined for all $a \in \mathbb{R}.$ But then this implies $\forall a (z=ai),$ and it seems that each $a$ requires a different $z$ to make the statement true, i.e., $z$ depends on $a,$ yet $\forall a (z=ai)$ doesn't allow that.

Answer 1

"Let" statements modify the context for subsequent content by introducing symbols and assumptions that can be referenced later. They don't translate to closed formal sentences themselves; the introduced variables are free until some later step produces a closed statement using e.g. universal generalization. In your example this could be something like $\forall a\forall z(z=ai\implies zi=-a).$

Statements of the form "Let $v=\dots$" can also be regarded as introducing notational abbreviations instead of adding any formal content.

Answer 2

Since this is only a part of a mathematical text, I suggest to write $$a \in \mathbb R \land z=ai.$$ Since your text is not a statement, you cannot write it as a closed formula. When you prove the statement $a \in \mathbb R \land z=ai \Rightarrow \phi(a,z)$ for some formula $\phi(a,z)$, you can put quantifiers before: $\forall z \forall a (a \in \mathbb R \land z=ai \Rightarrow \phi(a,z))$; equivalently: $\forall z \, \forall a \in \mathbb R (z=ai \Rightarrow \phi(a,z))$.

I recommend you not to use formulae at places English is better understandable. From my suggestion, it is not clear that $a \in \mathbb R$ is a definition, so your sentence $(1)$ is perfectly fine. Definitions are usually written with colon, i.e., $a:=b+c$ or $$(a,b,c) \text{ is a pythagorean triple} :\Leftrightarrow a^2+b^2=c^2.$$

For your definitions, this would give $a :\in \mathbb R \land z:=ai$, but I never saw the symbol $:\in$, so it would be difficult to parse.

I think the reason why I did not see the symbol $:\in$ is that this definition is not unique. Picking an arbitrary element of a set usually leads to open formulae as I suggested.

Answer 3

Take the statement "Let $a \in \mathbb{R}$ and let $z=ai.$" $(1)$

Here, you are assigning a denotation ($z:=ai$) and a restriction ($a$ belongs to a strict subset of the discourse domain $\mathbb C$).

And in such statements, it is tacit that $a$ is arbitrary.

So, $(1)$ means

• Let $a$ be an arbitrary real number and let $z$ denote $ai.$

In English, this means "Let's choose any real $a$ then define $z$ such that $z=ai$ for that particular $a$ we have just chosen".

Sure, but a key point of $(1)$'s intended meaning is that we are free to vary the value of $a.$

"arbitrary constant" to describe $a$

Yes: in the large, $a$ is variable ("arbitrary"), while within any iteration of what follows $(1),\,$ $a$ has a particular value ("constant").

How do we write $(1)$ in formal logic?

I know that $\forall a \exists z (z=ai)$ is one option, but is that correct/the only one?

$(1)$ is the beginning fragment of a proof, and isn't really an assertion so isn't really an FOL sentence. After Universal Generalisation has been invoked, you might then end up with, for example,

• $\forall a{\in\mathbb R}\;\forall z{\in\mathbb C}\;(z=ai\implies iz=-a)$

or

• $\forall a{\in\mathbb R}\;(ai^2=-a).$