The printed arrow is a partial-function arrow. Thus the central objects are partial computable functions , with total computable functions as the special case in which every input has an output. Here includes zero; changing this convention by a computable shift changes none of the results. A program computing must halt with output exactly on its domain, and run forever elsewhere. A finite program is a function in intension, whereas its possibly partial input-output map is a function in extension; many programs have the same extension.
A precise machine model is a register machine with finitely many instructions to increment a register, decrement it conditionally, jump, and halt. Registers hold natural numbers. A Turing machine instead uses a finite transition table, a finite alphabet and an unbounded tape. These models simulate one another: encode the finite nonblank tape, state and head position as numbers for the register simulation; conversely represent each register by a finite tape block and implement its increment and decrement by finite scans. Tuple inputs can be encoded by a primitive recursive pairing function. The equivalence of these formal models is a mathematical result. Their identification with every informal effective procedure is the Church–Turing thesis, rather than an additional mathematical theorem about an already formal notion.
There is also an algebraic description. Begin with zero, successor and projections, close under composition of partial functions and primitive recursion, and then under unbounded minimization. The primitive recursion scheme is
Applied within the primitive recursive class it produces only total functions, by mathematical induction on . Unbounded minimization searches for the first zero of ; its output is defined only if that search reaches such a zero with every preceding necessary computation defined. Composition is likewise strict about the intermediate values it requires. These schemes compile into machine programs using finite subroutines, loops and an unbounded search loop.
For the converse, encode a machine's finite configurations and finite computation histories using Gödel numbering. Testing that a history starts with the specified input, that every adjacent pair follows the transition table, and that its final configuration halts is primitive recursive: all the tests are bounded by the finite code. Extracting the final output is primitive recursive too. For a suitable checking predicate and output decoder this proves the Kleene normal form theorem:
The symbol means equality of values and of definedness. A halting computation has a passing history code and every passing history has its actual output; a nonhalting computation has none. This proves that the partial recursive and machine-computable functions coincide, including their domains of divergence.
Finite programs can be effectively listed. Simulating the program with index gives a universal partial computable function . Fixing some inputs is effective syntactically: prepend instructions writing those constants and then call the original program. This proves the S-m-n theorem in this machine presentation. In particular, reductions that construct a program from numerical parameters really do produce its index effectively.
The primitive recursive functions are a proper subclass of the total computable functions. Enumerate all valid unary primitive recursive descriptions, interpreting invalid descriptions as zero. Evaluating any fixed valid description terminates by structural induction. Thus the diagonal map is total and computable, but cannot be one of the enumerated primitive recursive maps, since . This is a total computable diagonal over primitive recursive syntax. The evaluator can terminate on every particular description without itself being primitive recursive.
In contrast, one cannot effectively enumerate exactly the programs for all total computable functions. If such an infinite enumeration were available, wait for its th program and run it on , then add one. Totality makes this another total computable function, while its diagonal disagrees with every listed function. Equivalently, there is no total computable universal evaluator listing precisely all total computable maps.
The halting problem is undecidable. If decided whether program halts on , construct a program which halts on input exactly when says that it does not halt. Taking to be 's own index gives a contradiction. The halting relation is nevertheless computably enumerable, since finite halting histories can be searched for.
More generally, a set is computably enumerable exactly when it is the domain of a partial computable function. From an enumeration, halt on when appears; in the other direction use dovetailing over all inputs of a partial program to enumerate its halting inputs. A set is a computable set exactly when both it and its complement are computably enumerable: dovetail the two searches and return the answer from the one that succeeds. Neither a semidecision procedure nor an unbounded search supplies a uniform negative answer.
Finally, the Rice theorem explains the scope of this obstruction. Let be a nontrivial property of the extension of a partial computable program. Choose a partial computable whose -status differs from that of the nowhere-defined function. Given a program and input , effectively form the program which, on , first waits for to halt and then computes . If never halts its extension is nowhere defined; otherwise its extension is . A decision procedure for would therefore decide the halting problem. Effective descriptions allow universal simulation and positive verification, but not a decision procedure for every semantic property or for termination.
Represent the arena by a pruned set-theoretic tree of legal finite positions. Players I and II alternate; every position has a legal continuation. The usual terminal-position convention can also be handled by adding terminal wins and losses at the initial stage. Give the branches the product topology generated by finite-position cylinders, and let be I's winning open set.
Define the winning-position attractor in an infinite game by transfinite recursion. Start with
At a successor stage retain and add I-positions with at least one child in , and II-positions with every child in . At a limit stage take the union. The increasing sequence stabilizes because the positions form a set: strict increases at arbitrarily many stages would select too many distinct positions. Write for the stable set. The rank of a position in is its first entry stage; any positive such rank is a successor ordinal.
If the initial position belongs to , at every I-position of positive rank choose a child that was present at the preceding stage. Every move by II also leads to a child of smaller rank, by the rule for II-positions. There is no infinite strictly decreasing sequence of ordinals, so every play following this strategy in an infinite game reaches after finitely many moves. Its complete branch then belongs to . Hence this is a winning strategy in an infinite game for I.
If the initial position is outside , every move of I stays outside . At a II-position outside at least one child is outside : otherwise the entry ranks of its set of children have a common ordinal bound, and that position would enter at the next stage. Choose such a child. This gives II a strategy in an infinite game that never enters . A resulting branch cannot belong to , because is an open set and would therefore have a finite prefix whose whole cylinder lies in , namely a member of . Thus II wins. This proves the Gale-Stewart theorem for an arbitrary set-sized arena, in the ordinary metatheory with choice. Countability of the move set was never used.
The restriction on the payoff is essential. Under the axiom of choice, already for binary moves there is an undetermined game. There are strategies for each player, since a strategy is a binary-valued map on a countable set of positions. List I's strategies and II's strategies for . Each strategy is compatible with different plays, obtained by varying all the opponent's binary moves.
At stage , choose a fresh play following and then a different fresh play following , avoiding every previously chosen play. Fewer than plays have been used at that stage, even when is singular, so these choices are possible. Let . No I-strategy wins , because its selected is outside ; no II-strategy wins, because its selected is inside . Future choices avoid all earlier , so they never spoil the first assertion. This is the choice diagonalization of an undetermined game. Consequently determinacy for all payoff sets is incompatible with the axiom of choice. The attractor still makes sense for a nonopen payoff, but an avoiding play may then enter the payoff without ever having a winning finite prefix.
Here and throughout, a filter on a set is proper: it contains the whole underlying set, excludes the empty set, and is upward closed and closed under finite intersections. An improper filter cannot be extended to a proper ultrafilter.
Order the proper filter extensions of by inclusion. The union of a chain is again a proper filter on a set: any two members already occur in one member of the chain, where their intersection belongs; the empty set never appears. By Zorn lemma, take a maximal proper extension . If , adjoining must make the generated filter improper, so some has . Upward closure then gives . Exactly one of belongs to , proving the ultrafilter lemma.
Let be nonempty structures for a common first-order language, and let be an ultrafilter on the index set . In the ultraproduct , identify functions when ; interpret function symbols coordinatewise and relations by membership of their coordinate truth sets in . The Łoś theorem states, for every first-order formula ,
Changing representatives changes a coordinate truth set only outside a member of , so the definitions are well defined.
Prove the theorem by structural induction on formulas. An induction on terms gives , and therefore the required equivalence for atomic equality and relation formulas. For conjunction the truth set is an intersection, and a finite intersection belongs to a proper filter on a set exactly when each constituent does. For negation it is a complement, and the ultrafilter decides exactly one of a set and its complement. These prove the Boolean induction steps.
For the existential step, a witness in gives, by induction, a member of on which holds. It is contained in the coordinate existential truth set, so that set belongs to . Conversely, if
choose a coordinate witness for , and any element of the nonempty factor otherwise. Then the truth set of contains . Induction gives a witness in the ultraproduct. Universal quantification follows from negation and existence. This completes the actual proof of the Łoś theorem.
For the compactness theorem, take to be the set of finite subsets of , and choose a model of each such subset. The cones
are nonempty and satisfy . They generate a proper filter on a set, which extends to an ultrafilter by the proved lemma. For every , the coordinate truth set of contains . The Łoś theorem therefore gives
This proves the requested compactness theorem. In fact the same proof works without the countability restriction on the language.
Fix an effective syntax encoding for the language. Let be the finite set of axioms observed in the first steps of an enumeration of the given semidecidable axiomatization. These finite approximations can be computed in bounded time, even if the original axiom set is empty or finite. For each , form the precisely bracketed logical conjunction
with . Let .
Each is logically equivalent to , so all members of follow from the original axioms. Every original axiom eventually belongs to some , and its corresponding member implies it. Hence axiomatizes exactly the same theory.
To decide whether a candidate sentence belongs to , let be its syntactic length. A conjunction of copies has length at least , so a representation can only use . Compute each for , construct its finitely many candidates, and compare them literally with . This finite procedure always terminates and accepts exactly . It does not wait for a nonexistent next axiom, nor assume that conjunction parsing determines the original repeated formula uniquely. Thus is a decidable equivalent axiomatization, proving the Craig trick.
Use the logical truth constants , and put
For a truth assignment with true, has the value of and has the same value. For an assignment with false, both have the value of . Thus the propositional variable elimination identity is
Neither substituted formula contains .
Let , and eliminate all the private letters of by taking
where a Boolean assignment substitutes or for each letter. Then . Every assignment satisfying satisfies the disjunct corresponding to its own private-letter values, so .
If an assignment satisfies , choose a disjunct witnessing this, and modify only its values on to the corresponding . The modified assignment satisfies , hence satisfies by soundness of . Its values on every letter of have remained unchanged, so the original assignment also satisfies . Therefore . The propositional completeness theorem converts these two valid implications into
proving propositional interpolation constructively.
If the syntax does not initially include , they can be admitted as logical constants without adding propositional letters. This convention matters when the common vocabulary is empty: a grammar in which every formula must contain a letter has no letter-free interpolant at all. For example, two tautologies using disjoint letters entail one another but cannot have an interpolant in that grammar. The truth-constant convention supplies exactly the necessary empty-vocabulary case.
Work inside a model of ZF. Let be a definable class bijection, with definable inverse, so that its image and inverse image of every set are sets by Axiom schema of replacement. Define new membership by
This is the Rieger-Bernays permutation model convention used here. Its basic advantage is that every prescribed old set is the new extension of the object . We verify the axioms rather than treating a membership permutation as automatically harmless.
The new axiom of extensionality follows because equality of the new extensions means , hence . The new empty set and unordered pair are and . Union and power set are represented by
Indeed, the elements of the first object are exactly the new elements of new elements of ; the elements of the second are exactly the objects whose new extensions are subsets of .
Translate an arbitrary formula recursively by replacing each atomic by . This is an ordinary definable formula in the old model. Old axiom schema of separation forms any specified subclass of , and supplies the new separated set. Old Axiom schema of replacement similarly collects the uniquely specified images of all elements of , and applying supplies its new representative. This verifies the full schemas, including formulas with unbounded quantifiers.
For axiom of infinity, define and
Then . These objects are distinct by induction: equality of with an earlier would equate old sets of respectively and distinct members. Old replacement collects , and is a new inductive set. Thus the construction satisfies every axiom of ZF except possibly Axiom of foundation.
Now interchange the old objects and and fix everything else. For we have , so its new sole member is itself: . This Quine atom contradicts Axiom of foundation. The identity permutation preserves the original model and its foundation. Hence, relative to consistency of ZF, foundation is independent of the other ZF axioms.
For the further independence result, a full permutation of a model of choice is insufficient. If the old model satisfies axiom of choice, then for any new family of nonempty new sets, old choice selects for every . Encode its graph using the new ordered pairs, and represent that graph by . This is a new choice function. We therefore add a hereditary finite-support restriction to a universe with many Quine atoms.
Start now with a model of ZFC. Put , and let interchange and for every , fixing other objects. All these transpositions are disjoint: the infinite ordinals are distinct and none is a singleton. In the resulting membership structure, is an infinite family of Quine atoms.
Build its universe by the internal transfinite hierarchy
Write for the union over the old ordinals. Apart from the atomic self-loops, an object's new members have lower construction ranks. Every permutation of therefore extends recursively to : on atoms use the prescribed permutation, and on other objects put
This is well defined and preserves . A nonatom cannot be sent to an atom, since an extension consisting solely of one atom already represents that atom. Recursing with gives the inverse, so these maps are genuine automorphisms.
Say that has finite support if every such permutation fixing pointwise fixes . Let consist of the atoms and the objects with finite support all of whose new members, recursively away from atomic self-loops, belong to . This is the hereditarily finite-supported Quine-atom model. We check why it still has the required set-theoretic axioms.
It is closed under taking new members, so extensionality remains valid. The empty object and the pure finite ordinals have empty support. Their internally represented infinite collection also has empty support, giving infinity. Pairs and unions use the finite unions of their constituents' supports; all their members remain hereditary members of .
For a set , take all objects whose new extensions are subsets of . They form an old set, since the unrestricted new power set is an old set and membership in is definable. Its representative has support contained in a support of , because an automorphism fixing permutes precisely these hereditary subsets. All its members belong to . Hence this is the power set required inside , not a claim that unrestricted external subsets are retained.
For separation, relativize the formula to . A support for together with supports of the finitely many parameters fixes the resulting subclass; its members are hereditary, so its representative belongs to . For replacement, old replacement applied to this relativized definable functional relation collects the range. Its members have a common bound on their construction ranks, by taking the supremum of the set of ranks, so the range's representative lies in . The same finite union of parameter and domain supports fixes the range by uniqueness of each image. It is therefore hereditary and belongs to . These arguments verify the full schemas. Thus .
Finally and the family of its two-element subsets belong to with empty support. Suppose a choice function for this family belongs to , and let be a finite support for . Choose distinct atoms and transpose them. This permutation fixes and fixes the unordered pair , but interchanges its two possible selected members. Equivariance would require
which is impossible. Hence choice fails in . Together with a model of ZFC, or with its full permuted model satisfying choice and failing foundation, this proves independence of axiom of choice from ZF minus foundation, relative to consistency of ZFC. All hierarchy and support arguments are internal to the starting model; no transitive-model assumption is needed.
For the Ehrenfeucht-Mostowski theorem, let be an infinite first-order structure and any linear order. Choose a full Skolem expansion : add witness functions for existential formulas, repeat in the expanded languages, and take their union. We will construct a model of its theory containing distinct generators , , forming an order-indiscernible sequence.
Adjoin the elementary diagram of , the inequalities for , and for every expanded-language formula and every two increasing -tuples of indices, the sentences
Every finite subcollection is satisfiable in . To prove this, choose a countably infinite sequence of distinct elements of , and for each of the finitely many relevant arities color its increasing index tuples by the finite vector of truth values of the formulas of that arity. Repeated applications of the Ramsey's theorem give an infinite subsequence homogeneous for all these finitely many finite colorings. Interpret the finitely many mentioned by its elements in their index order. All indiscernibility and distinctness constraints hold, and the finite diagram fragment holds because the ambient structure is still .
By compactness theorem, a model of the full enlarged theory exists. Its Skolem hull generated by the is elementary: whenever an existential formula with parameters in holds in , its chosen witness function returns a value in , so the Tarski-Vaught test applies. Its reduct is a model of . If the index order has size , the hull has size at most , and it contains distinct generators.
Every order automorphism of induces the automorphism
To check well-definedness, write any two terms being compared over the same increasing list of their generators. Their equality is an expanded-language formula; indiscernibility of the order-indiscernible sequence preserves its truth under . The same argument preserves each relation, and the term construction preserves the functions. Applying gives the inverse. The extension is unique in the specified Skolem language since every hull element is a term in the generators; no uniqueness among all automorphisms of the reduct is being asserted. This proves the Ehrenfeucht-Mostowski theorem, including its usual automorphism consequence.
For simple typed set theory with atoms, use sorts , predicates for sets, and typed membership from sort to sort . Atoms have no members, extensionality compares sets, and every well-typed formula defines a set of the next sort. Typical ambiguity is the schema for every closed typed sentence, where the superscript raises all types by one.
Here are concrete full typed models before imposing the ambiguity schema. Choose increasing natural numbers and set
The auxiliary merely interprets the set predicate at the lowest sort. Define typed membership by
Then the other objects of are atoms, regardless of their old membership. Every subset of has its representative in , giving comprehension even for formulas with higher-sort quantifiers and parameters. Extensionality holds for the set representatives and atoms have no typed members. The rank gaps leave infinitely many atoms at each sort, and all sorts are infinite.
Consider finitely many ambiguity instances with unraised sentences , and choose a fixed window length sufficient to include every sort used and its auxiliary predecessor. Color every increasing -tuple of natural numbers by the vector of truth values of these unraised sentences in its finite rank-window interpretation. There are only colors. The Ramsey's theorem gives an infinite homogeneous set. Choose successive points from it. The first points and last points have the same color, while the latter interpretation of is exactly the former model's interpretation of . The auxiliary predecessor shifts too, so this remains true for sentences mentioning the lowest set predicate. Extend the chosen rank sequence arbitrarily to interpret the remaining sorts. This yields a model of typed set theory satisfying all the specified ambiguity instances.
Thus every finite subset of the typed axioms together with all ambiguity instances has a model. Applying multisorted compactness theorem gives
The final model satisfies first-order typed comprehension, with quantification over its own sorts and sets as in Henkin semantics.
The exponent-two Erdős-Rado theorem for pairs says that for every infinite cardinal ,
In particular, a finite or countable coloring of pairs from has an uncountable monochromatic subset. We prove the general statement by an end-homogeneous tree construction.
Let be any coloring on an ordinal . Route a vertex through an increasing sequence of preceding vertices as follows. Start with the least vertex. After ancestors , , have been selected, choose the least remaining candidate , above those ancestors, satisfying
The terminal candidate always qualifies, so the procedure eventually reaches it. Candidate sets shrink and their least elements increase. If an intermediate candidate is , its route is precisely the earlier part of the route to , because all earlier color tests agree. Consequently the routes define a set-theoretic tree on the vertices.
Along a branch, the color from an ancestor to every later branch vertex is constant. Also a node of height is determined by its sequence of colors to its ancestors: reconstruct the ancestors as successive least candidates with those prescribed colors, then reconstruct the node as the least final candidate. Thus its level has at most nodes.
Apply this with and . If every node had height less than , each level would have size at most , and there would be at most such levels. Their total size would be at most , contradicting . Hence some route has at least ancestors. For each ancestor mark its constant color to all later route points. Since there are only colors, one occurs on ancestors. Those ancestors form the required monochromatic set. This proves the theorem.
To make the ordinal function precise, one useful ordinal partition-bound function is
The target here is ordinal order type. For infinite , the proved theorem with supplies a bound : its homogeneous set has order type at least , and it handles all the required color counts. Finite targets are handled by finite Ramsey theorem bounds. Thus is total, nondecreasing and .
Suppose a sequence of transfinite iterates , with suprema at limit stages, has supremum an uncountable cardinal at a limit stage, with every earlier iterate below . Then
choose an earlier iterate at least and use the next one as a bound. If the iteration has already stabilized, it has already found a fixed point instead.
This closure forces to be a strong limit cardinal. For any infinite , color pairs of distinct binary strings of length by their first differing coordinate. This uses colors and has no monochromatic triangle: three binary digits at one coordinate cannot be pairwise different. It gives a coloring on with no homogeneous target of type . Since colors are allowed when the target is the ordinal , we have
Finite exponents satisfy the strong-limit requirement automatically for uncountable .
The needed additional condition is the tree property: every tree of height , with nonempty levels of size less than , has a cofinal branch. In the present convention it forces to be a regular cardinal. If were singular, take a cofinal sequence of smaller cardinals of length and form the disjoint union of chains of those lengths. This tree has height and total size , levels of size at most , but no branch of length , a contradiction.
For any , apply the preceding color-routing tree to a coloring . If a route already has length , use it. Otherwise its levels are indexed below and each has size
for infinite exponents, by the strong-limit property; finite cases satisfy the same needed bound directly. The tree has nodes, so regularity forces its height to be . The tree property supplies a cofinal branch. The ancestor-color partition of that branch has one class of size , since and is regular. Thus for every , and
We have proved that an uncountable function-closed cardinal with the tree property is regular and strong limit, hence strongly inaccessible, and that it is the requested fixed point.
The paper's final sentence, read as a claim about the tree property alone, is false. Already has it by the König infinity lemma but is not uncountable; even with uncountability stipulated, there are relative-consistency models with the tree property at . The latter counterexample is documented in the research account of Mitchell forcing. The rigorous conclusion in the iterated-function context is the one just proved: function closure supplies strong limit, and the tree property supplies regularity and a branch. Strong limit and regularity follow from distinct hypotheses in this context.
Let be a full Skolem expansion of an infinite structure , choose distinct for , and extend the cofinite filter to a nonprincipal ultrafilter on . For a finite subset of the desired index order , define the ordered Fubini product of ultrafilters on by
where means . These nested tests decide complements and preserve intersections by induction on , so is indeed an ultrafilter. For the empty set use the one-point index set and its principal ultrafilter.
Put . If , projection of coordinates induces
A truth test independent of a coordinate is unchanged by its dummy ultrafilter quantifier. Consequently pullback preserves exactly the -large subsets, proving that the map is well defined and injective. The Łoś theorem, applied to every formula rather than just to equality, proves that it is an elementary embedding. Projections compose, so these elementary maps form a coherent directed system.
Take its directed limit of elementary embeddings . Explicitly identify two stage elements when their images agree at a common larger stage, and interpret functions and relations there. For an existential formula true in the limit, its parameters and a witness occur at a common stage; elementarity then pulls truth back to the stage of the original parameters. This verifies that all stage maps into the limit are elementary.
Let be the image in this limit of the coordinate class . These elements are distinct: in , equality would require , whose inner-coordinate section is a singleton and hence not in the nonprincipal . For , the truth of any expanded-language formula on is exactly
This expression depends on the formula and the tuple length, not on the chosen increasing indices. Thus is an order-indiscernible sequence. The empty-coordinate stage embeds elementarily into .
Their Skolem hull is elementary by the witness-function argument, and an order automorphism of extends to it by transporting the generators in every term. Equality and relation preservation follow from the displayed uniform truth test, and the inverse order automorphism gives the inverse map. Therefore this proves the Ehrenfeucht-Mostowski theorem through ultrapowers and their directed limit, with no Ramsey-theoretic step.
A model-theoretic ultralimit is the direct limit of a chain of successive ultrapowers along their diagonal elementary maps. It is not the topological notion of a limit along an ultrafilter. We first prove the precise relative embedding lemma needed to synchronize two such limits.
If , then embeds elementarily into an ultrapower of , with the embedding restricting on to its diagonal map. To prove this Frayne embedding lemma, use the elementary diagram of with the elements of treated as named parameters. Every finite fragment of that diagram has a realization in : replace its finitely many names from by variables and existentially quantify their conjunction. It is true in , and hence true in by elementarity. Choose these simultaneous realizations for each finite fragment, keeping every parameter from interpreted as itself; give unmentioned names an arbitrary default in the nonempty .
On the index set of finite fragments, extend the filter of cones to an ultrafilter . For each , let be its value in the chosen coordinate realization. Every diagram sentence is satisfied on its cone, so the Łoś theorem makes an elementary embedding . Inequalities in the diagram ensure injectivity. If , all its coordinates equal , giving exactly the diagonal map.
There is also the initial version: if merely , then embeds elementarily into an ultrapower of . A finite fragment of the elementary diagram of , with all its names replaced by variables, yields an existential sentence true in and hence in . The identical finite-fragment and cone construction therefore proves this version without already assuming an embedding.
Start with . Use the initial version to place elementarily in an ultrapower of . Relabel embedded copies so we can regard the elementary maps as inclusions. Apply the relative version to to obtain an ultrapower of containing , and whose inclusion of is its diagonal map. Next apply it to to obtain an ultrapower of containing , again fixing the earlier diagonal inclusion. Continuing gives an elementary chain
The common union is elementary over every stage by the elementary chain theorem, and
The first presentation is a model-theoretic ultralimit of . The second, preceded by the initial diagonal embedding of into , is a model-theoretic ultralimit of . Each consecutive same-letter inclusion is precisely the corresponding ultrapower diagonal map, not just an unspecified elementary embedding. Thus the two limits are identified with the same structure , proving

Articles by others on the same topic (0)

There are currently no matching articles.