# Variant of free logic that accepts domain emptiness but rejects non-referring terms

To my naive perspective, domains that might be empty and terms that fail to denote (via constant symbols that don't refer or partial functions) feel radically different. The former seems ordinary and the latter seems quite novel.

The SEP article on free logic mentions the following passage about free and inclusive logics and the differences between them (emphasis mine).

Classical predicate logic presumes not only that all singular terms refer to members of the quantificational domain D, but also that D is nonempty. Free logic rejects the first of these presumptions. Inclusive logic (sometimes also called empty or universally free logic) rejects them both. Thus while inclusive logic for a language containing singular terms must be free, free logics need not be inclusive.

This leaves open the possibility of accepting domain emptiness and rejecting non-referring terms. I didn't see any mention of it in that article or the one on second and higher-order logics, which seems to mostly focus on model theory, semantics, and decidability.

Allow empty domains while rejecting partial functions and non-referring constants seems very, very familiar to me and I'm wondering if systems with this property have a name.

The following is a personal "notation" of sorts that I've been using for years without carefully examining; I'm including it here in the hopes that it'll be familiar to folks with a similar background and to provide motivation for the question. The purpose for the notation (which is really just higher order logic used without a fixed deductive system accompanying it) is to resolve ambiguities related to quantifier scope in natural language when explaining things or taking notes.

The syntactic convention I'm most familiar with for informal/quasiformal use is cobbled together from some experience I have with programming, basic type theory, math, and semantics of natural languages. Anything vaguely collection-like can appear after the `:` and `→` builds larger types or "things that can be quantified over" by making a collection of functions. Maybe others use a similar notation informally, I'm not sure.

``````∀x:A→B.P(x)∧Q(x)
``````

In such a system, empty domains do not cause any problems. A `forall` statement is always true when the domain is empty and an `exists` statement is always false.

Terms that don't refer however, cause serious problems because the whole resulting well-formed formula will fail to "type check". I usually handled them with relations or a special sort that included a designated bottom element (similar to an option type in programming).

• So singular terms do refer to members of the quantification domain D... which might be empty. In other words, they are non-referring. The only way I can see this working is to disallow any singular terms, which just gives you standard predicate calculus without individual constants. But one can reintroduce those through definite descriptions anyway. And they must sometimes be non-referring if empty domains are allowed. Jan 19, 2021 at 6:42
• May I ask why? :) Like, is there a problem a non-classical logic would address? Jan 19, 2021 at 8:59
• We need to clarify whether we have a single quantificational domain with typeless variables, or a many-sorted logic. The SEP article assumes the former. Under that assumption, there is no point having a logic that describes an empty domain with no non-referring terms, since that would leave nothing to refer to. In your example sentence, A and B appear to be types, so you presumably want to have typed variables and to allow some types to be uninstantiated. This should be OK provided at least one of your types is instantiated and you are careful about how you express the instantiation rules. Jan 19, 2021 at 11:56
• I didn't want to over-emphasize my personal notation in the question, but the way I was thinking of it there are many sorts (types) and constants have to be known to have a certain type in order to be used. In a certain sense, the sorts in my notation are also extra-logical, in addition to function and constant symbols. I don't think the notation I described is really coherent or forms a complete system by itself, but it does have the property of permitting empty domains and lacking non-referring terms, so I'm interested in real approaches that also have that property. Jan 19, 2021 at 21:59

The variant of free logic that permits domains to be empty, but rejects non-referring terms is simply first-order logic.

Some presentations of first-order logic allow the domain to be empty, others require it to be non-empty.

For example, in Alex Kruckman's lecture notes, first-order logic potentially has multiple sorts and allows the domain of any of the sorts to be empty.

In settings where (an) empty domain(s) is/are allowed, using a constant symbol at all has the effect of ruling out intepretations with an empty domain.

However, this not special. Any non-logical symbol must be interpreted. Using a predicate symbol R or non-nullary function f requires the interpretation to attach a meaning to R or f. Constant symbols rule out structures with empty domains in precisely the same way that the predicate symbol R rules out a structure that does not assign a meaning to R.

• The terminology for the nonstandard FOL with empty domain is just called inclusive logic, it has several technical inconveniences one of which is particularly related to variable interpretation (assignment function): the definition of truth in an interpretation that uses a variable assignment function cannot work with empty domains, because there are no variable assignment functions whose range is empty...This technique does not work if there are no assignment functions at all; it must be changed to accommodate empty domains... Feb 7, 2022 at 5:09
• @DoubleKnot, I don't think there's consensus on terminology. According to the SEP article, inclusive logic permits partial functions and non-referring constants as well. Also, the variable assignment approach does work if you restrict variable assignments to only assign values to the open variables of a wff. Then you get one variable assignment when the model has an empty domain and the formula is closed and zero otherwise. From what I can tell, there are other ways presentation can vary for FOL as well, such as whether non-normal models exist (i.e. whether `=` enforces meta-level sameness). Feb 7, 2022 at 5:35
• Seems to me your SEP ref allows partial function interpretation for its nonlogical functional symbols in its signature, not about the variable assignment function though (My WP ref explicitly asserts assignment has to be range-non-empty). So even you only want to "restrict variable assignments to open variables of a wff" in the case of an empty domain, above said Tarski semantics technique doesn't work and needs to be changed just to accommodate such edge case. Like in coding ultimately you weigh your a few options regarding edge cases... Feb 7, 2022 at 6:00
• In (mathematical) practice, first-order logic is not often studied by itself, but is instead used as a stepping stone to something more powerful, such as set theory or Peano arithmetic. For axiomatic set theory in particular, you usually either have the axiom of infinity or the axiom of the empty set, both of which assert that at least one set exists (so the domain cannot be empty). Most any reasonable set theory will at least have an empty set, so this isn't really something you can work around. Similarly, PA requires the existence of the natural numbers. Mar 9, 2022 at 6:05