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?

  • 1
    $\begingroup$ It's more a quirk of language, you are naming the product of primes less than $n$, by $k$. If you are happy that $n$ denotes a number, I don't know why you are unhappy about multiplying all primes less than $n$ together? If you want some mathematical formalism to express that you can try $ k= \Pi_{p<n,p \text{ is prime}} p$, but, that doesn't do anything new for you? $\endgroup$
    – James
    Feb 16, 2015 at 18:31
  • $\begingroup$ To start with in proof, you can assume anything you want in an initial premise, even a contradiction. Later, in your conclusion, you will be able to generalize on any variables that where introduced in that premise. It gets a little more complicated with nested premises and conclusions, and when you introduce variables by existential specification (instantiation). You may find my proof software and accompanying tutorial helpful in this regard. Download them at my website dcproof.com $\endgroup$ Feb 16, 2015 at 19:54
  • $\begingroup$ It's the job of formal logic to encode such devices adequately. If it can't, it is not rightfully called a logic. Define Socrates to be a man. Define all men to be mortal. Then Socrates is mortal. $\endgroup$
    – Loki Clock
    Feb 19, 2015 at 13:58

3 Answers 3


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

  • 1
    $\begingroup$ @skyfire - this is proved in this way : 1) $\forall x(x-x=0)$; 2) $x-x=0$ -- by $\forall$-E; 3) $\exists y(x-y=0)$ -- by $\exists$-I; 4) $\forall x \exists y (x-y=0)$ --- $\forall$-I, because $x$ not free in 1). $\endgroup$ Feb 17, 2015 at 19:45

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.

  • $\begingroup$ Very nicely and concisely put. Only I would rephrase it as $\exists a,~ a=P$, which is generally what I think is meant when people say "P exists". $\endgroup$
    – DanielV
    Feb 23, 2015 at 5:20

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)

  • $\begingroup$ Appreciate the response, but it's a bit over my head, I'm not sure what a monoid is :( pretty much the only knowledge I have on proof is a reading through a logic book and so I'm attempting to ease into ZF Set theory whilst reading proof type books to catch all the methods employed on my way through :) $\endgroup$
    – skyfire
    Feb 16, 2015 at 19:22
  • $\begingroup$ Well if you want a formal way of solving the problem, keep learning set theory and you'll encounter definitions by recursion soon enough. If you want an informal understanding of what you need to do to correctly say "let x be the thing such that $\phi(x)$", you need to prove that there exists something which satisfies $\phi$, and that there is only one such thing. For instance to reason using the HCF of $x$ and $y$, first you need to prove that there exists exactly one natural number $z$ which divides them both, and such that any other natural number which divides them both divides $z$ $\endgroup$
    – Blunka
    Feb 16, 2015 at 19:32
  • $\begingroup$ The case of reasoning using $\prod_{p<n,\text{ } p \text{ prime}}p$ is more complicated since you're not using an object which uniquely satisfies a certain property - or rather you are, but the property is a recursive one, and it's not obvious how you write it down in eg the first order language of arithmetic $\endgroup$
    – Blunka
    Feb 16, 2015 at 19:35

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.