 Now for the third topic in this section: what can be called encoding down. The technique is easy to understand. Suppose that we have on hand a set \(\Phi\) of first-order axioms. As is well-known, the problem of deciding, for arbitrary formula \(\phi\), whether or not it’s deducible from \(\Phi\) is Turing-undecidable: there is no Turing machine or equivalent that can correctly return “Yes” or “No” in the general case. However, if the domain in question is finite, we can encode this problem down to the propositional calculus. An assertion that all things have \(F\) is of course equivalent to the assertion that \(Fa\), \(Fb\), \(Fc\), as long as the domain contains only these three objects. So here a first-order quantified formula becomes a conjunction in the propositional calculus. Determining whether such conjunctions are provable from axioms themselves expressed in the propositional calculus is Turing-decidable, and in addition, in certain clusters of cases, the check can be done very quickly in the propositional case; very quickly. Readers interested in encoding down to the propositional calculus should consult recent  DARPA-sponsored work by Bart Selman.  Please note that the target of encoding down doesn’t need to be the propositional calculus. Because it’s generally harder for machines to find proofs in an intensional logic than in straight first-order logic, it is often expedient to encode down the former to the latter. For example, propositional modal logic can be encoded in multi-sorted logic (a variant of FOL); see (Arkoudas &amp; Bringsjord 2005). Prominent usage of such an encoding down can be found in a set of systems known as Description Logics, which are a set of logics less expressive than first-order logic but more expressive than propositional logic (Baader et al. 2003). Description logics are used to reason about ontologies in a given domain and have been successfully used, for example, in the biomedical domain (Smith et al. 2007). 