Use the axioms for a strict dense linear order without endpoints:The first three give strict linear order; the next gives density; the final two exclude endpoints. Domains are nonempty under the adopted first-order semantics, and these axioms force them to be infinite.

The downward Löwenheim-Skolem theorem says that a structure in a countable language has a countable elementary substructure containing any specified finite or countable set of its elements. More generally the size bound is $\max (|\mathcal{L}|,|C|,{\aleph }_0)$ for a required parameter set $C$. In particular any satisfiable theory in a countable language has a model of size at most countable.

To see the last assertion directly from the completeness construction, add only countably many witness constants in the Henkin construction. There are then countably many finite closed terms, and taking their quotient cannot increase cardinality. The resulting term model is therefore countable. For the elementary-substructure version, perform the witness construction inside the given structure, choosing actual witnesses and closing under the function symbols. The induced substructure is elementary by the Tarski-Vaught test. This is the same witness mechanism as the completeness construction, with the ambient structure supplying the chosen witnesses.

The upward companion states that a theory with an infinite model has models in every sufficiently large infinite cardinal, at least $|\mathcal{L}|+{\aleph }_0$. Add that many pairwise unequal constants, apply compactness, and then the size-bounded construction. The countable consequence is the part needed below.

In the Henkin construction, first extend the consistent sentence set to a complete consistent theory with witnesses in an expanded language containing fresh constants. Its term model has closed terms modulo provable equality as elements:Functions are interpreted by applying their symbols to representative terms, and an atomic predicate holds of term classes exactly when the corresponding atomic sentence belongs to $T$. Equality axioms make these definitions independent of representatives. The Henkin witness property handles the existential step in the truth lemma, so the resulting structure satisfies $T$ and hence the original $\Sigma$.

An arbitrary sentence set need not already have enough closed terms or witnesses. Calling this a term model for $\Sigma$ means a term-model construction of a model satisfying $\Sigma$, usually through that witnessed completion; it does not assert that every arbitrary $\Sigma$ itself already supplies the construction.

Suppose a structure satisfies every sentence of $\Sigma$. By the soundness theorem for first-order logic, every sentence derivable from $\Sigma$ is true in this structure. In particular it cannot derive both a sentence and its negation, because they cannot both be true under the usual semantics.

Therefore $\boxed{\Sigma \text{ satisfiable}⟹\Sigma \text{ consistent}}$. This direction uses soundness alone, without constructing a model from a proof-theoretic assumption.

Order the consistent sets of sentences extending $\Sigma$ by inclusion. This collection is nonempty. The union of a chain is consistent: any derivation of a contradiction uses finitely many assumptions, which all lie in one member of the chain. Zorn's lemma therefore supplies a maximal member, which is a maximal consistent extension of $\Sigma$.

For a countable language one can instead enumerate all sentences and successively add either a sentence or its negation while preserving consistency. At least one choice is consistent, since inconsistency of both extensions, together with the deduction theorem for propositional logic and classical reasoning, would make the previous stage inconsistent. The union of the stages is consistent by finite use of assumptions and decides every sentence, so it is maximal consistent.

The chain proof covers arbitrary set-sized languages; no restriction on the language cardinality was printed here. The later prohibition on choice applies to the cardinal-arithmetic question, not this logic construction.

A set of sentences is satisfiable if some nonempty first-order structure in its language makes every sentence in the set true. Because the formulas are sentences, their truth is independent of the assignment in a first-order structure.

This is a semantic existence condition. Its equivalence with syntactic consistency is the content of the classical Gödel's completeness theorem, together with soundness.

A set of sentences is maximal consistent if it is consistent and no proper extension by further sentences remains consistent. Equivalently it is consistent, deductively closed, and decides every sentence: for each $\theta$, exactly one of $\theta$ and $\neg \theta$ belongs to it.

For example, if $\Sigma ⊢\theta$ but $\theta \notin \Sigma$, adding $\theta$ does not create a new contradiction, contrary to maximality. Thus maximality includes deductive closure, not only having as many independent axioms as possible.

A consistent set of formulae, restricted here to sentences, does not derive a contradiction in the chosen classical deductive system. Equivalently there is no sentence $\theta$ for which both $\Sigma ⊢\theta$ and $\Sigma ⊢\neg \theta$ hold. By explosion, an inconsistent set derives every sentence; a consistent set does not.

This is a syntactic condition about finite derivations, rather than a definition in terms of models.

Only one logical implication of the printed equivalence is justified:The new system's first axiom is an old axiom, its replacement axiom is derivable in the old system by part (iii), modus ponens rule is shared, and its deduction rule is admissible in the old system by the theorem allowed in the source. Induction on a new-system derivation therefore translates it into an old-system derivation with the same assumptions.

The reverse logical implication is false for the displayed systems. Take $\Gamma =\varnothing$ and let $\varphi$ be an instance of the old contraposition axiom, for example with distinct propositional variables in place of $\alpha ,\beta$. It is an old-system theorem, but the matrix countermodel in part (ii) refutes its derivability in the new system. Thus the requested two-way equivalence cannot be concluded from these printed axioms.

The old system does derive the replacement axiom. Here is a syntactic proof using only its axioms, modus ponens rule, and the permitted deduction theorem for propositional logic.

First derive explosion. From $U$ and $\neg U$, the first axiom gives $\neg V\to \neg U$. The old third axiom then gives $U\to V$, and modus ponens rule with $U$ gives any desired $V$.

Next derive the classical reductio rule. Suppose $\Gamma ,\neg B$ derives both $C$ and $\neg C$. Let $T$ be the theorem $B\to B$, obtainable by applying the deduction theorem for propositional logic to the identity derivation from assumption $B$. Explosion under $\Gamma ,\neg B$ gives $\neg T$, so the deduction theorem for propositional logic gives $\Gamma ⊢\neg B\to \neg T$. The old third axiom with $\alpha =T$, $\beta =B$ yields $\Gamma ⊢T\to B$. Since $T$ is a theorem, $\Gamma ⊢B$. Thus a contradiction under $\neg B$ permits deriving $B$ with that temporary assumption discharged.

Now assume $h=\neg \beta \to \alpha$ and $\neg \alpha$, and temporarily also assume $\neg \beta$. Modus ponens rule gives $\alpha$, contradicting $\neg \alpha$. The just-proved reductio rule discharges $\neg \beta$ and gives $\beta$. Finally discharge $\neg \alpha$ and $h$ by the deduction theorem for propositional logic:No propositional completeness theorem is needed in this derivation.

The requested derivation does not follow from the printed axiom set. Use a two-valued matrix interpretation with ordinary material logical implication and designated value $1$, but interpret the unary symbol $\neg$ by the constant function $N(0)=N(1)=0$.

Every instance of the first axiom $\alpha \to (\beta \to \alpha )$ is valid. In the replacement axiom, both $N(\beta )\to \alpha$ and $N(\alpha )\to \beta$ have value $1$, so its whole logical implication is valid as well. Modus ponens rule preserves the designated value. The deduction rule is sound for semantic consequence under this interpretation because logical implication is the ordinary truth-functional logical implication. Induction on derivations, allowing arbitrary sets of assumptions, therefore makes every theorem valid in this matrix.

But the old contraposition axiom has valuewhich is false when $\alpha =1$ and $\beta =0$. ConsequentlyThis is a truth-matrix countermodel for a Hilbert axiom set. A nonstandard interpretation of a primitive symbol is legitimate for proving syntactic nonderivability: only preservation by the displayed axioms and rules is required. The source would need a stronger negation axiom or an extra negation principle to support its requested conclusion.

Let $f=\alpha \to (\beta \to \gamma )$ and $h=\alpha \to \beta$. Temporarily assume $f$, $h$, and $\alpha$. Modus ponens rule first gives $\beta \to \gamma$ from $f$ and $\alpha$, then $\beta$ from $h$ and $\alpha$, and finally $\gamma$.

Apply the deduction theorem for propositional logic successively to discharge $\alpha$, then $h$, then $f$. The result isthe required axiom scheme. This derivation uses only assumptions, modus ponens rule, and the added deduction rule; no negation axiom is involved.

No. The full language can express $\neg (x_0\dot{=}{x}_0)$, which is false in the singleton structure from part (i). Every formula of the reduced language is true in that structure under every assignment in a first-order structure. Therefore no formula of the reduced language can be logically equivalent to this negated equality.

This is a singleton truth-preservation obstruction to expressive completeness. Adding both quantifiers to logical implication does not repair the failure: on this particular nonempty singleton model, quantification cannot create a false formula from true atomic formulas.

Use structural induction on formulas. Every term denotes the unique element. Every atomic predicate is true by hypothesis, and every equality is true because its two terms denote that same element.

If both immediate subformulas of an logical implication are true, their logical implication is true. A universal or existential quantification ranges over the singleton domain; its matrix is true for the only possible value by induction, so either quantified formula is true. These are all the formation cases in the reduced language. Hence

True. In the formation rules, commas occur only between arguments in a function application or an atomic predicate application. Each such argument list includes an opening parenthesis. Subsequent construction of larger terms or formulas retains those symbols.

Equivalently prove by simultaneous structural induction on terms and formulas that an expression containing no opening parenthesis contains no comma. Variables and constants have neither; a comma-bearing function or predicate application already has an opening parenthesis; equality, connectives, and quantifiers cannot introduce a comma outside their constituent expressions. Taking the contrapositive proves the claim.

False. Let $\varphi$ be $x_i\dot{=}{x}_i$ and let $t=x_j$ with $j\ne i$. There is no quantifier that could capture a variable, so $t$ is free for $x_i$ in $\varphi$. Capture-avoiding substitution givesThe number of occurrences of $x_i$ falls from two to zero, contradicting the proposed strict increase. Even capture-avoiding substitution of $x_i$ itself would leave the formula unchanged and refute the strict inequality.

False. Choose a variable $x_j$ different from $x_i$ and takeThe variable $x_i$ does not occur at all, so in particular it is not free. Yet the formula has one universal-quantifier symbol and zero occurrences of $x_i$. The hypothesis on free occurrences of one variable does not control quantifiers binding other variables.

False. A ternary atomic predicate gives a counterexample:This string contains one opening parenthesis and two commas. Thus its number of opening parentheses is smaller than its number of commas. A high-arity argument list contributes several commas while requiring only one pair of parentheses.

The first-order terms are the least collection containing every variable and constant and closed under formation of $f(t_1,\dots ,t_k)$ whenever $f$ has arity $k$ and the $t_j$ are terms. A closed term has no variables.

The first-order formulas are the least collection containing the atomic formulas $t_1\dot{=}{t}_2$ and $P(t_1,\dots ,t_k)$ of the appropriate arities, and closed under negation, logical implication, and universal quantification: from formulas $\varphi ,\psi$ one may form $\neg \varphi$, $(\varphi \to \psi )$, and $\forall x_i\varphi$, with the chosen fully parenthesized grammar. Only finite expressions obtained by these rules are formulas. No additional strings belong to either collection.

Terms denote elements under an assignment in a first-order structure; formulas receive truth values in a first-order structure. The two syntactic categories have different formation rules even when they use some of the same punctuation.

The alphabet of a first-order language separates logical symbols from nonlogical symbols. In the standard presentation here the logical symbols are the variables $x_0,x_1,\dots$, equality $\dot{=}$, negation $\neg$, logical implication $\to$, the universal quantification $\forall$, and the punctuation symbols parentheses and comma. The nonlogical symbols are constant symbols, function symbols of each specified finite arity, and predicate symbols of each specified finite arity, such as $f_n^{(k)}$ and $P_n^{(k)}$.

Constants can equivalently be treated as zero-ary function symbols. Their arities belong to the language specification. Other logical connectives, and $\exists x\varphi$ as an abbreviation for $\neg \forall x\neg \varphi$, need not be primitive alphabet symbols. This distinction matters in counting literal symbol occurrences.