Use the numeralwise enumeration in arithmetic convention in the first-order theory: membership supplies a standard stage with a provable enumerating instance, while nonmembership makes every standard-stage instance refutable. Put . By the definition of , the diagonal instance is exactly .
If , then . Numeralwise enumeration in arithmetic supplies a natural number such that . But universal instantiation of gives . This contradicts first-order consistency. ThereforeThis uses the formal proof obligations in numeralwise enumeration in arithmetic in , rather than merely the external assertion that a logical formula has a particular complexity.
One-consistency says that no bounded arithmetic formula has a provable existential closure while each of its standard numeral instances is refutable. It implies first-order consistency, since an inconsistent classical first-order theory proves every logical formula.
If is one-consistent, (i) gives , so . Numeralwise enumeration in arithmetic therefore givesIf , classical logic gives . The matrix is bounded, and the preceding displayed derivations refute every standard instance. This violates one-consistency. ConsequentlyTogether with (i), this yields undecidability of this first-order sentence under the stronger hypothesis, without asserting that ordinary first-order consistency alone suffices for its negative half.
Bounded completeness of an arithmetic theory means that every bounded arithmetic first-order sentence true in the standard natural numbers is provable in . If is first-order consistent and proves a false bounded arithmetic sentence , bounded completeness of an arithmetic theory also proves its true bounded negation, a contradiction. Conversely, if every bounded theorem is true, cannot be inconsistent, because inconsistency would prove the false bounded arithmetic sentence . ThusIf is one-consistent and proves with bounded matrix, that existential sentence cannot be false: otherwise every would be a true bounded arithmetic sentence and hence provable, contrary to one-consistency. Thus has Sigma-1 soundness.
Conversely, Sigma-1 soundness excludes inconsistency. If , it supplies a standard witness with true. Bounded completeness of an arithmetic theory proves , so first-order consistency forbids a formal proof of . Hence there cannot simultaneously be refutations of all standard instances. ThereforeFinite blocks of existential logical variables are treated as finite tuples of witnesses, with the same argument.
Omega-consistency forbids a logical formula of any complexity for which and for every standard . The difference from one-consistency is that the matrix is unrestricted. It implies first-order consistency.
For a complete first-order consistent classical first-order theory, theorem membership obeys the ordinary Boolean truth tables. For example, it proves a conjunction exactly when it proves both conjuncts; completeness and first-order consistency also make theoremhood of a negation the complement of theoremhood of the first-order sentence. Omega-consistency additionally gives the witness propertyThe reverse implication is existential introduction. For the forward implication, if no standard instance were provable, completeness would give a formal proof of each negated instance, violating omega-consistency. This works also after replacing additional free variables by numerals.
Now induct on logical formulas with their remaining free variables replaced by standard numerals. At the atomic level, the equivalence between theoremhood and standard truth follows from bounded completeness of an arithmetic theory and bounded soundness of an arithmetic theory from (b). The Boolean steps use the truth-table facts just proved. The existential step uses the witness property and the induction hypothesis on its matrix; universal quantification follows by negation. Hencefor every first-order sentence . Completeness ensures it decides each first-order sentence, and this equivalence ensures every decision is correct.
Start with the supplied bounded-complete, one-consistent first-order theory proving a false first-order sentence . Replace it by its deductive closure, which preserves these properties and contains . Enumerate the arithmetic first-order sentences as . Recursively extend the current first-order theory by either or , choosing an extension which remains one-consistent as permitted by the supplied lemma, and then take its deductive closure. Call the resulting increasing sequence , with the initial first-order theory, and put .
Every stage is still bounded-complete. By (b), every stage has Sigma-1 soundness. If proved a false Sigma-1 first-order sentence, the finite formal proof would use assumptions from one stage , contradicting its Sigma-1 soundness. Thus has Sigma-1 soundness and is bounded-complete, so (b) makes it one-consistent.
This soundness of an arithmetic theory argument is essential: the definition of one-consistency involves infinitely many standard refutations, so it would be insufficient merely to say that a violation has a finite formal proof. What has a finite formal proof is the false existential sentence, and bounded completeness of an arithmetic theory is what turns one-consistency into the needed soundness of an arithmetic theory condition.
The union is deductively closed because each formal proof has finitely many assumptions. It contains either or for every first-order sentence, by the numeralwise enumeration in arithmetic, and contains the false first-order sentence . If it were omega-consistent, (c) would make it correct on all first-order sentences, contradicting . We have therefore constructedOmega-consistency always implies one-consistency by restricting its matrices. This counterexample proves that the converse is strictly false.
Articles by others on the same topic
There are currently no matching articles.