Category:Predicate Calculus

Definition

The language of predicate logic can be defined as a formal system.

In order to do this, we need to specify the various components of this: the alphabet, the WFFs, the syntax and the axioms.

When expressed thus, predicate logic is referred to as the predicate calculus.

In fact, there is more than one way to define predicate logic as a formal system.

So although it is referred to as the predicate calculus, it is preferable to talk about a predicate calculus.

However, it is worth pointing out that although the formalizations themselves may vary considerably, the underlying system of logic that they define is in fact the same.

Similarly with propositional calculus being referred to as PropCalc, it is often abbreviated to PredCalc.

Definitions specific to this category can be found in Definitions/Predicate Calculus.

Specification

The predicate calculus can be expressed as a formal system.

We will use $\mathcal L_1$ to represent the formal language used to define predicate calculus as follows.

The Alphabet of Predicate Calculus

Vocabulary

The vocabulary of $\mathcal L_1$ can be defined as the following set $\mathcal P$ of more-or-less arbitrary symbols:

$\mathcal P = \left\{{\mathcal P_0, \mathcal P_1, \ldots, \mathcal P_k, \ldots}\right\}$

such that each $\mathcal P_n \in \mathcal P$ is a set of $n$-ary predicate symbols for each natural number $n \in \N$.

At least one of the sets $\mathcal P_n$ is non-empty.

The set $\mathcal P_0$ is a set of propositional symbols as in the Alphabet of Propositional Calculus.

In addition to the propositional symbols and signs of propositional calculus, the following are primitive symbols of predicate calculus:

Predicate Symbols

The predicate symbols, from $\mathcal P_0, \mathcal P_1, \mathcal P_2, \ldots$.

Variable Symbols

An infinite set $VAR = \left\{{x, y, z, x_0, y_0, z_0, x_1, y_1, z_1, \ldots}\right\}$ of symbols called variables.

Parameters

A set $\mathcal K$ of symbols called parameters.

Quantifiers

The quantifiers are:

• The universal quantifier $\forall$;

• The existential quantifier $\exists$.

Punctuation

The punctuation symbols used are:

The left parenthesis, right parenthesis, colon and comma: $( \ , \ : \ )$.

Each of the symbols of $\mathcal L_1$ is considered to have length of $1$.

The variables and parameters are referred to collectively as individual symbols.

WFF with Parameters

The set of all WFFs formed from the vocabulary $\mathcal P$ with parameters from $\mathcal K$ can be denoted $WFF \left({\mathcal P, \mathcal K}\right)$.

Relations

Let $X^n$ be the set of all length $n$ sequences: $\left({x_1, x_2, \ldots, x_n}\right)$ of elements from $X$.

The set of all $n$-ary relations on $X$ can be denoted $REL_n \left({X}\right)$.

Thus:

• The set $X^1$ is the same as $X$, and a unary relation on $X$ is a subset of $X$.
• The set $X^2$ is the same as $ X \times X$, and a binary relation on $X^2$ is a subset of $X^2$

The $0$-ary relations on $X$ correspond to truth values, thus:

The only sequence of length $0$ is the null sequence $\left({}\right)$.

So $X_0 = \left\{{\left({}\right)}\right\}$.

There are two $0$-ary relations on $X$:

The empty set $\varnothing$ corresponding to the truth value $F$;

The set $X_0 = \left\{{\left({}\right)}\right\}$ corresponding to the truth value $T$.

WFFs of Predicate Calculus

A WFF of predicate calculus, or predicate WFF, can be specified in the following ways:

Formal Grammar: Backus-Naur Form

A WFF of $\mathcal L_1$ is a string generated by the following formal grammar expressed in Backus-Naur form:

Note that this is a top-down grammar: we start with a metasymbol <formula> and progressively replace it with constructs containing other metasymbols and/or primitive symbols, until finally we are left with a well-formed formula of $\mathcal L_1$ consisting of nothing but primitive symbols.

Formal Grammar: Bottom-Up Approach

A WFF of predicate calculus $\mathcal L_1$ is a string generated by finitely many applications of the following rules of formation.

Let $Op = \left\{{\land, \lor, \implies, \iff}\right\}$.

Any string which can not be created by means of the above rules is not a WFF.

Atomic WFF

An atomic WFF of predicate calculus is a WFF of the form:

• Any propositional symbol of the alphabet of Propositional Calculus $\mathcal P_0$;

• $p \left({u_1, u_2, \ldots, u_n}\right)$, where $u_1, u_2, \ldots, u_n$ are individual symbols, and $p \in \mathcal P_n$ is an $n$-ary predicate symbol.

Abbreviation of WFFs

The WFFs of predicate calculus can be made more readable by allowing them to be abbreviated. The resulting strings are not actually WFFs as such, but can be translated back uniquely into full WFFs.

Rules for Abbreviation of WFFs

The rules of abbreviation for propositional calculus continue to hold.

In addition, the following also apply.

• We use $\dot =$ instead of $=$ to indicate a predicate symbol which corresponds to equality in the formal language. This is so as to avoid confusion between it and the usual equality symbol used outside of predicate calculus.

• Certain binary predicates like $\dot =$ and $<$ are usually written between the variables (e.g. $x < y$ instead of using the formal $<\left({x, y}\right)$. This convention is known as infix notation.

• So as to ensure that the natural precedence order is not confused, it is often a good idea to insert brackets round the quantifiers, for example: $\left({\forall x: P \left({x}\right)}\right) \implies q$ instead of $\forall x: P \left({x}\right) \implies q$, which could get confused with $\forall x: \left({P \left({x}\right) \implies q}\right)$.

Any string obtained from a WFF $\mathbf A$ by applying any of the above rules is called an abbreviation of $\mathbf A$.

The string obtained by applying as many of the above rules to a WFF $\mathbf A$ as possible is known as the standard abbreviation of $\mathbf A$.

Thus it can be seen that there may be several abbreviations of a WFF, but only one standard abbreviation.