# Definition:Language of Predicate Logic/Bourbaki

## Definition

There are many formal languages expressing predicate logic.

The formal language used on $\mathsf{Pr} \infty \mathsf{fWiki}$ is defined on Definition:Language of Predicate Logic.

This page defines the formal language $\LL_1$ used in:

Explanations are omitted as this is intended for reference use only.

### Alphabet

#### Letters

The letters used comprise two classes:

#### Signs

The signs used are the following:

 $\ds \lor$ $\ds :$ the disjunction sign $\ds \neg$ $\ds :$ the negation sign $\ds \Box$ $\ds :$ signifying a quantified variable $\ds \tau$ $\ds :$ signifying an existential quantifier

and are called "logical signs".

### Collation System

The collation system used is that of Bourbaki assemblies.