I sent a mail to Leslie Lamport about this topic. He kindly asked me to post our messages.
____________________________________________________
I read the thread "Partial Functions" on the TLA+ Google group. Hereunder is my account about this subject.
First of all I am an engineer, not a mathematician.
In France, during all my education after the elementary school, from the age of 11 in 1969 to the age of 23 in 1981, I was taught "mathématiques modernes" (
http://fr.wikipedia.org/wiki/Mathématiques_modernes <
http://fr.wikipedia.org/wiki/Mathématiques_modernes> ), in the direct line of Bourbaki.
There was a clear difference between "une fonction" (a function) and "une application" (a total function). When we studied a function, the first thing to do (the first question of the exercise) was to define the "domaine de définition" (domain) of the function.
I retrieved my course notes from my first year post high school (I was in class of "mathématiques supérieures" -
http://en.wikipedia.org/wiki/Classes_Préparatoires <
http://en.wikipedia.org/wiki/Classes_Préparatoires> ).
------------------------------
--------------------------------------------
Definitions.
Let E and F be sets.
. A graph is a sub-set of E \x F.
. A "relation" (binary relation) between E and F is a triple (E,F,G) where G is a graph from E \x F.
. A "fonction" (function) f is a "relation" (E,F,G) for which the following
holds: if (x, y) \in G and (x,y') \in G then y = y'.
. The "domaine de définition" (domain) of a function f is D(f) = {x \in E:
\E y \in F : (x,y) \in G}
. An "application" (total function) is a function f for which the following holds: D(f) = E. In other words it is a "relation"
for which the following holds: \A x \in E : \E! y \in F such that (x,y) \in G. Therefore, we can write y = f (x).
[In France, we use \E! for "there exists one and only one"]
Property
For each "fonction" (function) there is a related "application" (total function).
[Today I realize that "the" related one was the one with the "biggest"
domain.]
------------------------------
----------------------------------------------
According to the above property, we used (teachers and students) the word "fonction" for "application", except when the difference of meaning mattered.
I know you can read French:
http://fr.wikipedia.org/wiki/Application_(mathématiques) <http://fr.wikipedia.org/wiki/Application_(mathématiques)> (especially section 1).
Yours faithfully,
Dominique Couturier
____________________
Dear Dominique,
[...]
Thanks for the information. So, suppose you proved a theorem in a class on real-valued functions, and in a class on complex-valued functions you had a function f with f(x) a real number for all x in its domain. You then couldn't have applied to f any of the theorems you proved in the earlier class were for functions (E, F, G) with F the set of reals and f has F equal to the set of complex numbers. I wonder why people make so unnecessarily complicated. Did you ever encounter any occasion in which adding the E and F to the definition of a function was helpful? In any event, I will use the term "simple" instead of "usual", since \ simplicity seems to be unusual in this world.
[...]
By the way, I'm curious: What were you taught was the meaning of f(x) when x is not in D(f)? If the answer was "you weren't allowed to write it", then that would mean you couldn't write \A x : (x \in D(f)) => P(f(x)) for some predicate P.
Cheers,
Leslie
______________________
Dear Sir,
[...]
4/ What were you taught was the meaning of f(x) when x is not in D(f)?
Remember that if you write f(x), implicitly f is a total function and x \in D(f). So you were not allowed to write tan(pi/2). If ever you wrote it on the blackboard, the teacher would probably cry out: Horreur ! Get out of my classroom at once!
5/ Paradoxically, it doesn't mean we couldn't write \A x : (x \in D(f)) => P(f(x)). Because if x \in D(f) is false, we do not need to "evaluate" f(x) : (false => M) is true whatever the value of M, then (x \in D(f)) => P(f(x)) is true.
It was not an explicit rule given to the students, but I think all of us thought this way.
I think we used (without realizing what we did) kind of 'moderate' interpretation of logic, as you call it in your book "Specifying Systems".
You know, formal logic was not the main concern of Bourbaki!
6/ Do remember that I am not a mathematician, and I was in "maths sup" 37 years ago.
Yours faithfully,
Dominique Couturier
________________________
Hi Dominique,
[...]
>4/ What were you taught was the meaning of f(x) when x is not in D(f)?
>
>Remember that if you write f(x), implicitly f is a total function and x \in D(f). So you were not allowed to write tan(pi/2). If ever you wrote it on the blackboard, the teacher would probably cry out: Horreur ! Get out of my classroom at once!
>5/ Paradoxically, it doesn't mean we couldn't write \A x : (x \in D(f)) => P(f(x)). Because if x \in D(f) is false, we do not need to "evaluate" f(x) :
(false => M) is true whatever the value of M, then (x \in D(f)) => P(f(x)) is true.
>It was not an explicit rule given to the students, but I think all of us thought this way.
>I think we used (without realizing what we did) kind of 'moderate' interpretation of logic, as you call it in your book "Specifying Systems".
Well, I’m glad you were using what I regard as the simple, natural way to interpret something like 1/0: it’s some unspecified value, which might equal 42 or the set of quaternions or anything else. Some people think it should have a special non-value “undefined”, which leads to the complication of having to deal with three-valued logic.
>You know, formal logic was not the main concern of Bourbaki!
I know they were mathematicians, and formal logic isn’t the main concern of mathematicians. However, I thought that they wanted to build all of math from axioms and definitions, and they wanted it to be rigorous. You can’t avoid this issue if you do that. However, you can avoid mentioning it. I suspect that their attitude was that they never discussed meaning. Math is just a set of rules that tells you how to prove things about well-formed (syntactically correct) formulas. Since 1/0 \in Reals is a well-formed formula, you can ask whether you can prove it from the axioms. There’s a problem only if the axioms aren’t sound, which means you can prove FALSE. Engineers aren’t satisfied with that view of math (and I expect mathematicians aren’t satisfied with it either, but they were when I was in school), so I felt obliged to write that section oo “silly formulas”.
[...]
Leslie
_________________