A proper filter on a set contains , excludes , is upward closed, and is closed under finite intersections. Order its proper extensions by inclusion. The union of a nonempty chain is again a proper filter: finitely many members lie together in one chain member. Zorn lemma, and hence the axiom of choice, gives a maximal extension . If neither nor belongs to , maximality of says adjoining either one produces the improper filter. There are therefore with and , contradicting . Thus is an ultrafilter.
For Łoś theorem, interpret the ultraproduct using when , with functions and relations interpreted coordinatewise. These interpretations are well defined because changing finitely many argument representatives changes them only outside the intersection of their agreement sets, which belongs to . For any first-order formula and sequences of parameters,Prove this by structural induction. Atomic formulas follow from the interpretation of terms. Conjunction uses finite intersections; negation uses the ultrafilter dichotomy between a set and its complement. If holds in the ultraproduct, a witness sequence gives a subset of in . Conversely, choose a witness for in every factor where one exists, and an arbitrary element in every other factor. This is the second explicit use of the axiom of choice; all factors have nonempty carriers. The inductive hypothesis applied to supplies the ultraproduct witness. The other connectives and universal quantification follow from these cases.
For the possible worlds, use free filters, equivalently proper filters extending the cofinite filter . Here “nonprincipal” must have this free-filter meaning: merely saying that a filter has no single generating subset need not make an accessible least world. The designated world is , and all worlds have carrier . Atoms, including equality, are forced byEquality may identify distinct sequences at a world; it is a persistent congruence, and at an ultrafilter world its quotient is the ordinary ultraproduct.
The required equivalence with all ultraproducts uses dense-extension filter semantics. Its recursive clauses areEvery extension in these clauses is a free proper filter. The dense clause for disjunction is essential; for propositional formulas, local disjunction would instead give a Kripke model for intuitionistic propositional logic and would invalidate the claimed equivalence.
The useful separation fact is membership in a free filter is detected by its ultrafilter extensions:Indeed, if , every has infinite intersection with : a finite intersection would imply after intersecting with a suitable cofinite set. Hence adjoining generates a free proper filter, which extends to a nonprincipal ultrafilter by the ultrafilter lemma.
Induction on formulas now gives . Negation and implication follow by adjoining the positive set on which their classical truth conditions fail. For disjunction, membership of lets every extension be refined to an ultrafilter containing one of the two sets. If that union is absent from , an ultrafilter extending contains its complement and has no further proper extension, contradicting the dense clause. For existence, choose coordinate witnesses on as in Łoś theorem. For universality, if , choose a counterexample in every factor outside it and arbitrary elements elsewhere. The resulting sequence has , so cannot force that instance. The converse follows from upward closure and persistence.
At the designated world, therefore,This semantics validates classical first-order logic, including law of excluded middle. For example, every free filter has an ultrafilter refinement deciding an atomic formula, so its excluded middle is forced even when neither disjunct is forced at the original world. To see concretely why local disjunction fails, take and an atom true exactly at even indices: neither its truth set nor its complement is cofinite, although every ultraproduct satisfies its excluded middle.
Use the following form of the omitting types theorem. Let be a consistent first-order theory in a countable first-order language, and let be a countable family of finite-arity partial types. Suppose each is a nonprincipal partial type: no formula consistent with satisfies for every . Then has a countable model omitting all the .
For the proof, add countably many fresh constants and perform a Henkin construction. Enumerate three kinds of tasks: deciding each sentence, providing a fresh constant witness for each existential sentence, and making every constant tuple omit each of the corresponding arity. Starting with the empty set, keep a finite set such that is consistent. A sentence can be decided in one of its two ways while preserving consistency. For an existential sentence, add with fresh; inconsistency would contradict freshness and the existential sentence itself.
For an omission task at a tuple , let be the conjunction of . Replace its constants by variables, identify the occurrences of the tuple's constants with the corresponding variables , and existentially quantify the other variables. If the tuple repeats a constant, include the corresponding equalities between its variables. This gives with consistent. Nonprincipality supplies such thatis consistent. Reintroducing the constants shows that is a permitted next stage. Thus each constant tuple will fail some formula of each prescribed type.
The union is consistent by the finite character of formal proofs, complete in the expanded language, and has the Henkin witness property. Its term model has closed terms modulo provable equality as elements, and satisfies the truth lemma for a Henkin term model, proved by induction on formulas. It is countable. Every closed term equals a constant in this model: apply the witness task to . Consequently every tuple is represented by a constant tuple and fails a formula of each . This proves simultaneous omission.
For arithmetic, the nonstandard element type isIn a model of Peano arithmetic, an element omits this type precisely when it is one of the standard numerals: arithmetic proves that every element at most equals one of . A model omitting everywhere is therefore isomorphic to the standard structure .
For a complete consistent theory , this gives the particularly useful equivalenceThe first implication is the omitting types theorem. For the converse, if a consistent over the theory of true arithmetic implied every , completeness would give . A standard witness contradicts the implication .
Completeness matters in this formulation. One must not claim that is automatically nonprincipal over an arbitrary incomplete arithmetic theory. For example, assuming consistency of Peano arithmetic, the formula saying that is the least code of a proof of a contradiction is consistent with that theory, by Gödel second incompleteness theorem, and implies for each standard . It makes principal over that incomplete theory, although its standard model still omits the type. The theorem is a sufficient omission criterion, not a necessary one for arbitrary partial types over incomplete theories.
The machine characterization is computation by a Turing machine: the machine halts with exactly on inputs in the domain of a partial function and does not halt elsewhere. The syntactic characterization is the least class containing the initial functions of recursion theory and closed under composition of partial functions, primitive recursion and unbounded minimization. Such functions are the partial recursive functions, equivalently the partial computable functions.
For clarity, composition here is strict: is defined only when every inner value is defined and is defined on the resulting tuple. Likewise primitive recursion requires all preceding recursive values. The partial minimization is defined when such a exists and all earlier values are defined and nonzero; an undefined earlier value blocks the search.
A lambda-definable partial function is represented by a closed untyped lambda calculus term satisfyingOn an input outside its domain there must be no Church numeral beta-equivalent to the result. A stronger representation can be arranged: undefined inputs have no head normal form.
Here are the components for proving that every partial recursive function is lambda-definable. Zero and projections are immediate; lambda definition of the successor function uses . Church Booleans encode a conditional by , with and . PutIteration takes to for , proving that encodes the predecessor function and that correctly tests zero.
Use a fixed-point combinator and the strict sequencing operationFor any numeral , reduces to . If the first argument has no head normal form, neither does the whole expression. Thus composition is implemented by nesting on every inner result before applying the outer representing term. This guard is important: an unguarded projection could discard an undefined inner computation.
For lambda definition of primitive recursion, with already represented by , takeThe tuple notation abbreviates successive abstractions and applications. On numeral inputs, induction on proves the required recursion equations, including strict propagation of undefined preceding values. The beta reduction follows the selected conditional branch only.
For lambda definition of unbounded minimization, useThis searches in increasing order. An undefined value blocks the zero test; an infinite sequence of nonzero values continues forever; the first zero returns its numeral. Under normal-order beta reduction, both failure cases have no head normal form. Structural induction on partial-recursive declarations now supplies the stronger representation claimed above.
Conversely, beta reduction is an effective operation on finitely encoded lambda terms. Enumerate all finite reduction sequences from , stopping when a result is a Church numeral in beta-normal form. If , the Church-Rosser theorem gives a reduction to that numeral. It also makes the output unique. The enumeration therefore computes exactly the represented partial function; by the equivalence of the first two characterizations it is partial recursive. Hence
A many-one reduction is a total computable function with . A Turing reduction is an oracle machine which decides with oracle . It may make several adaptive queries and combine their answers. Every many-one reduction is a Turing reduction, by asking the single question . The converse fails: for the diagonal halting set , its complement is Turing-reducible to by reversing one oracle answer, but is not many-one reducible to . Such a reduction would make the complement computably enumerable, contradicting undecidability of the halting problem.
The Friedberg–Muchnik theorem asserts that there are computably enumerable sets with incomparable Turing degrees:Here is a finite-injury priority construction proving it. Enumerate all Turing functionals and put the requirements in the priority orderStart with . Each requirement has a fresh witness, a waiting or acted status, and a restraint on the other set. A restraint forbids lower-priority strategies from enumerating numbers below into that oracle. Globally remember all previously chosen witnesses, including abandoned ones, and never choose any of them again.
For , choose an unused witness outside , larger than the stage and every current higher-priority restraint. Keep it out of . Wait until the bounded simulation converges with value zero. If this happens, enumerate into , put a restraint on , where is one more than the largest oracle query in the observed computation, and mark the strategy acted. For , interchange and .
At stage , consider the first requirements. Choose the highest-priority one needing a witness or waiting with an observed zero computation. Perform its indicated action, then initialize all lower-priority requirements: abandon their witnesses, clear their restraints, and reset their status. Do nothing if no requirement needs attention. Since witness selection respects higher restraints, and higher actions initialize every lower strategy, all protected computations are respected by lower-priority enumerations. Each stage is a finite effective calculation, so and are computably enumerable sets.
Verify by induction along the priority order that every requirement is initialized only finitely often and acts only finitely often. The highest requirement chooses one witness and can diagonalize at most once. After all higher requirements have finished acting, the next requirement is never again initialized; it obtains a final witness and can diagonalize at most once. This proves finite injury for every requirement and ensures that no requirement is permanently starved by higher attention.
Consider after its last initialization. If it acts, its witness belongs to , while the protected computation with oracle remains zero: higher strategies no longer act and lower ones respect its restraint. Thus . If it never acts, its private witness remains outside . Were , the computation on that witness would converge to zero with a finite oracle use. Since the increasing sets eventually agree with on this finite initial segment, a sufficiently late bounded simulation would detect that computation and make act, a contradiction. The symmetric argument verifies every .
Thus the two sets have incomparable Turing degrees. Both are noncomputable, since a computable set is Turing-reducible to every oracle. Both are also strictly below the degree of the halting problem: every computably enumerable set is Turing-reducible to , while completeness of one would make the other reducible to it. This supplies the intermediate degrees sought in Post problem.
Articles by others on the same topic
There are currently no matching articles.