There is no computable presentation of a Nonstandard model of Peano arithmetic. We prove Tennenbaum theorem by obtaining a computable set separating two recursively inseparable sets.
Fix an effective enumeration of partial computable functions, implemented by deterministic machines, and putThese are disjoint computably enumerable sets. To see that they are recursively inseparable sets, suppose a computable set contains and avoids . Its indicator function has some index . If , then , contradicting that output. If , then , contradicting . Thus neither output is possible.
Let be a Nonstandard model of Peano arithmetic. A recursive presentation of a structure here means a presentation on in which its arithmetic operations are total computable functions; equality of presentation codes is ordinary equality. Write for the element represented by the standard numeral . The presentation codes of are fixed constants, so is a total computable function obtained by repeated addition. Presentation codes and the arithmetic values they name must be kept distinct.
Use bounded simulation of a computation predicates saying that machine , on input , has halted by time with output . We can choose these as primitive recursive predicates represented in Peano arithmetic. Determinism and induction on the computation length give, provably in Peano arithmetic, monotonicity in andA genuine standard halting computation has a finite certificate which Peano arithmetic verifies. Consequently, if or , the corresponding holds in for some standard .
Choose a nonstandard element of . It exceeds every standard numeral. Let be the th prime number, starting with . Peano arithmetic proves the prime-divisibility coding of a finite set needed here: for each , an element can be formed as the product of precisely those with for which holds. Formally,This is an internally finite product, not a claim that its externally observed index set is finite. Its existence follows by mathematical induction on the cutoff: start with , multiply by the next distinct prime number when its predicate holds, and otherwise retain the product. Unique prime factorization ensures that earlier divisibility decisions are preserved. The standard prime enumeration and these finite-product constructions are provably total in Peano arithmetic.
Define the external subset . If , its standard halting time is below , and monotonicity gives , so . If , its output-one certificate and the provable incompatibility above exclude , so . Hence separates and .
Finally is a computable set. Given standard , compute the ordinary integer and its numeral in the presentation. Enumerate all presentation codes , and for each test the finitely many standard remainders forEach test is decidable using the assumed total computable functions. The division theorem of Peano arithmetic guarantees a quotient and a remainder below the standard numeral . Every element below that numeral is one of , so the search terminates; the remainder is unique. Return yes exactly when . This makes a computable set, contradicting the recursively inseparable sets construction. Therefore
The minimal deterministic finite automaton is unique up to an isomorphism preserving the initial state, transitions and accepting states. We use complete deterministic finite automata over the fixed alphabet; the PDF's abbreviation FDA has this meaning. State names themselves cannot be unique.
For words , introduce the Myhill-Nerode equivalenceIt is an equivalence relation, and appending the same letter to equivalent words preserves it: a suffix after is the suffix after . Since is a regular language, take any recognizing deterministic finite automaton. Words reaching the same state are equivalent, since every further suffix gives the same computation. Thus has finite index.
The canonical residual automaton has one state for each class, initial state , transition , and accepting states those with . These choices are well-defined by Myhill-Nerode equivalence. Induction on the input length shows that reading reaches , so the deterministic finite automaton recognizes , and all its states are accessible states of a deterministic finite automaton. The same state can be described by the left quotient of a formal languageTwo states are different precisely when some suffix distinguishes their acceptance behavior.
Every recognizing deterministic finite automaton has at least as many states as there are classes: pick a representative from each class; two different representatives cannot reach the same state. The canonical residual automaton attains this bound, and therefore is a minimal deterministic finite automaton.
For uniqueness, let be any minimal deterministic finite automaton. All its states are accessible, since removing inaccessible states leaves a complete recognizing deterministic finite automaton with fewer states. Map a state reached by to . This is well-defined because two words reaching the same state are equivalent. It is surjective because every class has a representative. Both sets have the minimal number of states, so it is a bijection. It preserves the initial state and transitions by construction, and preserves accepting states by taking the empty word as the suffix. This is the required isomorphism with the canonical residual automaton, provingThe empty word is included throughout, and empty or universal regular languages have the corresponding one-state complete deterministic finite automata.
Yes: regular languages are closed under the shuffle of formal languages. The construction must allow letters common to both alphabets to be assigned to either input word.
Take complete deterministic finite automata recognizing . Construct a nondeterministic finite automaton on over . Its initial state is and its accepting states form . On a letter , its possible moves from areBoth moves are allowed when belongs to both alphabets. They may coincide; that causes no difficulty.
For every run, record whether each move updated the first or the second coordinate. The letters assigned to each coordinate, in their original order, form two words . The final coordinate states are exactly the states reached by reading in . Thus an accepting run expresses the input as an interleaving of a word of and a word of .
Conversely, given such an interleaving, assign each input position to the word from which it came. The corresponding choices of transitions form a run ending in . This proves equality between the recognized formal language and the shuffle of formal languages, in both directions. No assumption of disjoint alphabets is needed. If one contributing word is the empty word, no move need update that coordinate; the initial pair is accepting exactly when both empty words are accepted.
Apply the powerset construction to this nondeterministic finite automaton to obtain a deterministic finite automaton. In particular,
Every countable structure in a countable first-order language has a Scott sentence whose countable models are precisely its isomorphic copies. In particular two countable structures with the same countable infinitary logic sentences are isomorphic. Countability of both structures is essential to the back-and-forth conclusion; the sentence need not exclude uncountable models.
Let be a nonempty countable structure in a countable first-order language. The countable infinitary logic permits countable logical conjunctions and logical disjunctions, but only finite strings of quantifiers and finitely many free variables in each formula. We construct a Scott formula for every finite tuple from and every countable ordinal .
At stage zero, let be the conjunction of all atomic formulas true of and the negations of all atomic formulas false of . Include atomic formulas involving arbitrary terms and constants, not just relation symbols applied directly to variables. There are only countably many such formulas. This complete atomic description ensures that matching tuples determine a partial isomorphism of structures.
At successors putAt a nonzero limit ordinal , put . All these are formulas of countable infinitary logic: each indexing set is countable, and the free variables are only the fixed finite tuple. Rename bound variables when necessary. Transfinite induction also shows .
For tuples of the same length within , define by . Induction identifies this with the usual symmetric back-and-forth method equivalence: the tuples have the same atomic description at stage zero, and at a successor every one-element extension on either side has a matching extension at the previous stage. Thus these are decreasing equivalence relations, simultaneously for every finite tuple length.
There are only countably many pairs of finite tuples in . A pair can cease to be equivalent at most once. The supremum of the first separation stages of all pairs that separate below is a countable ordinal. Choose a countable at least that supremum. No pair can first separate at , soThis justifies stabilization without assuming that all tuples stabilize at one predetermined finite stage.
Now form the following Scott sentence, where the case has no displayed variables or quantifiers:It is a sentence of countable infinitary logic, because the family of all finite tuples is countable. The stabilization above and the truth of show .
Suppose a countable structure satisfies . Start with the empty matching tuples, and maintain . The corresponding conjunct of upgrades this to . The existential conjuncts extend the match by any specified element of . The universal-disjunction conjunct extends it by any specified element of . The atomic formula information makes a new element on one side match a new element on the other, and makes repeated elements agree with their earlier matches.
Enumerate both structures and alternate these two extension steps, including the least element not yet covered at each step. The union is a bijection preserving and reflecting every atomic formula, hence an isomorphism; for function symbols, eventually include both a tuple and the value of its function term to see explicitly that the function is preserved. For finite structures the same construction stops when both are covered. Conversely every isomorphic copy of satisfies , since isomorphisms preserve formulas of countable infinitary logic by induction on their construction. ThereforeIf countable have the same sentences, satisfies this Scott sentence of and is isomorphic to . This proves Scott isomorphism theorem.
Yes. There is a computable isomorphism, obtained by an effective back-and-forth construction. Decidability of the two orders makes the usual existence argument into an algorithm.
Maintain a finite order-preserving partial isomorphism of structures from to , starting with the empty map. At a forth step, take the least ordinary natural number outside its domain. Look at the finitely many mapped elements below and above in . Their images impose an open interval in : it lies above all the lower images and below all the upper images, with a missing bound interpreted as an unbounded side.
This interval contains a fresh element. If both bounds exist they are ordered correctly by the induction hypothesis; density supplies an element strictly between them. If there is just one bound, the absence of endpoints supplies an element beyond it; if there are no bounds, choose any element. Density and the absence of endpoints moreover give infinitely many points in every such open interval, so finitely many already used images can always be avoided.
Enumerate in the ordinary presentation order, test whether is unused and satisfies every required inequality, and choose the first successful candidate. All tests are decidable, and the existence argument proves termination. Extend by .
At a back step, take the least natural number outside the range, interchange the roles of and , and carry out exactly the same search for a fresh preimage. Alternate forth and back steps. Every stage is an effective terminating finite computation, and every stage remains an order-preserving partial isomorphism of structures.
Let . The least-unused scheduling puts every element of into the domain and every element of into the range. For example, after forth steps, all ordinary presentation numbers at most have been included, since each step removes the least missing one. Thus is a bijection preserving and reflecting the orders. To compute , simulate the construction until appears in its domain; this terminates. The corresponding range search computes its inverse. HenceThe searches use the decidable presentations, rather than a possibly ineffective choice of points in an abstract dense linear order without endpoints.
Write and . The displayed formula is . A proof of logical implication may use its temporary assumption more than once; this is ordinary natural deduction, not a linear proof system.
Assume , then , then , then . The identity weakening rule derives from the hypotheses and . Discharging by the implication introduction rule gives . Applying by the implication elimination rule gives . Discharge to obtain . Applying gives an ; discharge to obtain a ; apply once more to obtain , and finally discharge .
Here is the complete decorated natural deduction derivation, split at its intermediate conclusion to keep the tree readable. Superscript labels mark which assumption occurrences are discharged; both occurrences labelled are discharged together.To avoid an excessively wide final tree, continue the same derivation as follows, using the right-hand derived premise above:followed byThus the concise lambda term, with bound-variable types determined by the displayed tree, isUnder the Curry-Howard correspondence, implication introduction rules correspond to lambda abstractions, implication elimination rules to applications, and the identity weakening rule retains the first term while allowing an unused second hypothesis. No other inference rule or classical axiom is required.
A well-quasi-ordering is a reflexive transitive relation for which every infinite sequence has with . A bad sequence has no such pair. The labelled version of Kruskal's tree theorem says that finite rooted trees labelled in any well-quasi-ordering are themselves well-quasi-ordered by label-monotone tree embedding.
More explicitly, an embedding is an injective map of vertices preserving lowest common ancestors, and satisfying at every vertex. The root need not map to the host root. This is a homeomorphic embedding of a rooted tree: an edge can map to a longer path, but distinct branches must separate at the image of their common ancestor. We shall prove the stronger version in which every vertex's children are linearly ordered and embeddings respect that ordering. Forgetting the child order gives the stated result for unordered rooted trees.
We first establish the two well-quasi-ordering facts used in the proof. Every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. Indeed, color an index pair according to whether . The infinite two-color Ramsey theorem gives a homogeneous infinite set; the negative color would be a bad sequence, so the positive color gives the required subsequence. It follows that the componentwise product of two well-quasi-orderings is a well-quasi-ordering: first extract a nondecreasing subsequence in one coordinate, then find a good pair in the other.
Next prove Higman lemma: finite words over a well-quasi-ordering , ordered by subsequence embedding with coordinatewise increase of letters, are a well-quasi-ordering. Suppose not, and choose a minimal bad sequence by making the length of minimal among all choices admitting an infinite bad continuation of the already fixed prefix. No word is the empty word, since that embeds in every later word. Write with . Extract indices for which . ConsiderIt cannot be a bad sequence, since its first replacement is shorter than the minimal choice . But a good pair within the original prefix is impossible. A prefix word embedding into would embed into , contradicting the original bad sequence. And embedding into would, after appending the ordered last letters, embed into , also impossible. This contradiction proves Higman lemma, including words of arbitrary finite length.
Now suppose there is a bad sequence of finite ordered labelled rooted trees. Choose a minimal bad sequence by minimizing the number of vertices of , subject to the fixed prefix having an infinite bad continuation. Existence of a least possible size uses ordinary well-ordering of the natural numbers; after selecting such a tree retain a bad continuation to make the next choice.
Let be the collection of all proper rooted subtrees of all , with inherited labels and child ordering. These are the subtrees rooted at vertices other than the root, and each embeds into its containing tree. We claim is a well-quasi-ordering under the same label-monotone tree embedding.
Otherwise choose a bad sequence from , and choose for each a containing tree . The indices are unbounded in every tail: finitely many containing trees have only finitely many rooted subtrees, and an infinite bad sequence cannot repeatedly use one of these, since it embeds into itself. Passing to a subsequence, arrange . The spliced sequenceis bad. A good pair within either piece is already excluded. A comparison , where , would compose with to give , contradicting the original bad sequence. But is smaller than , contradicting the minimal choice at that position. This proves the claim about .
Describe by its root label and its finite ordered list of child subtrees. Every entry of lies in . By Higman lemma, is a well-quasi-ordering; hence so is . There exist with and an increasing injection matching the child subtrees in to child subtrees in , each by an embedding. Map root to root and combine these child embeddings. Different matched children lie in different target branches, so their paths meet exactly at the target root; within each branch the chosen embedding already preserves lowest common ancestors. The resulting map is a label-monotone tree embedding , a contradiction. ThereforeThe empty labelled tree, if included by convention, embeds into every tree and causes no exception. A common stronger formulation requires the source root to map to the target root. It also follows: the theorem just proved makes all labelled child subtrees a well-quasi-ordering, and the product then provides a good pair with roots explicitly matched, by the same final assembly. Internal child roots may map further down their matched branches. This must not be confused with edge-to-edge embedding, for which the theorem is false in general.
As printed, yes: the relation is universal. The original PDF puts the existentially quantified element in the same subset as the universally quantified element; this is not an OCR substitution. For each element of that subset, choose the element itself as witness, using reflexivity of the underlying well-quasi-ordering. For an empty subset the condition is vacuous. The truth value therefore never depends on the proposed target subset. On the power set this is a reflexive transitive relation, and every two terms of any infinite sequence are related:A well-quasi-ordering need not be antisymmetric, so universal comparability is allowed.
If the existential element is instead intended to belong to the target subset, the natural relation is the Hoare domination preorderFor arbitrary subsets the answer to that corrected question is no. Here is a complete counterexample, the Rado order. TakeThis is a partial order. Reflexivity is immediate. For transitivity, two same-row comparisons compose ordinarily. If the first comparison crosses rows and the second stays in its row, its target first coordinate is unchanged, so the cross-row inequality persists. If the first stays in its row and the second crosses, use ; if both cross, use . Antisymmetry follows because comparisons across distinct rows in both directions would require .
The Rado order is a well-quasi-ordering. Given an infinite sequence , if a first coordinate repeats infinitely often, its corresponding natural-number second coordinates have a nondecreasing pair, giving a same-row comparison. Otherwise each first coordinate occurs only finitely often, so the first coordinates in every tail are unbounded. In particular some later exceeds , giving .
For each , take the infinite row . For distinct , choose . The element is below no member of , since its first coordinate is different and fails. Thus for every pair of distinct indices. These subsets form an infinite antichain, so the Hoare domination preorder on is not a well-quasi-ordering.
If only finite subsets were intended, the answer changes again: the finite-subset lifting of a well-quasi-order is a well-quasi-ordering. Enumerate each finite subset as a finite word. Higman lemma gives an earlier word embedding into a later one with every letter increased, which witnesses Hoare domination preorder comparison of the underlying subsets. The PDF specifies no finiteness restriction, so this observation supplements rather than replaces the literal answer and the arbitrary-subset counterexample.
Articles by others on the same topic
There are currently no matching articles.