The first-order term $t$ is free for substitution for $x_i$ in $\varphi$ if, at every free occurrence of $x_i$ to be replaced, no enclosing quantifier binds a variable occurring in $t$. Equivalently, the substitution introduces no variable capture. Only free occurrences of $x_i$ are replaced.

A two-element model of $\varphi$ would be a finite model with even size, contrary to the defining property established in part (b). Every model of $\varphi$ therefore has size other than two, and the preceding interpretation of $\psi$ gives $\boxed{\{\varphi \}\models \psi }$. This includes infinite models, since the antecedent of $\psi$ is false there.

The antecedent says that the nonempty domain has at most two elements: its two witnesses need not be distinct. The consequent says it has exactly one element. ThusOne-element structures satisfy both sides; domains of size at least three, including infinite domains, make the antecedent false. The function $f$ has no bearing on this condition.

Semantic consequence under an assignment means that for every first-order structure $\mathcal{A}$ with the relevant first-order variable assignment $v$ into its domain,More explicitly, in a fixed structure this is the satisfaction implication at $v$; logical consequence requires that implication in all structures and assignments. An assignment takes values in a particular domain, so a single set map is not silently shared between unrelated domains.

By induction on first-order formulas, their truth values depend only on the values of their free variables. A first-order sentence has none. If all formulas here are sentences, every displayed satisfaction statement, and therefore the consequence condition, is independent of $v$.

Extend the first-order variable assignment recursively to first-order terms byFor atomic formulas, $\mathcal{A}\models t=s[v]$ exactly when $\tilde{v}(t)=\tilde{v}(s)$. Extend to the Boolean connectives by their truth tables, for example implication is false exactly when its antecedent is true and its consequent false. Quantifiers use modified first-order variable assignments:This recursion defines satisfaction for a set structure for every first-order formula.

First eliminate implication and biconditional using the logical equivalencesPush negations inwards using De Morgan's laws and eliminate double negations. Structural induction leaves only literals joined by conjunction and disjunction.

Now induct on that remaining expression. A literal is already in conjunctive normal form. A conjunction of two conjunctive normal forms is again one after associating its clauses. For a disjunction, write the two inductively obtained forms as ${\bigwedge }_i{C}_i$ and ${\bigwedge }_j{D}_j$ and use distributivity:Each $C_i\vee D_j$ is a clause. All operations preserve logical equivalence, proving the required form exists.

A conjunctive normal form is a finite conjunction of clauses, each clause being a finite disjunction of literals. A literal is a propositional variable or the negation of one. Thus its shape isA single clause or single literal is allowed; the necessary parentheses can be inserted according to the grammar.

Assign to each propositional formula its finite symbol length. The set of lengths of formulas logically equivalent to $\alpha$ is a nonempty subset of the natural numbers, because it contains the length of $\alpha$. The well-ordering principle for the natural numbers gives a least such length, and hence a shortest equivalent formula.

A shortest equivalent formula need not be unique. For example $(p_0\to p_0)$ and $(p_0\leftrightarrow p_0)$ are distinct tautologies of the same minimal length. A shorter formula would contain no binary connective and hence be a variable with some number of negations, which is not a tautology. This counts each propositional variable as one symbol, as in the stated language, and proves that a shortest equivalent formula need not be unique.

Logical equivalence means that the two propositional formulas receive the same truth value under every Boolean valuation of the propositional variables. Equivalently, $\alpha \leftrightarrow \beta$ is a tautology:

An instance of A3 isThe second assumed theorem and the modus ponens rule therefore give $\Gamma ⊢\beta \to \alpha$. Apply the preceding implication-composition derivation to this theorem and $\Gamma ⊢\neg \alpha \to \beta$. We obtain $\Gamma ⊢\neg \alpha \to \alpha$. The permitted theorem $(\neg \alpha \to \alpha )\to \alpha$ and one more modus ponens rule application yield $\boxed{\Gamma ⊢\alpha }$.

The following is a logical derivation using only A1, A2 and the modus ponens rule. The first two lines are assumptions:Thus $\boxed{\{\alpha \to \beta ,\beta \to \gamma \}⊢\alpha \to \gamma }$.

A theorem is derivable with no assumptions: $⊢\alpha$ abbreviates $\varnothing ⊢\alpha$. Its logical derivation consists entirely of axiom instances and applications of the modus ponens rule to earlier lines.

A logical derivation of $\alpha$ from $\Gamma$ is a finite sequence ${\delta }_1,\dots ,{\delta }_n=\alpha$ in which each line belongs to $\Gamma$, is an instance of one of the three specified axiom schemes, or follows from two earlier lines ${\delta }_j$ and ${\delta }_j\to {\delta }_i$ by the modus ponens rule. $\Gamma ⊢\alpha$ means that such a finite derivation exists. In particular, a derivation uses only finitely many assumptions even if $\Gamma$ is infinite.

The theory is consistent because the rational order is a model. If some sentence $\theta$ were not decided by the theory, both extensions by $\theta$ and by $\neg \theta$ would be consistent. By Gödel's completeness theorem and the countable-model consequence of Löwenheim-Skolem theorem, each would have a countable model. The two models would disagree on $\theta$, so could not be isomorphic. This contradicts part (iii).

Therefore the theory decides every sentence and is complete. Under the standard convention that a theory includes all its logical consequences, this makes it maximal consistent.

If one takes only the displayed finite list of axioms as a raw set, that list is not literally maximal consistent: one can add further theorems without inconsistency. The conclusion applies to its deductive closure, which is the complete theory of dense linear order without endpoints.

Enumerate both countable models. Build an increasing sequence of finite order-preserving partial bijections. At an even stage, take the first unmatched element of the first model. Its position relative to the finitely many already matched points determines an open interval or exterior ray in the second model. Density and absence of endpoints supply an unused point there, so the map extends.

At an odd stage perform the symmetric operation starting from the second model, extending the inverse map. Every required interval has infinitely many points, so avoiding the finitely many used values is possible. The union is a total bijection, by the alternating enumeration requirements, and it preserves and reflects order because every finite stage does. Hence it is an isomorphism of structures.

This is the back-and-forth method, proving countable categoricity of the dense-order theory.