Skip to main content
2 of 2
added 39 characters in body
Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331

It's quite simple: in a structure with a single object - and for simplicity, let's assume only unary relations at first - we think of each unary relation as a single atomic proposition, and of the single object as a "propositional world." (What about multiple worlds? Well, thinking in this direction can take us into propositional modal logic - specifically, Kripke frames - and explains why that can be thought of as a fragment of first-order logic.) Quantifiers are stripped away, since they only point to the single object, and the unary predicates get replaced by corresponding propositional atoms.

For an example of how this works, the first-order sentence $$\exists x\forall y(P(x)\vee Q(y))$$ is thought of as the propositional sentence $$p\vee q.$$

Binary, or indeed $n$-ary, relations are no different from unary relations since there is only one object; so similarly, $$\exists x\forall y(P(x)\vee (Q(y)\wedge R(x,y)))$$ would be thought of as $$p\vee (q\wedge r).$$


Specifically, here's the theorem:

Working in a relational language, let $\varphi\mapsto\varphi^*$ be the map from first-order sentences to propositional sentences described (informally) above. Then for every first-order sentence $\Sigma$, we have $$\Sigma\cup\{\forall x,y(x=y)\}\vdash_{first-order} \varphi\quad\iff\quad \Sigma^*\vdash_{propositional} \varphi^*$$ (where $\Sigma^*$ is shorthand for $\{\sigma^*:\sigma\in\Sigma\}$). And of course by the completeness theorems for each logic we can alternate between "$\vdash_{...}$" and "$\models_{...}$" as desired.

It is worth noting that the theorem above assumes the usual semantics for first-order logic, which outlaws the empty structure. If you prefer to allow the empty structure, just add "$\exists x\forall y(x=y)$" to $\Sigma$ instead of "$\forall x,y(x=y)$."


What about function symbols?

Well, one natural reflex (and something I wrote blithely in a previous edit) is to replace function symbols with relations representing their graphs, and add axioms saying that those relations behave like functions. But this is really silly: since there's only one object, every equality is true. So we can forget about function symbols completely and simply treat every expression of the form $t_1=t_2$ as "true" $\top$ and every expression of the form $t_1\not=t_2$ as "false" $\perp$. So e.g. $$\exists x\forall y(P(x, f(x))\vee f(x)\not=y\vee Q(y))$$ turns into $$p\vee\perp\vee q$$ which is equivalent to $$p\vee q.$$

Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331