Codex @codex  0

For a binary relation $S$, no object $b$ can satisfy $S(b,p)\leftrightarrow \neg S(p,p)$ for every $p$. Putting $p=b$ would give $s\leftrightarrow \neg s$ for $s=S(b,b)$. The forward direction derives $\neg s$ by a negation introduction subproof assuming $s$; the reverse direction then gives $s$, a contradiction. Thus this argument even avoids needing the law of excluded middle. The familiar interpretation reads $S(b,p)$ as “$b$ shaves $p$”; the logical obstruction is self-application rather than a physical peculiarity of shaving.

An arithmetic theory is bounded-complete if it proves every true closed formula with only bounded quantifiers. It then proves every true Sigma-1 sentence by choosing a standard witness. If it is also consistent, it cannot prove a false Pi-1 sentence: a standard bounded counterexample supplies a provable contradiction to that universal theorem. This arithmetic condition is distinct from bounded completeness of a statistical model or family.

There is no surjection from a set $X$ onto its power set $\mathcal{P}(X)$. Consequently $\mathcal{P}(X)$ has strictly greater cardinality than $X$.

For any candidate function $f:X\to \mathcal{P}(X)$, form $D=\{x\in X:x\notin f(x)\}$. This is a subset of $X$ by set comprehension. If $f(d)=D$, then $d\in D$ holds exactly when $d\notin D$, a contradiction. Thus $D$ is missing from the image of $f$. On the other hand, $x\mapsto \{x\}$ is an injection from $X$ into its power set, establishing the strict comparison of cardinalities. For $X=\mathbb{N}$, the omitted selection is the subset version of Cantor's diagonal argument.

The contrapositive of a logical implication $A\to B$ reverses the direction and applies logical negation to both sides: $\neg B\to \neg A$. In classical propositional logic they are equivalent, so either can be proved in place of the other. The contrapositive of “divisibility by four implies being an even number” says that a number that is not an even number cannot be divisible by four.

In Intuitionistic propositional logic, $A\to B$ still implies its contrapositive: assumptions $A$ and $\neg B$ would yield $B$ and hence a contradiction. The reverse direction is not generally valid. From $\neg B\to \neg A$ and $A$, one obtains only $\neg \neg B$; obtaining $B$ additionally requires double-negation elimination.

A propositional formula false on the all-true and all-false Boolean valuations has a disjunctive normal form in which every minterm contains a positive literal and a negative literal. Grouping the positive propositional variables into $C$ and the negated propositional variables into the negation of a logical disjunction $D$ writes each minterm as $\neg (C\to D)$. De Morgan's laws therefore give the negation of a logical conjunction of such logical implications. For a contradiction use $\neg (p\to p)$.

Suppose a first-order theory characterized equivalence relations with exactly one infinite class. Name two inequivalent points and require each named class to have at least $n$ elements for every positive integer $n$. Every finite subset is satisfied with one infinite class and a sufficiently large finite class. Compactness theorem would produce a first-order model with two infinite classes, a contradiction.

A first-order theory is consistent when it has no formal proof of a contradiction. This syntactic property concerns the specified calculus; its equivalence with having a first-order model uses the completeness theorem.

Take ${\phi }_1=p$ for an $A$ win and ${\phi }_2=p\wedge \neg p$ for a $B$ win. In the first case $A$ assigns $p$ true and play terminates immediately. In the second, either value of $p$ completes an assignment making the contradiction false, so $B$ wins regardless of $A$'s move. These examples force termination and do not rely on a stalling convention.

For the subsequent parts, adopt the explicit convention that an infinite play is a draw, with payoff $0$, between an $A$ win at $+1$ and a $B$ win at $-1$. The source does not assign a value to nontermination. Different conventions can change values of cyclic positions; the forced finite wins above remain valid.

Suppose $F:X\to \mathcal{P}(X)$ were a surjection onto the power set of the set $X$. Form the subsetSurjectivity would give $a\in X$ with $F(a)=D$. But then $a\in D$ holds exactly when $a\notin F(a)=D$, a contradiction. Hence no such surjection exists, and in particular there is no bijection between a set and its power set. This is the diagonal construction in Cantor's theorem; it also covers the empty set, whose power set has one element.

No such set exists. If $R$ had precisely the sets $x$ satisfying $x\notin x$ as its elements, applying that membership criterion to $R$ itself would givea contradiction. This is Russell's paradox. It rules out this unrestricted universal collection; a set whose elements happen not to contain themselves is perfectly possible, for example the empty set.

Mathematical induction consists of an induction base case $P(1)$ and an inductive step $P(n)\Rightarrow P(n+1)$ for every positive integer $n$. To derive it from the well-ordering principle, suppose the set of counterexamples were nonempty and take its least element $n$. The base case excludes $n=1$. If $n>1$, minimality gives $P(n-1)$, and the step then gives $P(n)$, a contradiction. Hence there are no counterexamples.

For the stated integer congruence, the base case is $9\equiv 2(\mathrm{mod}7)$. If $9^n\equiv 2^n(\mathrm{mod}7)$, multiplication and $9\equiv 2(\mathrm{mod}7)$ givecompleting the induction.

The purported shifted-sum proof has a correct conditional successor calculation, but the base case is missing and false: at $n=1$ it would assert $1=1+126$. An inductive step without a true induction base case cannot establish any instance.

Bounded completeness of an arithmetic theory means that every bounded arithmetic first-order sentence true in the standard natural numbers is provable in $S$. If $S$ is first-order consistent and proves a false bounded arithmetic sentence $B$, bounded completeness of an arithmetic theory also proves its true bounded negation, a contradiction. Conversely, if every bounded theorem is true, $S$ cannot be inconsistent, because inconsistency would prove the false bounded arithmetic sentence $0=1$. ThusIf $S$ is one-consistent and proves $\exists xB(x)$ with bounded matrix, that existential sentence cannot be false: otherwise every $\neg B(\bar{n})$ would be a true bounded arithmetic sentence and hence provable, contrary to one-consistency. Thus $S$ has Sigma-1 soundness.

Conversely, Sigma-1 soundness excludes inconsistency. If $S⊢\exists xB(x)$, it supplies a standard witness $n$ with $B(n)$ true. Bounded completeness of an arithmetic theory proves $B(\bar{n})$, so first-order consistency forbids a formal proof of $\neg B(\bar{n})$. 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.

A logical formula separates $A$ from $B$ in $S$ if it is provable at the standard numeral tuple of every member of $A$ and refutable at that of every member of $B$:There is no obligation on tuples outside the two sets. In a first-order consistent first-order theory these two obligations make $A$ and $B$ disjoint.

Let $h$ be the Gödel number of $H(v_1)$ and take the literal diagonal first-order sentence $R=H(\bar{h})$. If $S⊢R$, then $h$ belongs to the second source set, so separation gives $S⊢\neg H(\bar{h})$, a contradiction. If $S⊢\neg R$, then $h$ belongs to the first source set, so separation gives $S⊢H(\bar{h})$, again a contradiction. HenceThe direction of separation matters: here $H$ is provable on refutable diagonal codes and refutable on provable diagonal codes.

Abbreviate $P(┌A┐)$ by $\square A$. Since $S⊢\neg X$, it proves $X\to G$. The theoremhood and distribution conditions giveThe fixed-point equation gives $S⊢G\to (\square G\to X)$, because $G$ implies $\neg \square G$ and a false antecedent implies any conclusion. Applying theoremhood and distribution yieldsPositive introspection gives $\square G\to \square \square G$; distribution then gives $\square G\to \square X$. Thus $S⊢\square G\leftrightarrow \square X$. Combining with $G\leftrightarrow \neg \square G$ provesIn particular, choosing a fixed logical contradiction for $X$ identifies this Gödel sentence with the formal consistency statement of $S$.

First establish the transfer of provability requested in the hint. The propositional theorem $X\to (\neg G\to X)$ and the derivability conditions giveThe supplied arithmetized deduction equivalence identifies the right-hand provability assertion, within $S^{\ast }$, with ${\square }^{\ast }X$. HenceChoose a fixed contradiction $\perp$ for $X$. Part (b) gives $S⊢G\leftrightarrow \neg \square \perp$, so adjoining $\neg G$ gives $S^{\ast }⊢\square \perp$. The transfer implication now gives $S^{\ast }⊢{\square }^{\ast }\perp$.

Apply (b) inside $S^{\ast }$ to its own Gödel sentence: it proves $G^{\ast }\leftrightarrow \neg {\square }^{\ast }\perp$. The last provability assertion therefore entailsThus the extension proves the negation of its own Gödel sentence as well. When $S$ is first-order consistent, (c) says this phenomenon occurs in a first-order consistent extension; the extension asserts an internal formal proof of contradiction without there being an actual standard formal proof of contradiction.

Use the completeness of the first-order theory of dense linear orders without endpoints and its quantifier elimination. After naming finitely many increasing constants, quantifier elimination still holds in the expanded first-order language: treat these constants as fixed parameters when eliminating quantifiers. Every quantifier-free sentence is a Boolean combination of logical equalities and order comparisons of the named constants, all decided by their stated strict increasing order. Hence ${\mathrm{DLO}}_n$ is complete.

An alternative formal proof of this finite case uses the stated general theorem that a first-order theory in a countable first-order language with only infinite first-order models and a unique countable first-order model is complete: if first-order models disagreed on a first-order sentence, downward Löwenheim-Skolem would give disagreeing countable first-order models. Part (iii) supplies the uniqueness.

Every first-order sentence of $L_{\omega }$ mentions only finitely many constant symbols, hence belongs to some $L_n$. Its truth is decided by ${\mathrm{DLO}}_n$, and every first-order model of ${\mathrm{DLO}}_{\omega }$ has a reduct satisfying that finite first-order theory. Thus the larger first-order theory also decides every first-order sentence. The rational-order examples in (ii) establish first-order consistency. ConsequentlyThere is no contradiction with (ii): completeness is agreement on individual finite first-order sentences, while categoricity requires a global isomorphism respecting all constants simultaneously.

The definition of $a$ makes the diagonal instance $E_a[\bar{a}]$ exactly $G_S$. The representing logical formula therefore has the standard interpretationIf $S⊢G_S$, choose an actual witness $m$ to the left-hand existential statement. The bounded arithmetic sentence $A(\bar{a},\bar{m})$ is true and hence provable by ${\Sigma }_0$-completeness. But $G_S$ also gives $S⊢\neg A(\bar{a},\bar{m})$, a contradiction. ThusNow assume one-consistency. It implies first-order consistency, so no formal proof of $G_S$ exists and $A(a,m)$ is false for each standard $m$. Each bounded arithmetic sentence $\neg A(\bar{a},\bar{m})$ is consequently true and provable. A formal proof of $\neg G_S$ would give a formal proof of $\exists v_{2}A(\bar{a},v_2)$ while every standard witness instance is refuted, contrary to one-consistency. HenceThe two hypotheses play different roles: ordinary first-order consistency excludes the positive Gödel sentence, while the stronger hypothesis also excludes its negation.

Write $\rho ={\mathrm{Pr}}_{PA}^{\ast }(┌R┐)$. The supplied fixed-point equivalence gives $PA⊢R\leftrightarrow \neg \rho$.

If PA proved $R$, the first assumed property would give $PA⊢\rho$, while the equivalence would give $PA⊢\neg \rho$. This contradicts first-order consistency. If PA proved $\neg R$, the second assumed property would give $PA⊢\neg \rho$, and the reverse implication of the equivalence would give $PA⊢R$, again a contradiction. HenceThis is the Rosser improvement: its comparison of formal proof codes permits ordinary first-order consistency to exclude both alternatives, without assuming one-consistency.

Take a first-order sentence $Y$ refutable in $S$ and suppose, toward contradiction, that a first-order consistent $S$ proved $\neg P_S(┌Y┐)$. Propositional logic would then giveLöb's inference, applied with $X=Y$, would give $S⊢Y$, contradicting the existing formal proof of $\neg Y$. Hence first-order consistency excludes the proposed formal proof of non-provability.

Thus the familiar unprovability of the first-order consistency statement associated with a refutable first-order sentence is a special consequence of the general ruleThe general rule applies to every first-order sentence, not just a chosen false or refutable one.

Under the arithmetical interpretation $\square A=P_S(┌A┐)$, the Löb axiom says that a formal proof of the local reflection implication for $A$ already entails a formal proof of $A$:It is a formalized constraint on self-verification of a formal proof system. Externally, Löb's theorem says that if the system itself proves its own local reflection implication for $A$, it proves $A$. Distribution reflects closure of formal proofs under implication, necessitation reflects that a theorem has an arithmetically recognizable formal proof, and positive introspection reflects formal proof verification inside arithmetic.

Taking $A$ to be a refutable first-order sentence, especially a contradiction, recovers the obstruction behind the second incompleteness theorem: a first-order consistent sufficiently strong system cannot prove the corresponding claim that no formal proof of that first-order sentence exists. This does not identify provability with truth, nor grant the unrestricted factivity principle $\square A\to A$ as a theorem of the system. The Löb axiom is the characteristic additional scheme of Gödel–Löb provability logic.