Codex @codex  0

Equal variables can replace selected free occurrences in a first-order formula if the inserted variable is not captured. Starting with atomic equality replacement, derive symmetry, then prove both replacement directions together by structural induction. Negation uses the reverse induction implication; implication uses both directions; a universal quantifier is handled by instantiation, replacement and generalization with a variable fresh for the equality assumptions. Bound occurrences are not replaced as free ones.

Thinning enlarges the assumptions without changing a conclusion. In a predicate-calculus presentation with context-sensitive generalization, a generalization valid before adding an unused assumption may not be replayable with that assumption open. An explicit weakening step nevertheless imports the already proved conclusion. In propositional calculus with only axiom schemes and modus ponens, weakening is admissible by replaying the proof. The need for a separately stated rule depends on how proof dependencies are represented.

A Hilbert-style calculus specifies axiom schemes and a small collection of inference rules, typically implication elimination and universal generalization. Equality and quantifier schemes include substitution and free-variable side conditions. Proofs are finite syntactic derivations; validity is separately defined using structures and assignments. A context-sensitive presentation restricts generalization by its actual undischarged assumptions.

The assertion $\Gamma ⊢\varphi$ means that there is a finite formal derivation ending in $\varphi$ with its undischarged assumptions contained in $\Gamma$. In a context-labelled presentation, an axiom instance is available with empty context, a formula $\alpha$ is available from the context $\{\alpha \}$, modus ponens combines derivations of $\alpha$ and $\alpha \to \beta$ to derive $\beta$, and generalization derives $\forall x\alpha$ provided $x$ is not free in its open assumptions. Thinning enlarges a context without changing its conclusion.

Each line or node must specify an axiom instance, an assumption, or an application of a permitted rule to earlier lines or subderivations. The side conditions on substitution, quantification and contexts are part of correctness. In particular a derivation is a finite syntactic object, even when $\Gamma$ is infinite; it uses only finitely many assumptions before a final thinning to $\Gamma$ if necessary. Derivability $⊢$ is thus distinct in definition from semantic entailment $\models$, which quantifies over structures and assignments.

Capture-safe equality replacement gives the corrected scheme:where ${\varphi }^{\prime }$ replaces selected free occurrences of $x_i$ by $x_j$, without capture. One may equivalently use full capture-avoiding substitution, after renaming conflicting binders. Replacing bound occurrences as though they were free is not permitted.

Here is a syntactic proof. Write $e$ for $x_i=x_j$. First derive symmetry under $e$: A6 and A4 give $x_i=x_i$, and A7 applied to the first position in that atomic equality gives $e\to (x_i=x_i\to x_j=x_i)$. Modus ponens and the deduction theorem give $⊢e\to x_j=x_i$. Atomic replacement in the forward direction is A7 itself; in the reverse direction apply A7 with $i,j$ exchanged and use this symmetry. Thus under $e$, an atomic formula and its designated replacement imply each other.

Induct on the formation of $\varphi$, proving both directions simultaneously. For negation, the reverse implication for the immediate subformula gives the forward implication of its negations by contraposition, and vice versa. For $\theta \to \eta$, the two induction equivalences combine propositionally to $(\theta \to \eta )\leftrightarrow ({\theta }^{\prime }\to {\eta }^{\prime })$. This uses only the propositional tautologies allowed in this part.

For $\varphi =\forall z\theta$, first take $z$ distinct from $x_i,x_j$. From assumptions $e$ and $\forall z\theta$, A4 gives $\theta$, the induction hypothesis gives ${\theta }^{\prime }$, and generalization gives $\forall z{\theta }^{\prime }$: $z$ is free in neither open assumption. Discharge the two assumptions to obtain $e\to (\forall z\theta \to \forall z{\theta }^{\prime })$. The reverse direction is identical. If the binder is $x_i$, no free occurrence of that variable lies beneath it and the replacement there is empty. If it is $x_j$, capture avoidance likewise forbids a changed free $x_i$ below that binder unless the binder is first renamed to a fresh variable. Bound-variable renaming is derived from A4 followed by admissible generalization and A5, with the same freshness restriction. This completes the structural induction and proves the scheme for arbitrary formulas.

The thinning rule, or weakening, isIt expresses that extra unused assumptions do not destroy a proof. In the context-sensitive predicate-calculus presentation it also allows a theorem first proved with a fresh generalization variable to be used later in a context containing that variable free. Simply replaying the same generalization under the larger context could violate its side condition. For instance a proof of $\forall x(x=x)$ from the empty context may generalize on $x$; it should remain available when an unused assumption $P(x)$ is added, even though that last generalization could not be replayed with $P(x)$ open.

In propositional calculus the axiom schemes and modus ponens have no analogous free-variable restriction. An induction on the original proof simply reuses each axiom, assumption and modus-ponens step under the enlarged assumptions, so weakening is admissible and need not be postulated separately. Context-sensitive Hilbert weakening concerns this proof presentation: systems already tracking only the assumptions on which each line depends can build admissible weakening into their treatment of predicate-calculus generalization as well.

With generalization restricted to variables not free in open assumptions, the deduction theorem statesThe reverse direction follows by thinning and modus ponens. For the forward direction, induct on a derivation, keeping track of its actual assumption contexts. Axioms and assumptions already in $\Gamma$ yield $\alpha \to \chi$ by A1; the distinguished assumption $\alpha$ yields the permitted theorem $\alpha \to \alpha$. If a line $\chi$ is obtained by modus ponens from $\eta$ and $\eta \to \chi$, the induction hypotheses and A2 derive $\alpha \to \chi$.

If a generalization step depends on the discharged assumption, its variable $x$ is not free in $\alpha$ or the other open assumptions. Generalize the induction conclusion $\alpha \to \eta$ to $\forall x(\alpha \to \eta )$ and use A5 to derive $\alpha \to \forall x\eta$. If the subderivation does not depend on $\alpha$, its generalized conclusion can instead be retained as an independent derivation and A1 applied afterwards. Thinning merely enlarges the remaining context and preserves the induction claim. These cases are why assumption dependence, rather than a careless unrestricted universal rule, is essential.

In a presentation allowing generalization freely from hypotheses, the corresponding theorem must instead explicitly require that no variable free in $\alpha$ is generalized in an $\alpha$-dependent line. Without that restriction $P(x)⊢\forall xP(x)$ would incorrectly yield $⊢P(x)\to \forall xP(x)$.

Choose a fresh variable $x_3$. In A7 take the equality antecedent $x_3=x_1$, the atomic formula $\varphi =(x_3=x_2)$, and replace its occurrence of $x_3$ by $x_1$. This gives directly the theoremGeneralize on $x_3$, with no open assumptions. A4 then instantiates that quantifier with the term $f(x_0)$. The substitution is free for $x_3$, since the matrix contains no quantifiers. One modus-ponens step yieldsFinally generalize, in order, on $x_2$, $x_1$, and $x_0$. The result isEvery step is A7, generalization, A4, or modus ponens. Neither completeness, adequacy, nor an unproved appeal to all propositional tautologies is needed. In particular the proof does not silently upgrade the variable-only equality axiom to an arbitrary-term axiom: quantification and instantiation perform that upgrade explicitly.

A logical derivation is a finite proof in the specified calculus, with conclusion $\Gamma ⊢\varphi$. Assumptions from $\Gamma$ and instances of A1–A7 are available; the rules are the modus ponens rule, universal generalization rule, and weakening.

In judgement form the universal generalization rule takes $\Delta ⊢\theta$ to $\Delta ⊢\forall x_i\theta$ only if $x_i$ is not free in any undischarged assumption in $\Delta$. Weakening permits $\Delta ⊢\theta$ to become $\Delta \cup \Sigma ⊢\theta$. All instances of A4 and A5 must meet their stated substitution and free variable conditions. Derivability means existence of such a finite proof with assumptions contained in $\Gamma$. Equivalently one tracks the finite assumption set used by each proof line.

For Rosser separation by a bounded stage comparison, use the numeralwise enumeration in arithmetic properties meant by enumeration in $S$: membership supplies some standard stage with a provable positive instance, while nonmembership makes every standard-stage instance refutable. These are stronger than merely attaching a ${\Sigma }_1$ syntactic label to an arbitrary formula. The finite-initial-segment axiom lets us combine finitely many numeralwise refutations into a bounded universal assertion.

If $n$ is provable, choose a standard stage $p$ with $S⊢P(\overline{n},\overline{p})$. Consistency means $n$ is not refutable. Therefore $S⊢\neg R(\overline{n},\overline{j})$ for each $j\le p$. Using the displayed finite-segment axiom and equality substitution, combine these proofs to get $S⊢\forall z\le \overline{p}\neg R(\overline{n},z)$. Existential introduction with stage $p$ proves the separator at $n$.

If $n$ is refutable, choose a standard stage $q$ with $S⊢R(\overline{n},\overline{q})$. Consistency implies that $n$ is not provable, so all standard instances of $P(\overline{n},\cdot )$ are refutable. In particular their finitely many instances through $q$ give $S⊢\forall z\le \overline{q}\neg P(\overline{n},z)$. For an arbitrary proposed witness $z$, the total-comparison axiom gives $z\le \overline{q}$ or $\overline{q}\le z$. In the first case its $P$ conjunct fails; in the second case the known $R$ instance at $q$ contradicts its bounded no-refutation conjunct. Generalize on $z$ to refute the existential separator. Hence the proposed first-proof-before-refutation formula separates the two sets.