The alphabet of a first-order language separates logical symbols from nonlogical symbols. In the standard presentation here the logical symbols are the variables , equality , negation , logical implication , the universal quantification , 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 and .
Constants can equivalently be treated as zero-ary function symbols. Their arities belong to the language specification. Other logical connectives, and as an abbreviation for , need not be primitive alphabet symbols. This distinction matters in counting literal symbol occurrences.
The first-order terms are the least collection containing every variable and constant and closed under formation of whenever has arity and the are terms. A closed term has no variables.
The first-order formulas are the least collection containing the atomic formulas and of the appropriate arities, and closed under negation, logical implication, and universal quantification: from formulas one may form , , and , 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.
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.
False. Choose a variable different from and takeThe variable does not occur at all, so in particular it is not free. Yet the formula has one universal-quantifier symbol and zero occurrences of . The hypothesis on free occurrences of one variable does not control quantifiers binding other variables.
False. Let be and let with . There is no quantifier that could capture a variable, so is free for in . Capture-avoiding substitution givesThe number of occurrences of falls from two to zero, contradicting the proposed strict increase. Even capture-avoiding substitution of itself would leave the formula unchanged and refute the strict inequality.
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.
A collection of logical connectives is adequate, or has functional completeness, if every Boolean function of finitely many propositional variables can be expressed by a formula using those connectives and variables, with the usual convention for nullary truth constants stated if those are included.
An adequate example is . An inadequate example is : formulas using logical implication alone preserve truth when every input is true, so cannot express negation. These examples concern truth functions, rather than mere syntactic formation of 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
No. The full language can express , 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.
Let and . Temporarily assume , , and . Modus ponens rule first gives from and , then from and , and finally .
Apply the deduction theorem for propositional logic successively to discharge , then , then . The result isthe required axiom scheme. This derivation uses only assumptions, modus ponens rule, and the added deduction rule; no negation axiom is involved.
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 , but interpret the unary symbol by the constant function .
Every instance of the first axiom is valid. In the replacement axiom, both and have value , 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 and . 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.
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 and , the first axiom gives . The old third axiom then gives , and modus ponens rule with gives any desired .
Next derive the classical reductio rule. Suppose derives both and . Let be the theorem , obtainable by applying the deduction theorem for propositional logic to the identity derivation from assumption . Explosion under gives , so the deduction theorem for propositional logic gives . The old third axiom with , yields . Since is a theorem, . Thus a contradiction under permits deriving with that temporary assumption discharged.
Now assume and , and temporarily also assume . Modus ponens rule gives , contradicting . The just-proved reductio rule discharges and gives . Finally discharge and by the deduction theorem for propositional logic:No propositional completeness theorem is needed in this derivation.
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 and let be an instance of the old contraposition axiom, for example with distinct propositional variables in place of . 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.
Write and . All derivations below use the printed replacement axiom, so they do not rely on the false equivalence from part (a).
The identity logical implication follows by the deduction rule. Substituting , into the replacement axiom and applying modus ponens rule therefore gives double-negation elimination:Universal instantiation gives . Combine it with using modus ponens rule under a temporary assumption and then the deduction rule, obtaining .
In the replacement axiom now substitute and . Its antecedent is precisely the last theorem, and its consequent is . ThusUnder the fixed assumption and temporary assumption , modus ponens rule gives and then . Discharge the temporary assumption to obtain .
Finally apply universal generalization. The variable is not free in , because it is bound in and is not free in by hypothesis. Hence the side condition is satisfied andGeneralization is applied after the temporary assumption has been discharged; applying it while that assumption remained open would not be justified.
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 for which both and 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.
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 , exactly one of and belongs to it.
For example, if but , adding does not create a new contradiction, contrary to maximality. Thus maximality includes deductive closure, not only having as many independent axioms as possible.
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.
Order the consistent sets of sentences extending 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 .
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.
Suppose a structure satisfies every sentence of . By the soundness theorem for first-order logic, every sentence derivable from 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 . This direction uses soundness alone, without constructing a model from a proof-theoretic assumption.
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 . 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 and hence the original .
An arbitrary sentence set need not already have enough closed terms or witnesses. Calling this a term model for means a term-model construction of a model satisfying , usually through that witnessed completion; it does not assert that every arbitrary itself already supplies the construction.
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 for a required parameter set . 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 . Add that many pairwise unequal constants, apply compactness, and then the size-bounded construction. The countable consequence is the part needed below.
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.
Yes. The usual order on the rational numbers is strict and linear. Between lies the rational midpoint , and witness absence of endpoints. Thus it is a dense linear order without endpoints.
Yes. The usual order on the real numbers is strict and linear, midpoints witness density, and translation by supplies points on either side. It therefore satisfies the same dense linear order without endpoints axioms.
No. With its induced usual order, the closed interval has a least element and a greatest element. At zero there is no smaller domain element, and at one there is no larger domain element. It fails the no-endpoint axioms, although it is densely ordered.
Yes. The induced order is strict and linear and remains dense. For , the points and lie in the domain and are strictly below and above . Hence the open interval is a dense linear order without endpoints.
Yes. Removing zero leaves the induced order strict and linear, with no endpoints. For any there are infinitely many points in the real interval between them, so one can choose an intermediate point different from zero. More explicitly, the midpoint works unless it is zero, in which case is nonzero and lies strictly between the endpoints. Thus density also survives.
The missing point is a cut, not a pair of adjacent elements; the axioms do not require all cuts to be filled.
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.
The theory is consistent because the rational order is a model. If some sentence were not decided by the theory, both extensions by and by 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 , 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.
Articles by others on the same topic
There are currently no matching articles.