As far as I know, in a nutshell, if for a formal system $\mathcal{F}$ we have $\vdash_\mathcal{F} \exists! y \ \phi(y,x_1,\cdots,x_n)$ then we can safely introduce a new formal system $\mathcal{F}'$ that differs from $\mathcal{F}$ because it has a new function symbol $f$ and a new axiom $\vdash_\mathcal{F'} y=f(x_1,\cdots,x_n) \iff \phi(y,x_1,\cdots,x_n)$. More precisely, the new system $\mathcal{F'}$ is a conservative extension of $\mathcal{F}$.

However, sometimes it happens that new symbols are introduced even if the existential premise "$\exists! y \ldots$" is only "partial". For example, by studying $\mathcal{ZFC}$, I noted that usually intersection is only "partially defined", namely I have only $x\neq \emptyset\vdash_\mathcal{ZFC} \exists! y \ \forall u(u\in y\iff \forall v\in x(u\in v))$. By "partial", I mean that the case $x=\emptyset$ is escluded. In this case, the above scheme is not fulfilled, and I cannot introduce the new function symbol $\bigcap$ since this is not defined for $\emptyset$. Therefore, here is my first question. 1) Is there a more general scheme? Namely, is there a more general way to conservatively extend a system involving partial definitions? (I think the answer is no, but I need a confirmation)

An other common way to define intersection is to use separation, union and extentionality axioms to prove $\vdash_\mathcal{ZFC} \exists! y \ \forall u(u\in y\iff u\in \bigcup x \land \forall v\in x(u\in v))$. This solution produces a complete definition, and therefore I can extend $\mathcal{ZFC}$ introducing the new function symbol $\bigcap$ by exploiting the scheme reported above. However, this solution has different drawbacks, due to the fact that it imposes $\bigcap \emptyset=\emptyset$. For example, it is not true that $\vdash_\mathcal{ZFC} a\subseteq b \implies \bigcap b \subseteq \bigcap a$. But, this seems an apparent limitation, because I can state all the theorems (properties) about a certain $\bigcap x$ by simply adding the hypothesis $x\neq\emptyset$. For example, I can state $a\neq\emptyset,b\neq\emptyset\vdash_\mathcal{ZFC} a\subseteq b \implies \bigcap b \subseteq \bigcap a$. Actually, for this case, I could omit the hypothesys $a\neq\emptyset$, but the sense is to eliminate any occurrence of $\bigcap\emptyset$ from any reasoning, since I accept this patological definition only because I need to define the symbol $\bigcap$ for any member of the universe, not because I actually want to use it for patological cases. Therefore, here is my second question. 2) Is this way to procede correct (in general, not only for the intersection symbol)?

Thank you!

  • 2
    $\begingroup$ There's no problem with introducing partial functions: either think of them as relations - that is, replace "$f(x)=y$" with "$(x,y)\in F$" - or modify the semantics of first-order logic to allow partial functions (which basically doesn't cause any issues). $\endgroup$ – Noah Schweber Nov 26 '18 at 17:28
  • $\begingroup$ @Noah: I think Michele is worrying about the fact that even though the formal system doesn't prove (without additional assumptions) that there is a value $f(x)$, we do extend the language so that writing $f(x)$ becomes possible even without additional assumptions. In more generality, this syntactic extension is not conservative, for instance in the context of multi-sorted first-order logic, where we allow for empty sorts. By allowing the notion $f(x)$, we force the sort to be inhabited. $\endgroup$ – Ingo Blechschmidt Dec 16 '18 at 3:12
  • 1
    $\begingroup$ @IngoBlechschmidt "By allowing the notion $f(x)$, we force the sort to be inhabited." No, we can use that notation without forcing the sort to be inhabited: e.g. declare by fiat that any atomic proposition involving an undefined term immediately evaluates to "false" (note that this lets us express "$f$ is total" as "$\forall x(f(x)=f(x))$"). The notation may be suggestive of a non-empty sort, and our use of it may require a bit of semantics-juggling, but it doesn't force anything on us. $\endgroup$ – Noah Schweber Dec 16 '18 at 3:41
  • 2
    $\begingroup$ @Noah: Ah, I see. Okay. One probably needs to exert some care then in setting up the rules for existential quantification (of some calculus with respect to we want to verify soundness for), as (the formal translation of) a proof such as "Claim: $Y$ is inhabited. Proof: We have $f(x) : Y$." is not generally valid, but I'm willing to believe that this could be done. :-) $\endgroup$ – Ingo Blechschmidt Dec 16 '18 at 4:19
  • $\begingroup$ @IngoBlechschmidt Oh yes, care is definitely required! A similar comment applies to the convention that all structures be nonempty. Especially in light of category theory, allowing the empty structure generally seems preferable, and we can easily develop first-order logic for possibly-empty structures - but we would indeed need to modify our proof relation carefully to accommodate the change in semantics ("$\exists x(x=x)$" better not be a tautology in this setting!). $\endgroup$ – Noah Schweber Dec 16 '18 at 4:24

You're right to be careful, but this isn't a serious issue. Below I've outlined three basic approaches which all work.

The simplest approach is to work with relations instead of functions, conflating the function $f:X\rightarrow Y$ with its graph $G\subseteq X\times Y$. So e.g. "$\bigcap x=y$" would be shorthand for "$Intersection(x,y)$," and "$\bigcap\emptyset$ is undefined" would be shorthand for "$\forall y(\neg Intersection(\emptyset,y))$." We could in fact go right back to the set-up of first-order logic and drop functions entirely, since we truly can do everything with relations (even if sometimes it's annoying), and this gets around partiality concerns once and for all.

In practice, this is what logicians tend to do "under the hood" in my experience.

"But that's a really silly and unnatural thing to do!"

Yes, there is that. Well, in this case the fix you mentioned in the second part of your answer works perfectly well: define a "total version" of the partial function you want! No problems arise this way, as long as you're careful to keep track of the hypotheses needed to make your "totalized" operation behave as intended.

Sometimes there is a reasonable "default" to set our functions to (like $\emptyset$ in set theory or $0$ in arithmetic); a universally-applicable approach, while annoyingly arbitrary, would be to just make the function behave as the identity on a "bad" input (or be projection onto the first coordinate in the case of a multi-ary function). The details are left to the reader and are also silly.

"But that still doesn't feel right, and if our logic framework is making it hard to do math then there's something less-than-optimal with the logic side."

Honestly, I agree with this sentiment (which I'm rudely attributing to you). There are features of first-order logic I tend to (I'm inconsistent) dislike - most loudly, the restriction to partial as opposed to total functions. So let me outline how you can restructure first-order logic to allow partial functions.

There are four features we need to pay attention to:

  • What is a language?

  • What is a structure?

  • How do truth evaluations work?

  • How do proofs work?

I'm going to talk about the first three, and punt on the fourth.

  • Languages: Exactly the same. I have function symbols, relation symbols, and constant symbols, just as before. Syntactically, there is no difference.

  • Structures: Here's our first taste of freedom. A structure will now be allowed to use partial functions: e.g. if $f$ is a unary function symbol, then an $\{f\}$-structure $\mathcal{A}$ is a nonempty set $A$ together with a partial function $f^\mathcal{A}:\subseteq A\rightarrow A$.

  • Truth evaluations and satisfaction: Now we need to give a Tarski-style inductive definition of truth. The issue is that terms no longer need to refer to things. The most natural (in my opinion) fix is the "call-by-value" approach: as soon as you try to do something undefined, BOOM. Specifically, we'll leave all other clauses of the usual truth definition unchanged, but modify the atomic clause to say that any atomic formula involving a term which is not defined is automatically false - and a term with an undefined constituent is undefined. For example, if $f$ is always undefined and $g$ sends everything to $0$, then the sentence $g(f(a))=g(f(a))$ is false: it doesn't matter that both sides are literally the same expression, or that $g$ "doesn't need to look at" its input in order to decide what to output, the mere presence of the poisonous expression "$f(a)$" (either one) kills the whole setup immediately.

    • Note that we can express "$f$ is total" in this semantics: "$\forall x(f(x)=f(x))$" is true in a structure $\mathcal{M}$ iff $f^\mathcal{M}$ is total.
  • Proof system: There is as before an appropriate (= sound, complete, and recursively enumerable) proof system corresponding to the modified semantics above. Finding such a system is left as an exercise. (It is actually a good exercise, and basically involves closely reading the proofs of the soundness and completeness theorems and modifying them appropriately.)

At this point, once the above have been checked carefully, we have a basically satisfying approach; that it is satisfying for this particular context comes from further checking that adding a function symbol $f$ and the axiom "$\forall x_1,...,x_n,y[y=f(x_1,...,x_n)\iff \varphi(x_1,...,x_n,y)]$" always yields a conservative extension, regardless of what formula $\varphi$ (in the original language) you use.

  • $\begingroup$ You helped me a lot Noah! At a first impression, the second solution seems to be the most suitable to work practically, mostly thanks to its simplicity. The third solution seems to me to be really more professional (and beautiful), but it is also a way to treat undefined things with the same mechanisms we treat defined one. The trouble is if we are actually "authorized" to do that. Are we actually authorized to treat logically something like "the bag of that tree is curious"? I don't know, but this is just a different question. Thank you! $\endgroup$ – Michele Cirillo Dec 17 '18 at 10:59
  • $\begingroup$ @MicheleCirillo I'm not sure what "authorized" means. We can add whatever bells and whistles we want, as long as it doesn't interfere with what we've already decided on. In fact, there's even a name for what we're doing here: free logic. I'd argue that the answer to the question "are we actually authorized to [whatever]" is always "yes, if you can do so consistently" (are we "authorized" to add a square root of $-1$ to the real numbers?). $\endgroup$ – Noah Schweber Dec 17 '18 at 14:27
  • $\begingroup$ Sorry for my hurried answer @Noah. I not used in a correct way the comments. My "are we authorized to set UNDEF=F?" should be "The third solution is not just a tricky way to add new symbols. It is much more, since it introduces a semantics to deal with the concept of UNDEF. I encountered free logic for the first time, and so I have 1000 new questions, for example: why we should consider UNDEF=F, even if it is possible?". Now, I read that this is a debated point, and a possible alternative is the Neutral Semantic. , But all this is in the wrong place, sorry again. $\endgroup$ – Michele Cirillo Dec 17 '18 at 19:05

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.