Formal Logic

What it asks

Once inference is treated as structure rather than habit, it can be written down completely: a fixed vocabulary, rules for building sentences, rules for getting from sentences to sentences. That is a formal system, and it can be studied as an object.

The questions then become sharp in a way philosophical questions rarely are. Does every truth expressible in the system have a proof in it? Is there a procedure that decides, for any sentence, whether it follows? Can the system prove that it will never contradict itself? Each of those has an answer, and none of the answers is the one that was expected.

The recurring problems

Completeness and incompleteness. Godel proved in 1929 that first-order logic is complete: everything valid is provable. Two years later he proved that any consistent system strong enough for arithmetic contains truths it cannot prove, and cannot prove its own consistency. Both results are his; they point in opposite directions and both are correct.

Decidability. Some systems have a mechanical procedure that settles every question. First-order logic does not, as Church and Turing showed independently in 1936. That negative result is where computer science begins.

Expressive power against tractability. Every increase in what a system can say costs something in what can be established about it. There is no system that is both strong and fully behaved.

Which system is the right one. Nothing inside a formal system tells you whether it captures real inference. That judgement is made from outside, informally, which is a slightly uncomfortable position for the field to be in.

How it developed

Frege's Begriffsschrift in 1879 supplied quantifiers and variables and made modern logic possible. Peano and Russell developed the notation.

Hilbert then set the programme: prove, using only unquestionable methods, that mathematics is consistent and complete. It was the most ambitious project in the foundations of anything, and Godel ended it in 1931 while Hilbert was still alive.

What followed was not collapse but a new subject. Tarski gave a rigorous account of truth in formal languages. Church and Turing established what is computable, and in doing so invented the theoretical machine everything since runs on. Model theory, proof theory, recursion theory and set theory became branches of mathematics in their own right.

Philosophy kept the parts that bear on philosophical questions: modal logic for necessity, temporal logic for time, deontic logic for obligation, epistemic logic for knowledge.

The positions within it

Classical logic is the default and admits only two truth values. Intuitionism rejects excluded middle and requires proofs to be constructive. Relevance logic rejects the classical result that a contradiction entails everything. Many-valued and fuzzy systems add degrees.

Logicism, formalism and intuitionism are also the three classical positions on the foundations of mathematics, and are covered under Schools.

Where it stands now

Most formal logic now happens in mathematics and computer science. Type theory underlies proof assistants and functional programming; modal logic underlies verification; complexity theory grew directly out of decidability.

What stays in philosophy is the logic of things philosophy cares about, and the standing question of what obliges us to accept any particular system - which is not itself a formal question and never will be.