Axiomatic semantics: The notion of theory

p 297
A theory may be viewed as a formal language, or more properly a
*metalanguage*, defined by syntactic and semantic rules.

The syntactic rules for the metalanguage, or *grammar*, define the
meaningful statements of the theory, called *well-formed formulae*.

p 298
Given a grammar for a theory [...] we need a set of rules for
*deriving* certain formulae, called *theorems* [...].

To derive theorems, a theory usually provides two kinds of rules:
*axioms* and *inference rules*, together called "rules".

pp 299-300
An axiom *schema* [...] refers to arbitrary integers expressions.

In practice, most interesting axioms are in fact axiom schemata.

Inference rules are mechanisms for deriving new theorems from olders.
An inference rule is written in the form

	f1, f2, ..., fn
	---------------
	       f0

The formulae above the horizontal bar are called the *antecedents* of
the rule; the formula below it is called its *consequent*.

The mini-theory of integers needs an inference rule, useful in fact
for many other theories. The rule is known as *modus ponens* and makes
it possible to use implication in inferences.

p 301
The mechanism for deriving a theorem [is] called a *proof*.

pp 302-303
Conditional proof
Proof by contradiction