Gödel's completeness theorem for first-order sentences says that, in a standard sound first-order Hilbert calculus,Equivalently every first-order consistent set of first-order sentences has a first-order model: apply this existence statement to $T\cup \{\neg \sigma \}$ for the consequence formulation.

For the first-order model existence formal proof use a Henkin construction. Enlarge the language by fresh constant symbols and adjoin Henkin witness axiomsFreshness of $c_{\theta }$ preserves first-order consistency. In detail, if a contradiction followed after adjoining one witness axiom, the deduction theorem for first-order logic would yield its negation, from which one obtains both $\exists x\theta (x)$ and $\neg \theta (c_{\theta })$ over the old theory. Since the new constant symbol does not occur in that theory or in $\theta$, replace it by a fresh logical variable and generalize to derive $\forall x\neg \theta (x)$, a contradiction. Finitely many witness additions preserve first-order consistency successively, and unions preserve first-order consistency because formal proofs are finite. Iterate the enlargement so that logical formulas involving newly introduced constant symbols also receive witnesses. Include at least one constant symbol to guarantee closed terms.

Extend the resulting first-order consistent witnessed first-order theory to a maximal consistent set of first-order sentences $H$. In the equality-free case make the domain the set of closed terms. Interpret constant symbols and function symbols by their formal first-order term constructions; interpret an atomic formula byThe truth lemma for a Henkin term model follows by induction on logical formulas with closed terms substituted for their free variables. The logical connective steps use maximal consistency of a first-order theory. In the existential step, membership of $\exists x\theta$ supplies a witness constant and hence a first-order term satisfying $\theta$; conversely a satisfying closed term gives the existential sentence by an inference of the calculus. The term model consequently satisfies $H$ and the original theory. Equality is absent here, so distinct closed terms may remain distinct domain elements without further identifications.

For a standard classical propositional calculus, strong completeness statesTogether with soundness, this identifies semantic consequence with formal derivability. One proves the contrapositive by the maximal consistent set in propositional logic construction. If $\Gamma ⊬\varphi$, the set $\Gamma \cup \{\neg \varphi \}$ is propositionally consistent, by the deduction theorem for propositional logic and classical propositional reasoning. Extend it to a maximal consistent set in propositional logic $M$, deciding each logical formula in turn. At each stage at least one selection of $\theta$ or $\neg \theta$ preserves propositional consistency; a contradiction in the union would use only finitely many assumptions and hence already occur at a stage.

Define a Boolean valuation by $v(p_i)=1$ exactly when $p_i\in M$. Maximal consistency in propositional logic gives $\neg \theta \in M$ exactly when $\theta \notin M$, and $(\theta \to \eta )\in M$ exactly when either $\theta \notin M$ or $\eta \in M$. Structural induction on logical formulas therefore proves the maximal consistent set truth lemma $v(\theta )=1⟺\theta \in M$. Thus $v$ satisfies $\Gamma$ but falsifies $\varphi$, contradicting semantic entailment. The countable language here permits an enumeration of logical formulas; the corresponding general-language argument uses a well-ordering or a principle of maximality in a partially ordered set.

No finite axiomatization exists. Write $\Gamma$ for the axioms just constructed and suppose a finite set $\Delta$ of first-order sentences had exactly the same first-order models. Its logical conjunction $\delta$ is a single first-order sentence, and $\Gamma \models \delta$. By the compactness theorem there is a finite subset ${\Gamma }_0\subseteq \Gamma$ with ${\Gamma }_0\models \delta$: otherwise $\Gamma \cup \{\neg \delta \}$ would be finitely satisfiable and hence satisfiable, a contradiction.

Only finitely many of the integers $n$ in the torsion-free scheme occur in ${\Gamma }_0$. Choose a prime number $p$ larger than all of them. The cyclic group $\mathbb{Z}/p\mathbb{Z}$ satisfies all the group axioms and each of these finitely many conditions from the torsion-free abelian group axiom scheme: multiplication by an integer $1\le n<p$ is invertible modulo $p$, so $nx=0$ implies $x=0$. It consequently satisfies ${\Gamma }_0$, then $\delta$, and therefore $\Delta$.

But its nonzero elements have finite order $p$, so it is not a torsion-free group, contradicting the assumed description of the first-order models of $\Delta$. This establishes the nonfinite axiomatizability of torsion-free abelian groups, ruling out every finite set of defining first-order sentences, not just finite subsets of the particular scheme in part (c).

Use the following group axioms in the given language:Commutativity supplies the other identity and inverse equations. These first-order sentences therefore specify precisely an abelian group with the named identity $0$; an inverse function symbol is unnecessary because inverses are asserted to exist by a quantified formula.

For each positive integer $n$, let $t_n(x)$ be the first-order term recursively defined by $t_1(x)=x$ and $t_{n+1}(x)=t_n(x)+x$. Add the torsion-free abelian group axiom schemeEvery first-order model of these first-order sentences is an abelian group with no nonidentity element of finite order. Conversely every torsion-free abelian group satisfies each of the displayed first-order sentences. This is a countably infinite first-order axiomatization of exactly the required class.

The assertion that $\mathcal{A}$ is a first-order model of $\Gamma$ means that every first-order sentence belonging to $\Gamma$ is true in the first-order structure:Equivalently each first-order sentence is true under every assignment in a first-order structure, since first-order sentences have no free variables. The first-order sentences must all hold in the same interpretation of the language; one cannot select a different first-order structure for each member of $\Gamma$.

An $L$-structure consists of a nonempty domain $A$, an element $c^{\mathcal{A}}\in A$ for each constant symbol, a function $f^{\mathcal{A}}:A^n\to A$ for each $n$-ary function symbol, and a relation $R^{\mathcal{A}}\subseteq A^n$ for each $n$-ary predicate symbol. When equality is part of the logic it is interpreted as actual identity on $A$.

An assignment in a first-order structure is a function $s$ from logical variables to $A$. It induces a term valuation of first-order terms recursively:For an atomic formula, substitute these first-order term values into the interpreted relation, or compare them for equality. Extend satisfaction for a set structure through the truth tables of the logical connectives, and through the quantifier clausesThus the first-order structure and assignment in a first-order structure together determine truth values for all logical formulas. A first-order sentence has no free variables, so its truth does not depend on the assignment in a first-order structure.

Yes, for soundness and completeness of theoremhood. An axiom-only complete propositional calculus is obtained as follows. Declare every propositional tautology, and only such a tautology, to be an axiom; supply no inference rules. A formal proof then consists of a single axiom. Every proved logical formula is valid, giving soundness, and every valid logical formula is already an axiom, giving completeness.

This is not merely an unspecified collection: whether a finite propositional formula is a tautology is decidable by its finite truth table, so the axiom set can be recognized effectively. It is a deliberately uninformative Hilbert proof system, since all the work has been put into axiom recognition. If one instead asked for strong completeness of derivations from arbitrary additional assumptions, a system whose only formal proof lines are axioms or assumptions would not suffice; the affirmative construction here concerns $⊢\varphi$ versus $\models \varphi$.

There is a three-line Hilbert formal proof. Use A1 with $\alpha =\chi$, $\beta =\psi$; then use A3 with $\alpha =\chi$, $\beta =(\psi \to \chi )$:This is a direct logical derivation in the displayed Hilbert proof system. Neither the deduction theorem for propositional logic nor a completeness theorem for propositional logic is needed: the desired logical implication is just the contrapositive, supplied by A3, of the particular A1 instance on line 1.

Under any Boolean valuation there are two possibilities. If $\neg (\psi \to \chi )$ is false, the outer logical implication is true by vacuous truth. If it is true, then $\psi \to \chi$ is false, which forces $\psi$ true and $\chi$ false. In that case $\neg \chi$ is true, so the outer logical implication is again true. These possibilities exhaust the truth values of its antecedent; therefore

Translate logical formulas recursively, leaving propositional variables unchanged and translating negation by applying negation to the translation. For the other two logical connectives setThe first logical implication is false exactly when both original inputs are false; the second displayed logical formula is true exactly when both inputs are true. Hence each clause preserves truth values. Structural induction gives $v(T(\theta ))=v(\theta )$ for every Boolean valuation and every logical formula $\theta$ in the larger language.

By the assumed functional completeness of negation, logical conjunction and logical disjunction, any finite Boolean function has such a logical formula $\theta$. Its translation $T(\theta )$ uses only negation and logical implication and represents the same function. Thus $\{\neg ,\to \}$ is adequate.

A collection of logical connectives is functionally complete, or adequate, if every Boolean function of finitely many propositional variables is represented by a logical formula using only those logical connectives. More explicitly, for every $n\ge 1$ and every $F:\{0,1{\}}^n\to \{0,1\}$ there is a logical formula $\theta (p_1,\dots ,p_n)$ whose truth value under each Boolean valuation is $F(v(p_1),\dots ,v(p_n))$. Constant functions with Boolean values may use an otherwise irrelevant logical variable, for example $p\to p$ for truth and $\neg (p\to p)$ for falsity.

Fix any Boolean valuation $v$. Logical equivalence of $\alpha$ and $\beta$ means $v(\alpha )=v(\beta )$ for this Boolean valuation and every other one. Follow the unique path from the replaced node to the root of the formula syntax tree. At a negation node, equal input truth values have equal negations. At a logical implication node, the unaffected child has the same truth value before and after subformula replacement, while the affected child has the same truth value by induction; the resulting logical implications therefore agree as well.

Induction along that finite path yields $v(\varphi )=v({\varphi }^{\prime })$. Since $v$ was arbitrary,This is the replacement theorem for logical equivalence: the semantics of each logical connective depends only on the truth values of its immediate inputs.

Fix the particular occurrence of $\alpha$ that is being replaced. The subformula analysis above makes it a node of the formula syntax tree of $\varphi$. Proceed by structural induction on the surrounding logical formula.

If this node is the root, the subformula replacement gives $\beta$, already a logical formula. Otherwise, if $\varphi =\neg \psi$, the chosen occurrence lies inside $\psi$. The induction hypothesis gives a logical formula ${\psi }^{\prime }$ after the subformula replacement there, and the whole result is the logical formula $\neg {\psi }^{\prime }$. If $\varphi =(\psi \to \chi )$, a proper chosen occurrence lies in exactly one of the two children. Replacing inside that child gives either $({\psi }^{\prime }\to \chi )$ or $(\psi \to {\chi }^{\prime })$, each a logical formula by the formation rule. A logical variable has no proper subformula, so there is no additional base case.

Therefore replacing the designated subformula occurrence by any logical formula preserves well-formedness. The argument concerns one chosen occurrence; it does not require simultaneous subformula replacement of every occurrence of the same string.

The unique readability theorem says that every propositional formula has exactly one of the following forms: a unique propositional variable; $\neg \psi$ for a unique logical formula $\psi$; or $(\psi \to \chi )$ for a unique ordered pair of logical formulas $(\psi ,\chi )$. These three alternatives are disjoint. Consequently each logical formula has a unique formula syntax tree and a uniquely determined principal logical connective whenever it is not a logical variable.