Formal logic behind defining variables in a proof (not E.I. or U.G, etc.)

Question

This is something I have been curious about and hopefully has a simple answer. Often when looking at proofs I will come upon a step that goes along the lines of "define y = ..." and then proceed to use the defined y to show some conclusion. For example in Euclids infinity of primes theorem

he defines " let k be the product of all the prime numbers less than n"

followed by "now let m = k + 1".

and proceeds to reason with these definitions to arrive at the desired results. My question is to what sort of constraints are there to defining new objects to a proof? I am aware of universal generalization rule which requires some restrictions in introducing an arbitrary constant as well well as the other quantifier rules of inference such as existential instantiation and so on. However this whole defining a variable does not seem to be any of these rules.

So at the end of the day can you simply define objects like this all willy nilly like? What sort of justification can you write for such a step? It seems problematic to me because I feel like you need to ensure the existence of such objects before you can introduce them like this, and in particular a step such as " let k be the product of all the prime numbers less than n" seems to define an object that has more meaning than simply a definition given by an equation that defines the object of previously defined terms (like "define m = k + 1").

So this begs the question of whether you can arbitrarily define objects that have unconfirmed properties. This does not seem right because then you could be reasoning with statements that are false but since you "defined" them without restriction you mistakenly inferred something that turns out to be false.

So long story short: what is this method known as formally and what sort of restrictions are associated with it?

Answer 1

It seems to me that you are looking for the $\exists$-Elimiantion rule of Natural Deduction.

See Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 179 :

We turn to ($\exists$E). This is the most complicated of the natural deduction rules, and many first courses in logic omit it.

How can we deduce something from the assumption that ‘There is a snark’? If we are mathematicians, we start by writing :

(*) Let $c$ be a snark

and then we use the assumption that $c$ is a snark in order to derive further statements, for example,

(§) $c$ is a boojum [imaginary dangerous animal].

If we could be sure that (§) rests only on the assumption that there is a snark, and not on the stronger assumption that there is a snark called ‘$c$’, then we could discharge the assumption (*) and derive (§). Unfortunately, (§) does explicitly mention $c$, so we cannot rule out that it depends on the stronger assumption. Even if it did not mention $c$, there are two other things we should take care of. First, none of the other assumptions should mention $c$; otherwise (§) would tacitly be saying that some other element already mentioned is a snark, and this was no part of the assumption that there is a snark. Second, the name $c$ should be free of any implications; for example, we cannot write $cos \theta$ in place of $c$, because then we would be assuming that some value of $cos$ is a snark, and again this assumes more than that there is a snark. However, these are all the points that we need to take on board in a rule for eliminating $\exists$.

Thus, the rule for $\exists$-Elimination is formalized as follows :

from a derivation $\Gamma \vdash \exists \phi$ and a derivation of $\Delta, \phi[t/x] \vdash \chi$, where t is a term [constant symbol or a variable] which does not occur in $\chi, \phi$ or in any undischarged assumption in $\Gamma$ or $\Delta$ except in $\phi[t/x]$, we can infer $\Gamma, \Delta \vdash \chi$, i.e. we can infer $\chi$ from the undischarged assumptions of the two previous derivations except $\phi[t/x]$.

---

In your example, taken from Euclid, Book IX,Prop.20 :

Prime numbers are more than any assigned multitude of prime numbers.

Provided that Euclid defines [Book VII, Def.11] :

A prime number is that which is measured by a unit alone [i.e. its only divisor not equal to itself is the unit]

and thus we know that there are prime numbers [$1$ is], Euclid makes the assumption :

Suppose that there are $n$ primes, $a_1, a_2,\ldots, a_n$. (Euclid, as usual, takes an specific small number, $n = 3$, of primes to illustrate the general case.)

Let $m$ be the least common multiple of all of them. Consider the number $m + 1$. If it’s prime, then there are at least $n + 1$ primes.

So suppose $m + 1$ is not prime. Then according to VII.31, some prime $g$ divides it. But $g$ cannot be any of the primes $a_1, a_2,\ldots, a_n$, since they all divide $m$ and do not divide $m + 1$. Therefore, there are at least $n + 1$ primes. Q.E.D.

The proof runs as follows :

• let $a_1, a_2,\ldots, a_n$ primes; then $\exists x (x = lcm(a_1, a_2,\ldots, a_n))$ : this is $\exists x \phi$

• let $k=lcm(a_1, a_2,\ldots, a_n)$ : this is $\phi[k/x]$

• let $m=k+1$; clearly $m \ne a_1, a_2,\ldots, a_n$; if $m$ is a prime we are done;

• otherwise, there is a prime $g$ which divides $m+1$ and $g \ne a_1, a_2,\ldots, a_n$.

In both case we have that :

$\exists x (x \ne a_1, a_2,\ldots, a_n \, \text {and} \, x \, \text {is prime} \, )$, and this is $\chi$.

The sentence $\chi$ does not contain $k$, and thus the conditions for $\exists$-E are satisfied and the conclusion holds.

---

Regarding the new example : "There is no largest real [or natural] number", we can "formalize" it as follows.

1) $\forall x(x < x+1)$ -- theorem of number theory

2) $x < x+1$ --- from 1) by $\forall$E

3) $\exists y(x < y)$ --- from 2) by $\exists$I

4) $\forall x \exists y(x < y)$ --- from 3) --- by $\forall$I, $x$ is not free in 1).

Thus, as you have noted, we do not need the existential elimination rule.

---

---

If you are searching for another example of "real life" use of $\exists$E, consider :

$a < b \land b < c \to a < c$ --- $a,b,c \in \mathbb N$

Proof :

1) assume : $a < b$ and : $b < c$ i.e. $\exists d(s(d)+a=b)$ and $(\exists e)(s(e)+b=c)$, where $s(x)$ is the successor function

2) assume for $\exists$E : $s(d)+a=b$ and $s(e)+b=c$

3) $(s(e)+s(d))+a=c$ --- by propety of equality

4) $s((s(e)+d))+a=c$ --- by recursive axiom for $+$ : $n+s(x)=s(n+x)$ and equality

5) $(\exists f)(s(f)+a=c)$ --- by $\exists$I i.e. $a < c$.

The last formula does not contain $d$ nor $e$; thus we can apply $\exists$E twice, discharging the "temporary" assumptions in 2), and we can conclude from 1) with :

$a<b, b<c \vdash a<c$.

Then, by $\to$I twice and tautological equivalence :

$(a<b \land b<c) \to a<c$.

Answer 2

When formalizing such an argument the line in the proof will be something like $\exists x (x=\prod_{p\in P}p)$, where $P$ is already defined as the set of primes less than $n$. You then proceed to reason about $x$ as usual. This has no special name that I know of: you are just introducing a variable to reason about a term. The restrictions are that you have already defined some term which correctly models whatever you want to reason about, in this case $\prod_{p\in P}p$ - so you want a term of your language, $t(n)$, with a free variable $n$ which will be a natural number, such that $t(1)=1$, $t(n+1)=\begin{cases} t(n) &\mbox{ if } n \text{ not prime} \\ t(n)\cdot n &\mbox{ if } n \text{ prime}\end{cases} $

The question is how you define such a term; this will depend on the formal system you are using. It is not too difficult in ZFC, where you can define $\prod_{i\in I}i$ for any finite subset of a monoid (such as the multiplicative natural numbers); the definition will use the standard techniques to define functions by recursion, which is not entirely trivial. It is essentially the same way you would define eg addition and multiplication on the natural numbers (and other ordinals). I can't find any particularly good references by a quick google, but if you look up definitions by recursion over the ordinals in any decent set theory textbook you will get the idea.

In PA, you can use the standard techniques for code recursive functions and sets, which is fairly cunning. There must be lots of references for coding such things (I like Cori and Lascar's mathematical Logic, book 2)

Answer 3

The newly-defined objects are valid if and only if they exist. That is, if you define an object $o$ that satisfies predicate $P$, you must prove that $\exists a, P(a)$.

Explanations: The newly-defined objects in a proof already exist before you define them, it's just that sometimes you don't think about them because they are irrelevant. But if you define absurd objects ("let $n$ be an integer that is both even and odd") then you can derive a contradiction.