Socratic Dictionary

First-Order Logic (FOL) Logic system

Sometimes know as predicate logic, this is the most common form of formal logic, in which the only subject of predicates and the only thing you can quantify over are individuals (objects). For example, if we have the predicates “is purple” (represented as $P$), and “is round” (represented a $R$), and an object such as a table (represented as $t$), in FOL we could say “the table is round” ($Rt$), or the “table isn’t purple” ($\neg Pt$). What we wouldn’t be allowed to say is “round is purple” ($PR$), or “purple is round” ($RP$). Notice, it isn’t that these statements are false, they are just not allowed in FOL. Sometimes we aren’t just talking about specific objects, sometimes we want to say “there exists a purple table” ($\exists x.Px$) or even “all tables are purple” ($\forall x. Px$). In logic, this is called quantification, and in FOL, you can only quantify over objects - like we did in those examples. It is against the rules to be able to construct a statement such as “there exists a round which is purple” ($\exists R . PR$). This all comes across as very sensible - it would be strange to have a system of logic where purple could be round - but that doesn’t mean that FOL is without criticism. Let’s introduce another object, a chair ($c$), and try and formalise this sentence in FOL: “the table has something in common with the chair”. It appears the only way to accurately reflect this statement would be to say, there exists some property which the chair has and the table has, but that would look like $\exists X. Xt \land Xc$. While some would argue there are ways around this, there are other statements that at least at first appear difficult to formalise in FOL (for a bit of fun, see if you could write “the table shares all properties of the chair”, “Dumbo is small for an elephant”, or “the plane flies quickly” in FOL).

Quantification Logical concept

Quantification is the logical operation of specifying how many things a proposition applies to, ranging over a domain of individuals, rather than naming any one of them directly. Say we have a predicate “is a philosopher” (represented as $P$). Instead of having to pick out each particular person and saying they are a philosopher, quantification lets us make a claim about a whole group. There are two standard quantifiers: the universal quantifier, written $\forall$ and said “for all”; and the existential quantifier, written $\exists$ and said “there exists” or “there is at least one”. “For all” allows us to say something holds for everything in a domain, for example “all humans are philosophers” becomes $\forall x.Px$ (where the domain is humans). “There exists” allows us to say that there is at least one thing in the domain. For example, “some humans are philosophers” becomes $\exists x. Px$. What types of thing you are allowed to quantify over depends on what logic system you are using, but in the most common, [first order logic](https://dailysocratic.com/dictionary/first-order-logic-fol/), you can only quantify over individuals, but in some other systems, such as second order logic, you to also quantify over predicates! One of the other interesting things about these two quantifiers, is you don’t actually need both of them. If I want to say “all humans are philosophers”, I could equivalently say “there does not exist a human who isn’t a philosopher.” If I write both of these out logically, they look quite different. The first looks like $\forall x. Px$ and the second, $\neg \exists x . \neg P x$. Yet, both appear to communicate the same idea. Similarly, if I say “no human is a philosopher”, that would look like $\forall x . \neg P x$, but the statement “there does not exist a human philosopher” communicates the exact same idea, yet would be written $\neg \exists x . Px$. As a general rule, $\forall x . \neg P x \equiv \neg \exists x . Px$, and $\neg \forall x. Px \equiv \exists x . \neg P x$. (note: for some logical systems this isn't true, but it is in [FOL](https://dailysocratic.com/dictionary/first-order-logic-fol/))