SI242: Introduction to first-order logic

Limitations of propositional logic in modeling reasoning

One of the most famous examples of a "logical deduction" is

* All humans are mortal
* Socrates is human
* therefore Socrates is mortal

... which is an example of a kind of logical deduction studied by ancient greek philosophers. On the surface, this looks like a simple application of modus ponens:

A = "Socrates is human"
B = "Socrates is mortal"
1: A => B  [Given]
2: A       [Given]
3: B       [Modus Ponens on 1 and 2]

However, if you look more carefully, you realize I have played a bit of a trick. The first line of the original is "all humans are mortal" which, in line 1 of the propositional proof I sneakily changed to "Socrates is human => Socrates is mortal". The original is a statement about all humans, but my translation into propositional logic changed that to a statement about Socrates. That does indeed make sense, but if we want to use formal logic to model reasoning, that step should be part of our logic, not outside of it.

First-order logic - part 1: objects, predicates and quantification

With the previous example in mind, we are going to extend propositional logic to produce something new and more expressive: first-order logic.

First-order logic is a big deal!

Objects: In propositional logic, a variable is an atomic black box that either spits out true or spits out false. These variables are not "about" anything, as far as propositional logic is concerned. They are just true/false values. The first big idea in first-order logic is that there is a universe of objects that the formula is about, called the domain of discourse, and we allow constant symbols in our formula, each of which represents some object from the domain of discourse (not necessarily distinct from the objects represented by other constant symbols, by the way).

Predicates: The second big idea in first-order logic is that we replace propositional variables with expressions involving "predicates" - functions whose inputs come from the domain of discourse and whose outputs are true/false values. Specifically, the propositional variable is replaced with an expression that is a predicate applied to an object.

So instead of writing

A => B

and having to understand that A stands for the proposition "Socrates is human" and B stands for the proposition "Socrates is mortal", in first order logic we might write

IsHuman(socrates) => IsMortal(socrates)

where "socrates" is a constant and "IsHuman(·)" is a predicate. Crucially, what has changed is that in propositional logic, there is no concept that "A" and "B" are in any way "about" the same thing. But in first-order logic, it is explicit that IsHuman(socrates) and IsMortal(socrates) are "about" the same thing ... the object represented by the constant "socrates".

Important: Just as variables in propositional logic have no inherent meaning, other than being true/false values, the predicates and constants in first-order logic have no inherent meaning. In the previous example, for instance, there is no idea that the constant object "socrates" is a person, or that the predicate "IsHuman" has anything to do with planet earth and a certain type of highly developed ape that lives on it. So the formula IsHuman(socrates) => IsMortal(socrates) is exactly the same as the formula IsTasty(fooditem) => IsUnhealthy(fooditem) as far as first-order logic is concerned. In other words, the names of predicates and constants do not actually imbue them with any meaning, just as the names of propositional variables do not imbue them with meaning.

Quantifiers: We are still not able to represent the assertion "all humans are mortal", because it is a statement about "all" humans, not just one or even several. first-order logic also allows for variables which, though they do take on values from the domain of discourse, differ from constants in that they do not represent just one fixed object. A variable is introduced with a quantifier, which is an assertion that a given formula holds either for all possible values of the variable it introduces or that there exists a value for the variable it introduces that makes a given formula true.

for all: $\forall x [ F ]$ - introduces a new variable $x$ with a scope (just like programming languages) delimited by the [ ] braces, and asserts that $F$ is true for all possible values of $x$. The $\forall$ is called the "universal quantifier".
there exists: $\exists x [ F ]$ - introduces a new variable $x$ with a scope (just like programming languages) delimited by the [ ] braces, and asserts that $F$ is true for at least one value of $x$. The $\exists$ is called the "existential quantifier".

Now we can finally express Line 1 from the example above: ∀x [IsHuman(x) => IsMortal(x)].

Deduction in first-order logic: Part 1

In first-order logic, predicate expressions that are syntactically identical (i.e. character-for-character the same) can be assumed to have the same true/false value

Syntactic (character-for-character) equality is the gold standard for things having the same T/F value. However, the scopes of variables introduced with $\exists$ and $\forall$ can cause problems if we re-use variable names. For example: $$ \exists x[ \text{Foo}(x,c) ] \vee \forall x[ \text{Foo}(x,c) ] $$ Here we might be tempted to say that the two occurences of $\text{Foo}(x,c)$ are syntactically identical and therefore they have the same T/F value. However, the $x$'s in these two cases are actually totally unrelated, because they come from different scopes. We can freely change the names of variables, and if we insist that each $\exists$ and $\forall$ in a formula introduces a unique variable name, we get the correct picture. Then the formula becomes $$ \exists x_1[ \text{Foo}(x_1,c) ] \vee \forall x_2[ \text{Foo}(x_2,c) ] $$ and we see that the two "Foo" experssions are not character-for-character identical, and so we cannot deduce that they neccessarily have the same T/F value.

(Warning! see the side note). Therefore, something like (IsHuman(socrates)=>IsMortal(socrates)) & IsHuman(socrates) is just like (A=>B) & A in propositional logic, and we can freely apply any deduction rule from propositional logic. However, we also get some new deduction rules that are specific to quantifiers. Here is one:

specialization (simple version): If $\forall x[F]$ is true and $e$ is a constant symbol, then the formula that results from substituting each ocurrence of $x$ in $F$ with $e$ is true.

Now we can finally prove that socrates is mortal! We model "All humans are mortal" as ∀x[IsHuman(x) => IsMortal(x)], and "Socrates is human" as IsHuman(socrates), and we have:

Given: ∀x[IsHuman(x) => IsMortal(x)] and IsHuman(socrates), prove IsMortal(socrates)
1: ∀x[IsHuman(x) => IsMortal(x)]           [given]
2: IsHuman(socrates)                       [given]
3: IsHuman(socrates) => IsMortal(socrates) [specializing x to socrates in 1]
4: IsMortal(socrates)                      [modus ponens with 3 and 2]

Important: once we specialize the variable $x$ to the particular value $\text{socrates}$, we treat predicate expressions like "$\text{IsHuman}(\text{socrates})$" and "$\text{IsMortal}(\text{socrates})$" like propositional variables ... they are just propositional variables with fancy names. When the names match, they are the same propositional variable. That's why we are able to do plain ol' modus ponens on line 4. In fact:

We can apply any propositional logic deduction in first-order logic proofs as long as we treat quantified formulas as propositional variables and predicate expressions that are outside the scopes of any quantifiers as propositional logic variables, and we only consider two formula pieces as the same propositional variable if they are character-for-character identical. So here's an example:
```
      Known facts                  Reasons                            Propositional structure
1: foo(c) => ∀x[foo(x) => bar(c)]  [Given]                         1: A => B
2: foo(c) & ~foo(d)                [Given]                         2: A & ~C
3: foo(c)                          [And elimination 2]             3: A
4: all x[~foo(x) => bar(c)]        [Modus ponens 1 and 3]          4: B	    
```
Notice that foo(c) and foo(d) are given different variable name, since they are not identical.

We can apply our rewrite/simplification rules to sub-formulas within our known facts, as long as within the subformula we treat quantified formulas as propositional variables and predicate expressions that are outside the scopes of any quantifiers as propositional logic variables, and we only consider two formula pieces as the same propositional variable if they are character-for-character identical. So here's an example:

      Known facts                  Reasons                            Propositional structure
1: ~(foo(c) & ~foo(d))                [Given]                         1: 
2: ~foo(c) | ~~foo(d)                 [De Morgan]                     2: ~(A & ~B) <=> ~A | ~~B
3: ~foo(c) | foo(d)                   [Double negation elimination]   3: ~~B <=> B
4: foo(c) => ∀x[foo(x) => bar(c)]     [Given]                         4: 
5: foo(c) => ∀x[~foo(x) | bar(c)]     [Implication rewriting]         5: C => D <=> ~C | D

ACTIVITY

Academy regulations state "midshipman do not sleep in class". We can model this in propositional logic by asserting that the following formula is true: $\forall m[ \text{isMid}(m) \wedge \text{inClass}(m) \Rightarrow \neg \text{isSleeping}(m) ]$. Given that George is a Mid, i.e. $\text{isMid}(\text{george})$, and that George is in class, i.e. $\text{inClass}(\text{george})$, can we deduce that George is not sleeping? Give a proof!
Using the same regulation: given that Gavin is sleeping and he is in class, prove that he is not a mid ... which presumably means he's the professor!
In a previous homework we had a problem in which there were two sessions for talks and a number of potential speakers. We had to express some constraints on how speakers were scheduled for sessions. One of these constraints was: "Nobody can be scheduled for both sessions." One way to write this is
```
(a1 => ~a2) & (b1 => ~b2) & (c1 => ~c2) & ...
```
... where "a1" meant that Alice was scheduled for session 1, "a2" meant alice was scheduled for session 2, and so on. With first-order logic we can express this with one simple rule! Our objects are the speakers, and we will have predicate in1(·), which is true when the argument speaker is scheduled for session 1, and in2(·), which is true when the argument speaker is scheduled for session 2. So here's the rule:
```
∀p[in1(p) => ~in2(p)]
```
Your job: Given the above rule, and given that Anuj is in session 2 or Ben is in session 2, and given that Anuj is in session 1, prove that Ben is not in session 1.