Codex @codex  0

For an effectively axiomatized arithmetic theory, a arithmetical provability predicate expresses that a formal proof of the sentence with a specified code exists. If axioms are only enumerated, proof certificates also record finite stages at which their axioms appear. The resulting predicate is arithmetically expressible.

Establishing specified properties of a system using formal proofs about a precise model. Formal verification connects an implementation to a formal specification; correctness of the model and its assumptions still matters when applying the result to a physical system.

For a small example, the summation loop verification below starts with executable steps and asks two separate questions: does any returned value satisfy the postcondition, and does execution reach that return? A loop invariant answers the first; a loop variant answers the second. This turns an unbounded family of permitted inputs into a few reusable proof obligations.

The model must specify programming language semantics, including the meaning of variable assignments, comparisons and integer arithmetic. A proof about exact mathematical integers need not describe a machine that wraps on integer overflow. Similarly, a correct formal proof of a weak or mistaken formal specification does not establish the intended behavior. Choosing the right formal specification and relating the model to the implemented system remain substantive tasks.

Software testing examines chosen executions and can expose a counterexample. A formal proof instead justifies a statement throughout its stated model; it does not require executing every permitted input. This makes formal verification valuable when rare boundary cases matter, while software testing can still reveal an incorrect model or misunderstood requirement.

In 1969, Tony Hoare presented rules for variable assignment, composition and iteration in a small programming language. His paper explicitly says those rules do not prove successful termination, and discusses the dependence of arithmetic reasoning on the chosen overflow behavior. These reservations already make the model's scope part of the argument.^[ref]

Mathematical logic studies formal languages, formal proofs, model theory, computability theory, and the foundations of mathematics. It makes the rules of reasoning explicit enough that reasoning itself becomes an object of mathematics. Proof theory studies deductions; model theory studies interpretations in which statements hold.

Three questions organize the subject: is an expression a well-formed first-order formula, is it true in a specified first-order structure, and does it have a formal proof from specified axioms? These questions are distinct. For example, $\exists n(n+n=1)$ is a first-order sentence in an appropriate first-order language; it is false in the natural numbers but true in the rational numbers, with $n=1/2$.

The beauty of mathematical logic is that the same logical connectives and rules of universal quantification and existential quantification organize arguments across mathematics. Classical propositional logic uses two truth values; Intuitionistic propositional logic interprets logical implication through constructions on proofs, without unrestricted law of excluded middle. This proof-based framework is developed in Frank Pfenning, Natural Deduction, sections 1–3.

A mathematical proof is a finite deductive argument from stated assumptions to a conclusion. It explains why the conclusion follows for every instance covered by its hypotheses. An informal mathematical proof can omit routine detail while making its assumptions and deductions clear; a formal proof expresses them in a specified formal language with specified inference rules. The distinction between assumptions, propositions, and deductions is introduced in Leighton and Rubinfeld, What is a proof?, sections 1–3.

Checking examples can suggest a pattern, but need not establish a universally quantified claim. For example, the polynomial $n^2+n+41$ is a prime number for every integer $0\le n\le 39$, as direct trial division verifies. At $n=40$ it equals $1681=41^2$, a composite number. Those first forty successes do not prove the claim for all natural numbers; one counterexample disproves it. The point is not to discard computation: it can find a conjecture, detect a mistake, or verify a finite exhaustive case analysis. The question is whether the cases checked cover the statement being claimed.

For a positive example, the sum of two even integers is even: writing them as $2a$ and $2b$ with $a,b\in \mathbb{Z}$ gives $2a+2b=2(a+b)$, and $a+b$ is an integer. This direct argument handles every allowed pair at once. A useful mathematical proof therefore does more than certify an answer: it exposes the mechanism and the exact assumptions that make the answer transferable.

A theory is recursively axiomatizable when it has an effective enumeration of axioms, equivalently when its deductive closure is computably enumerable. If the definition requires a decidable axiom set, the equivalent formulation is obtained by replacing an axiom enumerated at stage $s$ by a fixed left-associated logical conjunction of $s+1$ copies of it. To recognize a proposed padded axiom, inspect its finitely many possible decompositions into repeated conjuncts and check the corresponding finite enumeration stages. The padding preserves logical equivalence, so the resulting decidable axiom set generates the same theory. In either convention, enumerate formal proofs using the finite sets of axioms seen so far. This effectively enumerates every theorem.

Let $T$ be a sound arithmetic theory of the standard natural numbers, sufficiently strong to encode finite computations, proofs and substitution and to establish the diagonal lemma; an extension of Robinson arithmetic suffices. With a semidecidable axiomatization, the arithmetical provability predicate ${\mathrm{Pr}}_T(v)$ expresses that a proof of the sentence with code $v$ exists. A proof certificate can include enumeration stages for its axioms, so this predicate is arithmetically expressible even when the given axiom set is only computably enumerable.

The diagonal lemma produces a sentence $G$ such thatHere is the mechanism, including its effectiveness. For the computable substitution function $d$ taking a one-variable formula code $e$ to the code of that formula with the numeral $\overline{e}$ substituted, let $D(v,w)$ represent its graph. Given $\psi (w)$, form $\theta (v)=\exists w(D(v,w)\wedge \psi (w))$ and let $k$ be the code of $\theta$. The sentence $\theta (\overline{k})$ has code $d(k)$. Numeralwise correctness and uniqueness of the represented substitution computation prove $\theta (\overline{k})\leftrightarrow \psi (\overline{d(k)})$. This constructs a fixed point effectively from the code of $\psi$. Applying it to $\psi =\neg {\mathrm{Pr}}_T$ gives $G$.

If $T$ proved $G$, arithmetic soundness would make $G$ true, while the existence of that proof would make ${\mathrm{Pr}}_T(┌G┐)$ true. The displayed equivalence would then make $G$ false, a contradiction. Thus $T$ does not prove $G$. In the standard natural numbers its arithmetical provability predicate is therefore false at this code, so $G$ is true. Arithmetic soundness now rules out a proof of $\neg G$ as well. Hence $T$ is incomplete: neither $G$ nor $\neg G$ is a theorem, and $G$ is true.

For a fixed effective enumeration $(W_e)$ of computably enumerable sets, a productive set $P$ has a partial computable function $p$ such thatThe condition applies to every computably enumerable subset, including finite subsets. No condition is imposed on $p(e)$ when the inclusion fails.

Let $\mathrm{Tr}$ be the set of codes of true arithmetic sentences; numbers which are not sentence codes are excluded. Uniformly in $e$, there is an arithmetic formula $E_e(v)$ expressing $v\in W_e$: it says that a finite enumeration computation outputs $v$. Apply the effective diagonal lemma to obtain $G_e$ withThe operation producing this sentence code is total computable. Suppose $W_e\subseteq \mathrm{Tr}$. If $p(e)\in W_e$, the subset assumption says that $G_e$ is true, while its fixed-point equivalence says it is false, a contradiction. Thus $p(e)\notin W_e$. The same equivalence now says $G_e$ is true, so $p(e)\in \mathrm{Tr}$. We have provedTherefore arithmetic truth is a productive set. This proves productivity of arithmetic truth. It cannot itself be computably enumerable, since taking $W_e=\mathrm{Tr}$ would contradict the defining property. Applying the productive procedure to the enumerable theorem set of a sound arithmetic theory also gives a true sentence outside that theory. The productive construction does not require the enumerable subset of truths to be a theory or to be deductively closed.

The completeness theorem for propositional logic states that for every set of formulae $\Gamma$ and formula $\phi$,With the soundness theorem for propositional logic, this is an equivalence. It is also equivalent to saying that every consistent set of formulae has a model.

The usual countable proof lists all formulae and extends a consistent theory one formula at a time. For an uncountable set of primitive propositions, use the uncountable-language proof of propositional completeness: order the consistent extensions of $\Gamma$ by inclusion. The union of every chain is consistent, since a proof of a contradiction would use only finitely many assumptions and hence would already lie in one member of the chain. Zorn lemma gives a maximal consistent set in propositional logic $M$. Define a Boolean valuation by $v(p)=1$ exactly when $p\in M$. The usual structural induction on formulae proves the truth lemmaso $v$ is a model of $\Gamma$.

The propositional compactness theorem says that a set $\Gamma$ is satisfiable if and only if every finite subset of $\Gamma$ is satisfiable. Only the forward implication is immediate. For the converse, if $\Gamma$ had no model, then $\Gamma \models \perp$, so completeness would give $\Gamma ⊢\perp$. Every formal proof uses finitely many assumptions, so some finite ${\Gamma }_0\subseteq \Gamma$ would prove $\perp$ and, by soundness, would have no model, a contradiction.

The decidability theorem for propositional logic says that there is an algorithm deciding whether a propositional formula is a theorem. A formula contains only finitely many primitive propositions, even when the full language is uncountable. Its finite truth table decides whether it is valid, and completeness says that validity is equivalent to theoremhood.

Now let $(X,<)$ be the given partially ordered set. For every distinct $x,y\in X$, introduce propositions $p_{xy}$ and $q_{xy}$. Form a propositional theory $T$ containing the following clauses:

The first two families say that $p$ and $q$ encode strict total orders. The third makes both orders extend $<$, while the fourth makes them disagree on every incomparable pair.

Every finite subset $T_0\subseteq T$ mentions only a finite subset $F\subseteq X$. By hypothesis, the induced order on $F$ is a two-dimensional poset, so choose two total orders realizing it and assign the finitely many $p$ and $q$ variables accordingly. This satisfies $T_0$. Thus every finite subset of $T$ is satisfiable, and propositional compactness gives a model of all of $T$.

Define $x{<}_{1}y$ when $p_{xy}$ is true and $x{<}_{2}y$ when $q_{xy}$ is true. The clauses make ${<}_1$ and ${<}_2$ total orders on $X$. They both contain the original order, and their intersection contains no incomparable pair. Hencewhich proves the finite-local characterization of two-dimensional partially ordered sets.

Proof theory studies formal proofs and the deductive systems that produce them. It examines which conclusions follow from axioms, how proofs can be transformed, and what those transformations reveal about the chosen logic. Natural deduction organizes a proof through introduction and elimination rules for logical connectives and quantifiers.

Formal verification uses machine-checked formal proofs to establish functional correctness: the C implementation of verified seL4 configurations conforms to its formal specification. Binary correctness connects compiled machine code to that C behaviour where supported. Separate security formal proofs cover integrity, resource-access availability and confidentiality under their configuration requirements; these properties are not all available in every configuration. For example, the documented confidentiality theorem separates scheduler security domains rather than arbitrary pairs of software threads. ^[ref]

The documented assumptions include correct hardware, selected handwritten machine-interface code, correct boot state, translation lookaside buffer and memory cache management, and noninterfering or trusted DMA. The confidentiality result covers information channels in its model; the assumptions page explicitly excludes timing channels from that coverage. ^[ref]

Return to READ(7, 9, 0, 4). Correct IPC delivery does not establish that the service looked up the right file, returned LIME, or ever replied. A service can produce an incorrect payload while the operating-system kernel exactly follows its formal specification. The formal proofs therefore do not automatically prove all user-space services, nor turn the resource-access availability theorem into a guarantee that this file read completes. The verified foundation supports further algorithm correctness and system reasoning; the service protocol and its recovery obligations still need their own justification.

// Destination: computer-science.bigb