庄荣文会见科威特财政部次大臣哈利法

Question

What is the logical meaning of the word 'let' as used in mathematical theorems and definitions?

For example:

Let g be differentiable on an open interval O and let c ∈ O . . .

Answer 1

'Let' is a local definition or identity. It is common in algebra where we assign symbols to values, but it can be used in many ways.

Teacher: "Let the area of the field be A..."

Student: "But, Sir, what if it isn't?"

Many years ago, this gave me pause. Could the student have a point? I don't think so. If A is the area of the field and the field gets larger, either A gets larger, or A was the area of the field at some particular time. Or maybe the rest of the problem leads to some absurdity such that A cannot have a value. Or the definition turns out to be inadequate, and we have to revise it.

'Let' is a local definition. It is limited to some context. A is not tied to the area of a field forever. The definition will expire when the context does.

Answer 2

No specific "logical meaning".

Let: "to allow someone to do something".

See e.g van Dalen, page 8:

Theorem (Induction Principle): Let A be a property...

Thus, the use is: to introduce an assumption, an object with some specified property, etc that is relevant for the proof.

See D.J. Velleman, How to Prove It (Cambridge, 2006) page x:

Mathematical proofs are also constructed by combining certain basic proof structures. [...] sentences like “Let x be arbitrary” and “Suppose P” are not isolated steps in proofs, but are used to introduce the “for arbitrary x prove” and “suppose-until” proof structures.

Answer 3

When stating a theorem

Formally/syntactically, this is statement in the informal language introducing a variable with some qualifications that serve as the hypotheses of the theorem. Logically it might something like (why doesn't philosophy stack exchange support Latex??)

(For all g)(for all o)(for all c)(if (g is a function and o is an interval in the domain of g and c in O) then <some theorem follows>...)

We are using the formal variables of the formal languages, using "for all" quantification, and then applying the conditions stated in the "let..." statement as logical conditions in the antecedent of the main if... then ... construction of the theorem.

When Giving a Name to a Constructed Object

An example is given in the comments of defining phi = (1 + sqrt(5))/2. In this case we are doing a move of extension by definition. In this case we are adding a brand new letter to our formal language called phi. We have given a condition that defines phi. However, we cannot freely define new characters. We must be able to prove that there is a single unique element satisfying the condition used to define phi. If we do this then we can prove that the new language and theory that arise after this extension by definition is a conservative extension over the old theory. Informally, this means that we can't prove "new" theorems by introducing this new symbol to theory. It is just essentially an abbreviation for convenience.

Answer 4

Simple Example: If you want to prove that for all real numbers x, P(x) is true, you might start your proof with, "Let y be any real number." (Or simply, "Let y be a real number.") Then suppose you can derive "P(y)" without introducing any other assumptions. Then you can infer, as required that, for all real numbers x, P(x) is true.

Answer 5

You ask:

What is the logical meaning of the word 'let' when used in mathematical texts?

It depends on how seriously you take precision in your explanation. To explain it to a high school student, 'let' is simply an indicator in a proof to assign a value, presume existence of an abstract object, or to make a truth by declaration. For instance, letters which are often used as variables can be assigned a value. 'Let x which is a natural be 4' is an example that narrows the domain of discourse from all naturals to the value four. In this scope of the proof, x has now become a constant value because it will not change. Thus, this periphrastic imperative construction often carries overtones of presumptive rather than certain assertoric force. In other words, as in Mauro's answer, it is used to introduce an assumption or supposition sometimes to be discharged later

But, we can go into more detail about its status by discussing proof-theoretic semantics and natural deduction (IEP) to guide us in our thinking. In order to have a logical calculus, three things are required: a language L, which gives us our syntax, a rule set of inferences, which allows us to transform our grammatical constructions, and a set of axioms, which provide semantic content for the system. For instance, in a natural language proof in English at the secondary level, English and arithmetical syntax are our language, our language includes various axioms such identity a=a, commutativity of addition a+b=b+a, and associativity of addition (a+b)+c=a+(b+c). And for transformations, we can use rules such as a=b->a+k=b+k. Our proofs then follow our grammar, rules, and stay consistent with our axioms.

Sometimes, we have to assume things to determine if other things are true. For instance, in solving a system of equations, we may want to test possible domain values x where x is a natural number. 'Let x be 5' is a unit of discourse which brings about an effect above and beyond assignment of a value to a variable. It functions effectively as assigning a truth value on a presumptive basis so that it might be read as ("x=5 should be held as true"). So, we have assigned using an imperative utterance (the locutionary force), but have done more than the literal assignment. We have signaled to the agent parsing the proof they should assert the truth of the statement (the perlocutionary force).

Thus, like the expression, 'Hereby this assignment, this equation is true', we have accomplished a step in the mind of the agent attempting the proof, but using the third-person passive form of imperative. Like the imperative form in the second-person with the implied you ([you] make it be!), the third-person also has an implied grammatical subject: [reader] Let x be 5. Thus in our search for solutions for the system of equation, the agent who is providing the proof has implicitly guided the reader who is learning the proof the right place to assign a truth value.

If it happens the suppositional logic carries us to a contradiction, it may be that the value assigned, in this case 5, is wrong and cannot be equal to x. For instance, when dealing with parallel lines, the two lines will have no points in common, and therefore the assignment of a domain value will never allow us to calculate a range value that gives us a consistent system. We can then discharge assumption if making it gets us to violate the law of identity and arrive at an equation which says "4=5" for instance. Such a contradiction is a cue that our supposition, which is not an axiom in arithmetic, was useful but led to a proof by contradiction.

Alternatively, let as Jagerber48's answer gives, might be an actual conservative extension to a theory as an extension by definition. In this case, we have created what we in the CS world call syntactic sugar. We have introduced, by the imperative, a constant new term to represent a more complex expression. From WP:

an extension by definition formalizes the introduction of a new symbol by means of a definition. For example, it is common in naive set theory to introduce a symbol ? for the set that has no member.

Thus, we have not extended the axioms, but merely simplified the language by having one symbol represent a more complex construction making the language more comprehensible and ergonomic.

Note, we can also use the 'let' to bind variables to specific domains of discourse, such as presuming a statement which contains an extension in set-builder notation. For example, consider the the WP article on free and bound variables in the section on proof:

The variable n is introduced as an arbitrary but particular element of a set. The statement "Let n be..." implicitly functions as a universal quantifier, binding n for the scope of the proof. The proof establishes a property for this single, arbitrary n , which licenses the general conclusion that the property holds for all positive even integers... The variable k, on the other hand, is bound by an existential quantifier

And lastly, if you're familiar with Tarskian semantics, then it becomes clear that 'let' is not a part of the object language we are proving concepts with, but rather metalanguage of the theory with which we conduct proof. Alternatively, the logical historian John Corcoran in some of his work considers such constructions in the light of discourse grammar. This is why it would be appropriate as Dummett, Prawitz, and others are concerned, you are dealing with proof-theoretic semantics (SEP). See Prawitz's Natural Deduction: a Proof-Theoretical Study (GB) for a review of formalisms that attempts to capture the spirit of natural reasoning conducted by mathematicians.

Answer 6

A mathematical judgment, like a=1 (same as let a equal one), sets the context for a formal system.

What is a formal system?

Essentially, a formal system is a set of axioms (a=1 is an axiom), concepts (we assume a is a variable that can take values), and consequent theorems (deductions which can be finally reduced to the axioms); all expressed (formalized) with a formal language, that is, a set of statements with specific properties expressed with symbols.

In simple words, to formalize something means essentially to write it.

From an epistemological standpoint:

• A formal system is a tautology (there must not be contradictions),
• Has not necessarily logical relationships with empirical reality (the core structure of empirical truth we use to reason). For example, an axiom can be Let X be a set of the people without heads; although there is an empirical fallacy in such statement (in order to be counted as people, the element must have a head), it is still logically valid.

Another example: Conway's Game Of Life is a Formal System that defines the rules of a particular context, but this has no relationship with reality.

The notion of formal systems is based on Systems Theory, which defines the rules by which we choose rational elements and use them for the same goal as mathematics and logic: to develop knowledge and predict the future. For example, you can develop an informal system (for example, a context, a situation) based on two theoretical facts (axioms): a) you go shopping; b) you forget your wallet. Of course, you can predict multiple situations (conclusions, which are the equivalent to theorems in a formal system) in which you can go to prison.

In other words, logical systems (formal or informal), which are essentially rational*. allow us to develop ideas as contexts isolated from reality.

* A house is just a bunch of atoms, not a set of rooms or bricks; even if you can live in a house, the idea is essentially rational, the house-system is not really physical.