Maths - Predicate Logic

Predicate Logic (or also called Predicate Calculus) is the term for a formal and symbolic system of logic like first-order logic, second-order logic and so on.

It is defined over some (possibly infinite) set. It requires some form of assignment or relationship of the elements of the set to give true or false values.

Terms

Constants

Values have two values ether true of false, we may use alternative names as follows:

true
1
T  
false
0
_|_  

Variables

A variable is a letter or symbol used to represent a value (an object, not a proposition). A predicate containing variables can be made into a valid proposition if the variables are either:

Functions

Composite terms are formed by applying function symbols to other terms. Each function symbol has an 'arity' that is it takes in 'n' parameters and returns 'm' parameters.

Quantifiers

universal quantifier: for all for all
existential quantifier: there exists there exists (for some)

For universal quantifier we will use the notation for allx:σ.A(x) which is true if A(x) is true for every 'x' in type 'σ', where:

So,

for allx:σ.A(x) = A(a) /\ A(b) /\ ...

where a:σ, b:σ ... are all objects in discourse.

Simarly for existential quantifier we will use the notation there existsx:σ.A(x) which is true if A(x) is true for at least one 'x' in type 'σ'

there exists x:σ.A(x) = A(a) \/ A(b) \/ ...

where a:σ, b:σ ... are all objects in discourse.

Introduction Rules

for all there exists
A
for allx.A
(for allI) x not free in A
A[t/x]
there existsx.A
(there existsI)

Elimination Rules

for all there exists
for allx.A(x)
A[x/t]
(for allE)
 

[A]

...

there existsx.A B
B
(there existsE) x not free in B

Formulas

If x1, … ,xn are elements of the set and P is an n-place predicate symbol, then

P(x1, … ,xn) is an elementry formula

If A and B are formulas, then

are also formulas.

Connectives

Commonly used logical connectives include:

Programming

Formation Rules

for all there exists
 

[x:A]

...

A is a type P is a type
(for allx:A).P
(for allF) P is a type on the assumption that x is a variable of type A
 

[x:A]

...

A is a type P is a type
(there existsx:A).P
(there existsF) P is a type on the assumption that x is a variable of type A

Introduction Rules

for all there exists

[x:A]

...

.p:P
(λ x:A).p : ( for allx:A).P
(for allI) x not free in A
a:A p:P[a/x]
(a,p):there exists(x:A).P
(there existsI)

Elimination Rules

for all there exists
a:A f: (for allx:A).P
f a:P[a/x]
(for allE)
p:there exists(x:A).P
fst p:A
p:there exists(x:A).P
snd p: P[fst p/x]
(there existsE) projections

Computation Rules

for all there exists
((λ x:A).p a -> p[a/x] fst (p,q) -> p
snd (p,q) -> q

 


metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

cover Modern Graph Theory (Graduate Texts in Mathematics, 184)

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.