Formal Logic and Computation

Formal logic separates the shape of an argument from the subject it discusses. Syntax defines admissible expressions and proofs; semantics assigns interpretations and truth conditions. Relating the two makes it possible to state precisely what a proof system can establish and what a computational model can decide.

Syntax and Deduction #

A formal language starts with an alphabet of symbols and formation rules for well-formed formulas. Propositional logic contains proposition variables and connectives. First-order logic adds variables, function and predicate symbols, equality in common formulations, and quantifiers.

A deductive system adds:

axioms, formulas accepted without derivation or axiom schemas that generate formulas; and
inference rules, mechanical patterns that derive conclusions from premises.

A derivation is a finite sequence or tree in which every formula is an axiom, an assumption, or the result of an inference rule. The notation \(\Gamma \vdash \varphi\) means that formula \(\varphi\) is derivable from the assumptions in \(\Gamma\). The turnstile describes syntax: a proof checker can validate the derivation without deciding what its non-logical symbols mean.

Modus ponens is one inference rule:

text

P -> Q
P
------
Q

A formal system is consistent when it does not derive both a formula and its negation. Consistency is different from completeness and from the truth of the chosen axioms in an intended model.

Semantics, Models, and Quantification #

An interpretation for propositional logic assigns true or false to each atomic proposition. The connectives then determine the truth of compound formulas:

Formula	True When
\(P \land Q\)	Both operands are true
\(P \lor Q\)	At least one operand is true
\(P \rightarrow Q\)	\(P\) is false or \(Q\) is true
\(P \leftrightarrow Q\)	Both operands have the same truth value

First-order semantics requires a nonempty domain and an interpretation of each constant, function, and predicate symbol over that domain. A variable assignment supplies values for free variables. Quantifiers range over the domain:

\(\forall x\, P(x)\) is true when P holds for every domain element;
\(\exists x\, P(x)\) is true when P holds for at least one domain element.

For example, \(\forall x (Human(x) \rightarrow Mortal(x))\) does not assert that any humans exist. Combined with \(\exists x\, Human(x)\), it entails \(\exists x\, Mortal(x)\).

A model of a set of formulas makes all of them true. The notation \(\Gamma \models \varphi\) means that every model of \(\Gamma\) is also a model of \(\varphi\). The double turnstile describes semantic consequence rather than the existence of a derivation.

Validity, Truth, Soundness, and Completeness #

Truth belongs to a formula under an interpretation. Validity belongs to a formula or argument across interpretations:

A formula is logically valid when every interpretation makes it true.
An argument is valid when no interpretation makes all premises true and the conclusion false.
A sound argument is valid and has premises that are true in the intended interpretation.

Consequently, a valid argument can have false premises and a false conclusion. Validity guarantees only that true premises cannot lead to a false conclusion through that argument form.

Proof-system properties connect derivability with semantic consequence:

text

soundness:    if Gamma |- phi, then Gamma |= phi
completeness: if Gamma |= phi, then Gamma |- phi

Soundness says that the rules derive no semantic consequences that are invalid. Completeness says that every semantic consequence expressible in the logic has a derivation. Classical propositional logic and first-order logic have sound and complete proof systems. Gödel’s completeness theorem for first-order logic must not be confused with his incompleteness theorems: sufficiently expressive, consistent, effectively axiomatized theories of arithmetic cannot prove every statement that is true in their intended arithmetic interpretation.

Truth tables decide propositional validity because a formula with finitely many variables has finitely many valuations. First-order validity is not decidable by a corresponding finite table because models can have unbounded domains.

Turing Machines as a Model of Computation #

A deterministic single-tape Turing machine can be specified by:

a finite set of states, including start and halting states;
a finite tape alphabet with a blank symbol;
a tape unbounded in the mathematical model;
a head that reads and writes one cell; and
a transition function mapping the current state and scanned symbol to a new state, symbol, and head movement.

A configuration records the control state, tape contents, and head position. One application of the transition function moves from one configuration to the next. A machine recognizes a language when it accepts exactly that language’s strings; it decides the language when it halts and answers for every input.

Computability and Undecidability #

A function is Turing-computable when a Turing machine produces its result and halts for every input in the function’s domain. Other precise models, including lambda calculus and register machines, compute the same class of functions. The Church-Turing thesis identifies that class with effectively calculable functions. The thesis connects a mathematical model to an informal notion, so it is not a theorem internal to the model.

Countably many machines describe algorithms, but even languages over a finite alphabet form an uncountable set. Thus some languages are not decidable by any machine. The halting problem gives a constructive example: no Turing machine can decide for every encoded machine and input whether that computation will halt. A standard diagonal argument assumes such a decider, constructs a machine that contradicts the decider on its own encoding, and rejects the assumption.

Undecidable does not mean that every instance is impossible to answer. Static analysis, theorem provers, and type systems remain useful because they restrict the language, accept conservative answers, require annotations, or terminate without deciding every semantic property.