Propositional Logic, First-Order Logic, and Higher-Order Logics - MathOverflow

Propositional Logic, First-Order Logic, and Higher-Order Logics

2010-02-21T01:01:37Z

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.

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

Answer by François G. Dorais for Propositional Logic, First-Order Logic, and Higher-Order Logics

2010-02-21T02:14:01Z

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.

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.
The real difference between propositional and first-order logic is quantification. Quantifiers are naturally more expressive than logical connectives.
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 ℘(Aⁿ). 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 Aⁿ→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.
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.

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.
You may want to read on categorical logic.

Answer by Haim for Propositional Logic, First-Order Logic, and Higher-Order Logics

2010-02-21T16:32:22Z

" What are the advantages/disadvantages of using lower/higher-order formal logics?"

It seems that "strong" logics are not as well-behaved as first order logic. By Lindstrom's theorem, FOL is the strongest logic that satisfies both the Lowenheim-Skolm theorem down to Aleph0 and the compactness theorem (we say that a logic L1 is stronger than L2 when every elementary class of a theory of L2 is also en elementary class for a theory of L1). As the compactness property and the LS property are crucial for many important constructions in model theory, it seems that it's much harder to develop model theory for stronger logics.

Answer by none for Propositional Logic, First-Order Logic, and Higher-Order Logics

2010-12-02T08:14:52Z

The Wikipedia articles on first- and second-order logic are quite good. The second-order logic article iirc cites a paper by Väänänen which is also informative: http://www.math.ucla.edu/~asl/bsl/0704/0704-003.ps

Answer by Mark Adams for Propositional Logic, First-Order Logic, and Higher-Order Logics

2011-01-29T08:43:11Z

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