Return to Answer

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).

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.

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).

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.

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.

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.

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 complete and/or efficient and/or 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.

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.