Many non-classical logics are first introduced without a corresponding first order version. I'm thinking about things like modal logic, intuitionistic logic or partition logic here. My experience and expectation is that there normally is also some kind of "canonical" first order logic available, but that things like equality and functions can become "annoying". Since it is common to omitt annoying things like many-sorted typing in normal first order logic, I figured out that omitting equality and functions might often be OK.

The last time I asked a question about omitting equality and functions, I also omitted constants. While omitting equality was certainly central to that question, and omitting functions certainly simplified things, I'm no longer sure whether omitting constants was a good idea. I omitted them for that question, because I was too lazy to figure out whether they would changed the answer. One reason why omitting constants might be a bad idea is that open formulas are an "organic" part of first order logic, and a constant is quite similar to an unbound variable. Also, having constants forces one to think about some of the semantic issues that would be raised by having functions, without all the technical complications that functions can cause.

My concrete problem is that I want to write down a first order version of partition logic, and I'm wondering what might be an appropriate minimal subset of first order logic for that task.

  • Tell me if I understand your project correctly: you want to find the least expressive first-order language (minus: identity, non-nullary functions) that will allow you to express the primitive notions and formulas of partition logic. Similar projects have been carried out by van Benthem, for example, leading to a "correspondence theory" between modal logics and FOL. Are you basically aiming to do the same for partition logic? – Hunan Rostomyan Mar 28 '14 at 21:25
  • 1
    @HunanRostomyan The available publications about partition logic treat it as a propositional logic, i.e. there are no variables in the language. So I want to add variables to the language, and probably also the "forall" and "exists" quantifiers if possible. I'm not necessarily looking for the least expressive first-order language, a convenient subset without too much technical complications and ontological commitments will just be fine. Now I wonder whether constants would be important, even if they might carry some ontological commitments. – Thomas Klimpel Mar 28 '14 at 21:58

First-order is a language : individual variables and quantifiers ranging over a doamin of objects and no quantification over subset of teh domain (

To build up a first-order* theory, of course, we need axioms i.e. "distinguished" sentences of the language stating some "assumed" truth that we will use to characterize the general properties of the domain of discourse we are interested in.

Of course, we need also inference rules.

In order to make this machinery at work, to formulate a theory we need at least a predicate to be "selected" for the theory itself : set theories (like ZFC) use the "membership" relation (∈) and the "equality" relation (=).

In f-o PA (Peano's arithmetic) we need an individual constant (0), a binary relation (=), an unary fucntion (S) and two binary functions (+ and x).

We may consider a "level-zero" theory with only one binary relation : = ; it is the identity theory. With it we may state general properties of all (non empty) domains of discourse. Principle like (forall x )(x = x).

I suppose that all mathematical theories need equality, but this fact does not, in principle, entails that all interesting f-o theories need it.

Same as for individual constant (like 0 and the emptyset) : they are used for denoting distinguished elements of the domain.

  • I have no problem, if individual theories decide that they need equality, and take care to state the required axioms for the equality predicate explicitly. By doing so, they will restrict the possible models in ways appropriate for them. (However, I wouldn't call this "level-zero" theory.) This brings up the interesting question, if they can do the same for functions (or constants), if functions are not part of the "logical language". I will have to think about this, but this seems to be an important aspect. – Thomas Klimpel Mar 29 '14 at 12:51

Because I read the claim that intiutionistic logic is the logic of open subsets, let's describe a first-order semantics for a logic of open subsets, without equality and functions, but with many-sorted typing.

Let's assume we have a finite number of types α, β, ... for typing variables (so that a variable x of type α can be written as x:α) and a type *, which is the type of propositions. (Notation from The Seven Virtues of Simple Type Theory.) For each type α, a corresponding topological space X_α must be given. For each atomic proposition P, an open subset of the topological space X_* must be given. For each "atomic" predicate P(x:α, y:β), an open subset of the topological product space X_* x X_α x X_β must be given.

An open formula with free variables x:α and y:β will define an open subset of the topological product space X_* x X_α x X_β. If the classical interpretation of an operation like negation (¬P) or implication (P⇒Q) would lead to a non-open subset, it will be forced to an open subset by taking the (topological) interior of the non-open subset. The commonly used intuitionistic operations are the false proposition ⊥, the binary logical operations "and" ∧, "or" ∨, and "implication" ⇒, as well as the quantifier ∀ and ∃. For example ⊥ corresponds to the empty set (which is an open subset for any topological space), and the "and" P∧Q of two predicates P and Q is given by the intersection of the open subsets P and Q.

The definitions of P∨Q and ∃x:α.P are similarly unproblematic, but P⇒Q and ∀x:α.P require ensuring that the result is an open subset by taking the interior. The "implication" P⇒Q of two predicates P and Q is given by the interior of the union of the complement of P (in the corresponding product space) and the open subset Q. The universal quantification ∀x:α.P of a predicate P is given by the interior of the intersection over all x (in X_α) of the open subsets P|x.

Note that the semantics of constants was omitted, but the semantics of ∀x:α.P implicitly used a "very similar" concept. Defining the semantics of constants is easy (and doesn't require to take the interior of an intermediate result), so there seems to be no good reason to omit constants.

On the other hand, defining the semantics of equality would be quite annoying, because the formula x:α=y:α doesn't really define an open subset of the topological product space X_* x X_α x X_α. Taking the interior will definitively create confusion, because the formula x:α=x:α seems to correspond to the entire space X_* x X_α (which is an open subset). Note that for a normal predicate P(x:α, y:α), the formula P(x:α, x:α) canonically defines an open subset of X_* x X_α (and doesn't require to take the interior of an intermediate result), without any risk to create confusion. Hence there are good reasons to assume that omitting equality will simplify things enough to justify the occurred loss in expressivity.

Omitting the semantics of functions might be less clear cut for intuitionistic logic. Because nearly all first order formulations of intuitionistic logic include functions, I strongly suspect that they don't cause any harm. However, it still requires some work to figure out an appropriate semantics, and just because functions don't cause any harm for intuitionistic logic doesn't mean that functions won't cause any harm for partition logic either. So omitting functions should be OK, if equality is already omitted.

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.