# First Order Logic

# Overview

Here, we'll go over a variation of first order logic (skipping equality and functions) and construct a deductive system.

First order logic allows you to represent statements about the world and an interpretation system that allows you to arrive at conclusions based on logical deductions.

For example:

`// There is an individual l whose name is Leo`

Leo(l).

// There is an individual s whose name is Sam

Sam(s).

// Sam is a parent of Leo

Parent(s, l).

// For every parent x of y, y is a child of x

forall(x, y) (Parent(x, y) => Child(y, x)).

// Is Leo a child of Sam?

Child(l, s)?

# Syntax

The syntax of our variant of first order logic will use the following grammar:

`Program = (Statement | Question)*;`

Statement = Expression ".";

Question = Expression "?";

Expression = Predicate "(" Term, ... ")" |

"(" Expression Connective Expression ")" |

Quantifier "(" Variable, ... ")" Expression |

"~" Expression;

Term = Constant | Variable | Literal;

Literal = "true" | "false";

Connective = "&&" | "||" | "=>" | "<=>";

Quantifier = "exists" | "forall" ;

Constant = "A" | "X1" | "John" | ... ;

Variable = "a" | "x" | "s" | ... ;

Predicate = "Before" | "HasColor" | "Raining" | ... ;

There is an infinite set of individuals in the world that can be named with `Constants`

(e.g. `Alice`

, `John`

, `0`

, `1`

, etc), an infinite set of `Variables`

(e.g. `x`

, `y`

, etc) and two `Literals`

(`true`

and `false`

).

A `Variable`

, a `Constant`

or a `Literal`

is a `Term`

.

There is an infinite set of `Predicate`

s (e.g. `Man`

, `Mortal`

, `Parent`

etc).

A `Predicate`

can be connected to `t1, ..., tn`

`Terms`

to form an **Atomic** `Expression`

using `P(t1, ..., tn)`

. For example:

`// There is an individual "p", and individual "q" and "p" is a Father of "q".`

Father(p, q)

There are binary `Connectives`

(`and`

, `or`

, `=>`

, `nand`

, `xor`

).

If `P`

and `Q`

are expression and `C`

is `Connective`

, then `P C Q`

is a **Connected** `Expression`

. For example:

`// The individual "s" is a Philosopher and Greek`

Philosopher(s) && Greek(s)

There is a unary `Connective`

(`~`

).

If `P`

is an expression, then `~P`

is a **Negated** `Expression`

. For example:

`// The invidual "s" is not Alive`

~Alive(s)

There is the universal quantifier (`forall`

) and the existential quantifier `exists`

.

If `P`

is an `Expression`

and `x`

is a variable, then `forall(x) P`

(for all `x`

, `P`

holds) and `exists(x) P`

(for some `x`

, `P`

holds) are **Quantified** `Expressions`

. For example:

`// Every man is mortal`

forall(x) (Man(x) => Mortal(x))

// There exists a man who is Socrates

exists(x) Socrates(x)

An `Expression`

followed by the punctuation marker `.`

is a `Statement`

.

`// I'm stating that "Every man is mortal".`

forall(x) (Man(x) => Mortal(x)).

An `Expression`

followed by the punctuation marker `?`

is a `Question`

.

`// I'm asking "Every man is mortal"?`

forall(x) (Man(x) => Mortal(x))?

A `Program`

(or dialog) is a series of `Statements`

and `Questions`

.

For example:

`// s is an individual named Socrates`

Socrates(s).

// Socrates is a man.

Man(s).

// Is Socrates mortal? True.

Mortal(s)?

Another example:

`// Everything is awesome`

forall(x) Awesome(x).

// Is Socrates awesome? True.

Awesome(s)?

Quantified questions:

`// Every man is a person`

forall(x) (Man(x) => Person(x)).

// Every person is a mortal

forall(x) (Person(x) => Mortal(x)).

// Is every man mortal?

forall(x) (Man(x) => Mortal(x))?

# Interpretation

## Rules of Inference

In addition to the inference rules of Propositional logic we'll add a couple more:

The first, universal elimination, allows us to exchange an universally quantified `Variable`

for a `Constant`

. For example:

`forall(x) Awesome(x).`

Awesome(s)?

This is interpreted as `true`

, because:

`forall(x = s) Awesome(x = s).`

Awesome(s).