sgo.to

First Order Logic

Sam Goto

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 Predicates (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).

Unification