4 inserted missing words
1. Yes there are advantages/disadvantages in where the balance lies between the number of inference rules and the number of axioms when defining a logic. As Francois Dorais says in his answer, it depends on what you want to do with the logic.

2. All logics are for representing proofs, including propositional logic. The higher the order of the logic, the more powerful it is in the sense of its language being more expressive and its deduction being more general.

3. The criterion that determines the order of a logic relates to the kinds of value that can be quantified over. In a zeroth-order logic, there are just values and quantification is not supported (e.g. propositional logic, where the values are boolean values). In a first-order logic, there are functions which are distinct from values; only values can be quantified over (e.g. first-order predicate logic, natural number arithmetic). In a second-order logic, functions may take first-order functions as arguments, and first-order functions may be quantified over. In a third-order logic, second-order functions may themselves be arguments to functions and be quantified over, etc, etc. In a higher-order logic (this is a distinct concept from the concept of an nth-order logic), there is no fundamental distinction between functions and values, and all functions can be quantified over.

Note that usage of predicates can be considered as equivalent to usage of sets (some predicate returning "true" for a given value can be considered as equivalent to the value being an element of some set). Note also that a given logic may or may not fundamentally distinguish between general values and boolean values, and between functions and predicates (functions that return a boolean value).

4. Godel's (First) Incompleteness Theorem only relates to logics capable of at least expressing natural number arithmetic - any such logics are incomplete (unless they are inconsistent, in which case they are trivially complete). His Second Incompleteness Theorem relates to whether such logics are capable of proving their own consistency.

The advantage of a less powerful logic is that it is easier to reason about, and that it is tends to be easier to write algorithms for, in the sense that (depending on what the algorithm is intended to do) these algorithms will tend to be more complete and/or efficient and/or to terminate (e.g. algorithms for proving statements in the logic). The advantage of a more powerful logic is that it is more expressive and thus capable of representing and/or proving more of mathematics.

There are certainly higher-order logics that are not capable of expressing the whole of mathematics today (e.g. not capable of fully expressing category theory). I'm afraid I don't know enough to say whether there are/aren't any formal logics that are capable of expressing all of contemporary mathematics.

5. Type theory is the study of type systems. Presumably your question relates to the purpose of using a type system in a formal logic? (Apologies if I got the wrong end of the stick.)

Whether or not a logic uses a type system is another fundamental distinguishing attribute between logics. The alternative is to base the logic on set theory. Either way, the logic must somehow avoid consistency problems, like Russell's Paradox that exposed the inconsistency of Frege's formal logic, or the Kleene-Rosser Paradox that exposed the inconsistency of Church's original lambda calculus.

The purpose of a type system is to impose extra well-formedness restrictions on a formal language in addition to the restrictions imposed by the language's syntax. This is a way of ensuring that paradoxes can be avoided, as well as a practical way of helping the user of a logic avoid writing meaningless statements (such as "the number 5 is a vector space"). Russell actually invented type theory to solve the problem raised by his own paradox. Church used type theory to come up with an alternative, consistent lambda calculus.

3 filled in missing word
1. Yes there are advantages/disadvantages in where the balance lies between the number of inference rules and the number of axioms when defining a logic. As Francois Dorais says in his answer, it depends on what you want to do with the logic.

2. All logics are for representing proofs, including propositional logic. The higher the order of the logic, the more powerful it is in the sense of its language being more expressive and its deduction being more general.

3. The criterion that determines the order of a logic relates to the kinds of value that can be quantified over. In a zeroth-order logic, there are just values and quantification is not supported (e.g. propositional logic, where the values are boolean values). In a first-order logic, there are functions which are distinct from values; only values can be quantified over (e.g. first-order predicate logic, natural number arithmetic). In a second-order logic, functions may take first-order functions as arguments, and first-order functions may be quantified over. In a third-order logic, second-order functions may themselves be arguments to functions and be quantified over, etc, etc. In a higher-order logic (this is a distinct concept from the concept of an nth-order logic), there is no fundamental distinction between functions and values, and all functions can be quantified over.

Note that usage of predicates can be considered as equivalent to usage of sets (some predicate returning "true" for a given value can be considered as equivalent to the value being an element of some set). Note also that a given logic may or may not fundamentally distinguish between values and boolean values, and between functions and predicates (functions that return a boolean value).

4. Godel's (First) Incompleteness Theorem only relates to logics capable of at least expressing natural number arithmetic - any such logics are incomplete (unless they are inconsistent, in which case they are trivially complete). His Second Incompleteness Theorem relates to whether such logics are capable of proving their own consistency.

The advantage of a less powerful logic is that it is easier to reason about, and that it is tends to be easier to write algorithms for, in the sense that (depending on what the algorithm is intended to do) these algorithms will tend to be more complete and/or efficient and/or to terminate (e.g. algorithms for proving statements in the logic). The advantage of a more powerful logic is that it is more expressive and thus capable of representing and/or proving more of mathematics.

There are certainly higher-order logics that are not capable of expressing the whole of mathematics today (e.g. not capable of fully expressing category theory). I'm afraid I don't know enough to say whether there are/aren't any formal logics that are capable of expressing all of contemporary mathematics.

5. Type theory is the study of type systems. Presumably your question relates to the purpose of using a type system in a formal logic? (Apologies if I got the wrong end of the stick.)

Whether or not a logic uses a type system is another fundamental distinguishing attribute between logics. The alternative is to base the logic on set theory. Either way, the logic must somehow avoid consistency problems, like Russell's Paradox that exposed the inconsistency of Frege's formal logic, or the Kleene-Rosser Paradox that exposed the inconsistency of Church's original lambda calculus.

The purpose of a type system is to impose extra well-formedness restrictions on a formal language in addition to the restrictions imposed the language's syntax. This is a way of ensuring that paradoxes can be avoided, as well as a practical way of helping the user of a logic avoid writing meaningless statements (such as "the number 5 is a vector space"). Russell actually invented type theory to solve the problem raised by his own paradox. Church used type theory to come up with an alternative, consistent lambda calculus.

2 corrected grammatic error
1. Yes there are advantages/disadvantages in where the balance lies between the number of inference rules and the number of axioms when defining a logic. As Francois Dorais says in his answer, it depends on what you want to do with the logic.

2. All logics are for representing proofs, including propositional logic. The higher the order of the logic, the more powerful it is in the sense of its language being more expressive and its deduction being more general.

3. The criterion that determines the order of a logic relates to the kinds of value that can be quantified over. In a zeroth-order logic, there are just values and quantification is not supported (e.g. propositional logic, where the values are boolean values). In a first-order logic, there are functions which are distinct from values; only values can be quantified over (e.g. first-order predicate logic, natural number arithmetic). In a second-order logic, functions may take first-order functions as arguments, and first-order functions may be quantified over. In a third-order logic, second-order functions may themselves be arguments to functions and be quantified over, etc, etc. In a higher-order (this is a distinct concept from the concept of an nth-order logic), there is no fundamental distinction between functions and values, and all functions can be quantified over.

Note that usage of predicates can be considered as equivalent to usage of sets (some predicate returning "true" for a given value can be considered as equivalent to the value being an element of some set). Note also that a given logic may or may not fundamentally distinguish between values and boolean values, and between functions and predicates (functions that return a boolean value).

4. Godel's (First) Incompleteness Theorem only relates to logics capable of at least expressing natural number arithmetic - any such logics are incomplete (unless they are inconsistent, in which case they are trivially complete). His Second Incompleteness Theorem relates to whether such logics are capable of proving their own consistency.

The advantage of a less powerful logic is that it is easier to reason about, and that it is tends to be easier to write algorithms for, in the sense that (depending on what the algorithm is intended to do) these algorithms will tend to be more complete and/or efficient and/or to terminate (e.g. algorithms for proving statements in the logic). The advantage of a more powerful logic is that it is more expressive and thus capable of representing and/or proving more of mathematics.

There are certainly higher-order logics that are not capable of expressing the whole of mathematics today (e.g. not capable of fully expressing category theory). I'm afraid I don't know enough to say whether there are/aren't any formal logics that are capable of expressing all of contemporary mathematics.

5. Type theory is the study of type systems. Presumably your question relates to the purpose of using a type system in a formal logic? (Apologies if I got the wrong end of the stick.)

Whether or not a logic uses a type system is another fundamental distinguishing attribute between logics. The alternative is to base the logic on set theory. Either way, the logic must somehow avoid consistency problems, like Russell's Paradox that exposed the inconsistency of Frege's formal logic, or the Kleene-Rosser Paradox that exposed the inconsistency of Church's original lambda calculus.

The purpose of a type system is to impose extra well-formedness restrictions on a formal language in addition to the restrictions imposed the language's syntax. This is a way of ensuring that paradoxes can be avoided, as well as a practical way of helping the user of a logic avoid writing meaningless statements (such as "the number 5 is a vector space"). Russell actually invented type theory to solve the problem raised by his own paradox. Church used type theory to come up with an alternative, consistent lambda calculus.

1