Definition:Language of Predicate Logic/Bourbaki

From ProofWiki
Jump to navigation Jump to search


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.



The letters used comprise two classes:

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.


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".

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.

Collation System

The collation system used is that of Bourbaki assemblies.

See the $\mathsf{Pr} \infty \mathsf{fWiki}$ definition.

Formal Grammar

Also see