I've been reading up a bit on the fundamentals of formal logic, and have accumulated a few questions along the way. I am pretty much a complete beginner to the field, so I would very much appreciate if anyone could clarify some of these points.


1. A complete (and consitent) propositional logic can be defined in a number of ways, as I understand, which are all equivalent. I have heard it can be defined with one axiom and multiple rules of inferences or multiple axioms and a single rule of inference (e.g. Modus Ponens) - or somewhere inbetween. Are there any advantage/disvantages to either? Which is more conventional?
2. Propositional (zeroth-order) logic is simply capable of making and verifying logical statements. First-order (and higher order) logics can represent proofs (or increasing hierarchial complexity) - true/false, and why?
3. What exactly is the relationship between an nth-order logic and an (n+1)th-order logic, in general. An explanation mathematical notation would be desirable here, as long as it's not *too* advanced.
4. Any formal logic above (or perhaps including?) first-order is sufficiently powerful to be rendered inconsistent or incomplete by Godel's Incompleteness Theorem - true/false? What are the advantages/disadvantages of using lower/higher-order formal logics? Is there a lower bound on the order of logic required to prove all known mathematics today, or would you in theory have to use an arbitrarily high-order logic?
5. What is the role type theory plays in formal logic? Is it simply a way of describing nth-order logic in a consolidated theory (but orthogonal to formal logic itself), or is it some generalisation of formal logic that explains everything by itself?


Hopefully I've phrased these questions in some vaguely meaningful/understandable way, but apologies if not! If anyone could provide me with some details on the various points without assuming too much prior knowledge of the fields, that would be great. (I am an undergraduate Physics student, with a background largely in mathematical methods and the fundamentals of mathematical analysis, if that helps.)



Propositional Logic, First-Order Logic, and Higher-Order Logics
This is a long list of questions! These are all related to a certain extent, but you might consider breaking it up into separate questions next time.


1. Proof theorists tend to prefer systems with many rules and few axioms such as natural deduction systems and Gentzen systems. The reason is that these are much easier to manipulate and visualize. (Look at the statement and proof of the Cut Elimination Theorem for an illustrative example.) Model theorists tend to prefer lots of axioms and just modus ponens, like Hilbert systems. The reason is that the semantics of such systems are easy to handle, and semantics is what model theorists really care about.
2. The real difference between propositional and first-order logic is quantification. Quantifiers are naturally more expressive than logical connectives.
3. There are many, many flavors of higher-order logic. The two main classifications are set-based systems and function-based systems. There are variants which don't really fit this division and there are variants which mix both. With strong enough internal combinatorics, these are all equivalent.


The set-based system have a set A of type 0 objects, which are considered atomic. Type 1 objects are elements of the powersets ℘(An). When the base theory has an internal pairing function (like arithmetic and set theory), the exponent n can be dropped. Then, type 2 objects are elements of the second powerset ℘(℘(A)), and similarly for higher types. Set-based higher types are somewhat inconvenient without an internal pairing function.


Function-based systems are similar, with functions An→A as type 1. Again, with an internal pairing function, the higher types streamline to A → A, (A → A) → A, ((A → A) → A) → A, etc. However, it is common to use more complex types in these systems.
4. Be careful how you read Gödel's Incompleteness Theorem. For first-order logic, the hypotheses state that the theory in question must be recusively enumerable and that it must be powerful enough to interpret a reasonable amount of arithmetic. Those are important hypotheses. (And they explain why no such theorem exists for propositional logic.) There are many variants for higher-order systems, but you need to be even more careful when stating them. 


You can appreciate the difference between the different levels of higher-order logic by reading about [Gödel's Speed-Up Theorems](http://plato.stanford.edu/entries/goedel/#SpeUpThe).


Most of mathematics today is based on set theory, at least in a theoretical sense. In set theory, higher types are interpreted internally using powersets and sets of functions. They also extend transfinitely and this transfinite hierarchy of higher types was shown necessary to prove theorems very low in the hierarchy, such as [Martin's Borel Determinacy Theorem](http://en.wikipedia.org/wiki/Borel_determinacy_theorem).
5. You may want to read on [categorical logic](http://en.wikipedia.org/wiki/Categorical_logic).


