Formal proofs from sentence theories

Fix a set signature $L$ and a set $T$ of $L$-sentences, as in Theories, models and semantic consequence. Use exactly the finite syntax of Terms and formulas as finite set codes: negation, conjunction and existential quantification are primitive. In particular, $\mathrm{\forall }x\varphi$ abbreviates $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }\varphi$ and $\varphi \to \psi$ abbreviates $\mathrm{\neg }(\varphi \wedge \mathrm{\neg }\psi )$. Equality below between displayed formulas means equality after expansion of these abbreviations, not equivalence under first-order semantics.

The logical axioms are all instances of the following schemes. Terms are arbitrary $L$-terms and formulas may have free variables. Substitution and the free-for condition are those of Free variables and free-for substitution.

1. Every propositional tautology instance: substitute formulas for the letters of a finite Boolean expression whose value is true for every Boolean valuation. Expand Boolean abbreviations first. A quantified subformula may be substituted as a whole; first-order validity is not the definition of a tautology here.
2. $\mathrm{\forall }x\varphi \to \varphi [t\mathrm{/}x]$, when $t$ is free for $x$ in $\varphi$.
3. $\mathrm{\forall }x(\varphi \to \psi )\to (\varphi \to \mathrm{\forall }x\psi )$, when $x\mathrm{\notin }\mathrm{FV}(\varphi )$.
4. $\varphi [t\mathrm{/}x]\to \mathrm{\exists }x\varphi$, when $t$ is free for $x$ in $\varphi$.
5. $t=t$.
6. $s=t\to (\varphi [s\mathrm{/}x]\to \varphi [t\mathrm{/}x])$, when both $s$ and $t$ are free for $x$ in $\varphi$.

There are exactly three inference rules:

• Modus ponens: from $\varphi$ and $\varphi \to \psi$, infer $\psi$.
• Universal generalization: from $\varphi$, infer $\mathrm{\forall }x\varphi$.
• Restricted existential elimination: from $\varphi \to \psi$, infer $\mathrm{\exists }x\varphi \to \psi$, provided $x\mathrm{\notin }\mathrm{FV}(\psi )$.

A formal derivation from $T$ is a nonempty finite list of formulas, with each line annotated as an assumption in $T$, a displayed axiom instance, or an application of one of these rules to specified earlier line indices. Rule parameters and substitution data are part of the finite annotation. Write $T⊢\theta$ when such a derivation ends with $\theta$, and $⊢\theta$ when $T=\mathrm{\varnothing }$. All formulas, finite annotations and finite lists range over sets; imposing the displayed line conditions therefore specifies a set of proof codes, without a choice principle.

The premise that $T$ consists of sentences matters. For the same formal line rules applied to additional open assumptions, semantic soundness and discharge require restrictions: a generalized or existentially eliminated variable must not occur free in the undischarged assumptions on which that line depends. The sentence deduction theorem automatically satisfies this restriction; an open-assumption deduction theorem must check both rules.

Existential introduction is an axiom scheme, not a consequence silently imported from completeness. Neither replacement inside an existential quantifier nor quantified double-negation equivalence is part of the syntax convention; each must be derived from these rules when used. Soundness, deduction, fresh-constant proof transformations and completeness are separate proof obligations for this specified calculus. Domains are nonempty, as in the structure convention; no model-existence theorem is assumed here.