形式逻辑与计算

形式逻辑将论证的结构与其讨论的主题分离。 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.

语法与演绎 #

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.

语义、模型与量化 #

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.

有效性、真值、可靠性与完备性 #

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.

作为计算模型的图灵机 #

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.

可计算性与不可判定性 #

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.