A hypothetical refutation selects one finite target fragment

The five-line derivation is: line 0, A; line 1, not-A; line 2, the logical tautology $A\to (\mathrm{\neg }A\to \mathrm{\perp })$; line 3, $\mathrm{\neg }A\to \mathrm{\perp }$ by MP at 0,2; line 4, bottom by MP at 1,3. Its two nonlogical axiom lines give exactly $\mathrm{\Delta }=\{A,\mathrm{\neg }A\}$. The set of support lines has size 2, while the proof has length 5. Adding or repeating unrelated U axioms does not alter these premise references.

For this Delta the hypotheses of F1 would give a finite source fragment Gamma, a T proof of its suitable source-model existence, and a T proof converting that model into a model of Delta. But any Delta model satisfies both A and not-A, impossible, so appending the formal soundness proof of the displayed five-line derivation compiles a T-refutation. For a general proof with k axiom lines, taking their set gives at most k distinct axioms, and the same assembly depends only on that set.

To make this a B proof of a Con implication via F2, verify in B each arrow: extracting Delta from p, computing Gamma, generating its existence proof, generating the transfer proof, and appending the soundness/refutation block. A fixed finite assembly in step 2.1 does not by itself verify those maps uniformly. In the concrete proof, the extractor merely reads lines 0 and 1; its output contains neither the tautology nor the MP lines.