Finite support, weakening, and composition of derivations

Assign to an assumption line its singleton support, to an axiom the empty support, to an MP line the union of its two preceding supports, and to either quantifier-rule line the support of its one preceding premise. Induction on line number shows each support is finite and that the prefix derives the line from that support: no rule gains assumptions, and all side conditions are unchanged. In particular the last line has finite support.

Enlarging a sentence theory retains every assumption and line annotation. To concatenate proofs, add the length of the first list to every reference in the second. To replace proved sentence assumptions, insert their finite proofs before their uses and redirect each later reference to the new index of its premise. Induction on the old list gives a valid new list. Only finitely many proofs are inserted; a finite family of existing proofs can be selected by finite induction in ZF. Quantifier parameters and their free-variable restrictions are unchanged, and the new base assumptions are sentences.

For a nonempty inclusion-chain, every finite subset of its union lies in one member: choose a member containing each of its finitely many sentences, and repeatedly retain the larger of two comparable members; for the empty finite subset use any one member. A proof of $\mathrm{\perp }$ from the union would thus, by its finite support and weakening, be a proof from a consistent member, which is impossible.

For the empty chain define a syntactic Boolean valuation $V$: every atom has value $1$, negation and conjunction have their Boolean values, and $V(\mathrm{\exists }x\varphi )=V(\varphi )$. Induction on formula construction shows $V(\varphi [t\mathrm{/}x])=V(\varphi )$, since every atomic value is unchanged and substitution commutes with the Boolean constructors and either retains or traverses a quantifier. Consequently $V(\mathrm{\forall }x\varphi )=V(\varphi )$. All six axiom schemes have value $1$: the substitution axioms reduce to $a\to a$, distribution to $(a\to b)\to (a\to b)$, reflexivity to $1$, equality substitution to $1\to (a\to a)$, and Boolean tautologies to true Boolean instances. MP preserves $1$, generalization does not change the value, and existential elimination leaves its premise's value unchanged. But $V(\mathrm{\perp })=0$. Induction on proof length therefore rules out an empty-theory proof of $\mathrm{\perp }$, proving consistency also for the empty union.