proof
A key feature of the methods of mathematics, going back as far as ancient Greece, is the role of proof.
Though mathematics results may be discovered by diverse means of varying reliability.
They remain conjectures until they have been verified by proof.
Though the construction of a proof may be difficult its checking is expected to be routine, so that there remains no doubt in the conjecture once its proof has been checked.
The primary purpose of a logical foundation for mathematics is to provide a context in which the checking of mathematical proofs can be conducted.

syntax
The first formal element required of a logical foundation system is a formal definition of the syntax of the language in which mathematical conjectures are to be expressed.


typecorrectness
Some foundation systems make use of "type constraints" supplementary to the basic syntactic wellformedness conditions.
In some cases these additional conditions are decidable, and seem like an extension to the syntax, in other cases they are not decidable and welltypedness must itself be demonstrated by a proof, making typecorrectness rule seem like an aspect of the deductive system.
In more extreme cases (adopting the "propositions as types" paradigm) the entire deductive system is absorbed into the typecorrectness proof.

derivations
A key feature of formal logical systems in general (and hence of formal logical foundation systems for mathematics) is that the correctness of proofs is characterised by purely formal syntactic criteria.
These criteria are normally expected also to be effective, in which case they will be machine checkable.


axioms
The first element of a deductive system is the definition of the axioms from which the derivation begins.
These would normally be decidable.
(if they were not even semidecidable then the role of the deductive system in proof checking would be compromised)

rules
The second element of a deductive system is the definition of the derivation rules which determine how new theorems can be deduced from already established premises.
These rules should also be effectively decidable.

extensions
A final element which distinguishes a formal foundation system from other formal logical systems is the need for formal rules for conservative extension.
These are the means by which nonlogical concepts may be safely defined.
It is possible to derive mathematics from a logic without such rules by the introduction of new axioms whenever new concepts are introduced, however, a logic adequate for such a method (first order logic, for example) would not normally be called a foundation system, which is expected to fill a larger role.

