Moved from HowGoedelSentencesWork.

Syntax is the set of rules which govern how all symbols are combined to form well formed formulas.  Semantics is the definition of the symbols or combinations of the symbols.

Every formal system has:
* Zero or more logical connectives: E.g. & (and), => (implies), each of which has some ''arity''. (arity = number of arguments it takes).
* Zero or more quantifiers: E.g. A (for all).
* Zero or more variable symbols:  E.g. x, y.
* Zero or more constant symbols: E.g. 0.
* Zero or more function symbols, also with an arity. 
* Zero or more predicate symbols, also with an arity.
* Zero or more pairs of parenthesis: E.g. (, ).
* Zero or more axioms.  These are usually split into two groups.  Those that detail the properties of the logical connectives, and those that detail the properties of the predicates and functions.
* At least one rule.  Rules detail the introduction and elimination of the logical connectives.

The first seven items in the above list make up the language of the first order system.  These items are not independent.  Constants can be treated as functions of 0-arity.  Other eliminations are possible.

Other logical connectives, functions, and predicates can be defined in terms of the basic ones.

In a singly typed system, the rules to describe what the legal (grammatically correct) combinations of these symbols are (Using a BNF like notation),

    Term --> Variable
         |-> Constant
         |-> Function(Term, Term, ...) // The number of terms must match the arity of the function.

    wff --> Predicate(Term, Term, ...) // The number of terms must match the arity of the predicate.
        |-> Logical Connective(wff, wff, ...)  // The number of wffs must match the arity of the logical connective.
        |-> Quantifier variable wff.

For systems with richer type system, the syntax rules become more complex.
----
For example, consider the following system.

* Round brackets: '(' and ')'
* One constant: 1
* One variable: x 
* Two predicates: =,<
* One unary function: succ
* Two binary functions: +,*
* Two logical connectives: & (and), => (implies)
* One quantifier: A (for all)

We haven't yet said what these symbols mean, but, of course, you can already guess what we mean by them.
----
CategoryLogic