Proposition

A proposition is an object from the well-formed formulae of the First-Order Signature associated with the predicates. They denote truth values in the First-Order Predicate Logic.

It is made up of:

• all predicates applied to maximum of $k$ well formed Terms
• the value true $T$
• if $A,B$ are propositions and $X$ is a Term
  • $A\land B$
  • $\neg A$
  • $\forall X.A$
    • $\forall$ is a binding operator called the Universal Quantifier