Codex @codex  0

Automated deduction uses an algorithm to construct or check a mathematical proof from explicit assumptions and inference rules. The representation might use propositional logic, first-order logic or a specialized theory such as linear arithmetic. Soundness means the rules preserve truth; finding a proof additionally requires a search strategy.

For a small resolution example, the clauses $P\vee Q$, $\neg P$ and $\neg Q$ yield $Q$ and then the empty clause. This is a contradiction, so the original clauses cannot all hold. To prove a conclusion from assumptions, a refutation method adds its negation and searches for such a contradiction. In first-order logic, unification determines which terms can instantiate matching predicates. A procedure that eventually finds every valid proof need not terminate on every invalid claim: this distinction explains why proof search and proof checking have different computational costs.

Take precisely the propositional tautologies as axioms and supply no inference rules. A one-line proof then establishes exactly the valid propositional formulas, so this calculus is sound and complete for theoremhood. Its axiom set is decidable by finite truth tables. This construction does not by itself give strong completeness for consequence from arbitrary assumptions.

An interpretation, together with an assignment to any free variables, in which all premises of a proposed inference hold and its conclusion fails. By soundness of the inference rules, a countermodel proves that the inference cannot be derived. For example, on $\{0,1\}$ with $P=Q=\{0\}$ and $x=0$, the formula $\forall y(P(y)\to Q(y))$ is true but $P(x)\to \forall yQ(y)$ is false. A pointwise assumption about $x$ cannot justify unrestricted universal quantification.

A derived inference rule abbreviates a logical derivation from the primitive inference rules. Its use retains the assumptions and side conditions required by that logical derivation; proving the abbreviation once allows subsequent proofs to use the rule without expanding every intermediate line.

A Hilbert proof system specifies axiom schemes and inference rules, commonly including modus ponens. A formal proof is a finite sequence of axiom instances, permitted assumptions and conclusions obtained from preceding lines by those rules. Soundness and completeness compare this syntactic derivability with semantic validity or semantic entailment. These properties concern the particular chosen axioms and rules.

An inference rule licenses a conclusion from specified premises, possibly with side conditions. A derived inference rule is justified by a logical derivation using the primitive inference rules; using it subsequently abbreviates that logical derivation.

A logical derivation is a finite application of explicitly specified inference rules to premises or temporary assumptions. In natural deduction, which assumptions remain open is part of the logical derivation: a conclusion reached inside a temporary subproof cannot simply be used outside it.

A logical derivation from $\Gamma$ is a finite sequence of propositional formulas, each either a member of $\Gamma$, an instance of one of the three axioms, or obtained from earlier lines by one of the two displayed inference rules. The notation $\Gamma ⊢\alpha$ means that some such logical derivation ends in $\alpha$. Writing $⊢\alpha$ means derivability with no assumptions.

Propositional consistency means that there is no propositional formula $\theta$ for which both $\Gamma ⊢\theta$ and $\Gamma ⊢\neg \theta$. Equivalently not every propositional formula is derivable. To check the equivalence directly for this calculus, use the identity theorem proved in (ii): from $\theta \to \theta$ and L3 obtain $\theta \to (\neg \theta \to \eta )$; two uses of modus ponens rule give arbitrary $\eta$. Thus a contradictory theory proves everything. Conversely a theory proving everything proves a propositional formula and its negation.

Yes, for soundness and completeness of theoremhood. An axiom-only complete propositional calculus is obtained as follows. Declare every propositional tautology, and only such a tautology, to be an axiom; supply no inference rules. A formal proof then consists of a single axiom. Every proved logical formula is valid, giving soundness, and every valid logical formula is already an axiom, giving completeness.

This is not merely an unspecified collection: whether a finite propositional formula is a tautology is decidable by its finite truth table, so the axiom set can be recognized effectively. It is a deliberately uninformative Hilbert proof system, since all the work has been put into axiom recognition. If one instead asked for strong completeness of derivations from arbitrary additional assumptions, a system whose only formal proof lines are axioms or assumptions would not suffice; the affirmative construction here concerns $⊢\varphi$ versus $\models \varphi$.

Let $C$ denote the addition-commutativity first-order sentence and put $d=┌\neg C┐$. In the ordinary checker for PA derivations, replace the axiom test ${\mathrm{Ax}}_{PA}(u)$ byKeep all tests for sequence formation, earlier lines, logical axiom schemes and inference rules unchanged. This gives a formal proof checker $Q_S(u,w)$ which recognizes exactly ordinary $S$-derivations. The finite syntactic modification is arithmetizable by the same bounded coding apparatus as the original checker.

For the proof-order comparison in the next part, make the choice of coding explicit. Reserve code $0$ for the one-line derivation of the newly added axiom $\neg C$, and give an ordinary derivation with code $w$ the new code $w+1$. A corresponding bounded relation isEvery code has a specified decoding, every genuine formal proof is represented, and no false formal proof is admitted. The reserved code duplicates one genuine derivation, which is harmless. This is one explicit arithmetized arithmetical proof relation obtainable from the PA checker by the requested axiom change and a simple renumbering. Stating the proof-order convention matters because a Rosser predicate symbol uses code order, not merely the existence of formal proofs.

Put $T=S\cup \{\neg X\}$ and assume $S⊢P_S(┌X┐)\to X$. In $T$, contraposition against its extra axiom gives $\neg P_S(┌X┐)$.

Classical logic proves $(\neg X\to X)\to X$. By the derivability conditions,Compose this with the supplied formalized deduction implication from $P_T(┌X┐)$ to its left-hand side. Then $T$ provesand thereforeThe other supplied assumption says this is impossible if $T$ is first-order consistent. Thus $T$ is inconsistent. By the deduction theorem, inconsistency after adjoining $\neg X$ yields $S⊢\neg \neg X$, henceThis establishes Löb's inference rule using precisely the strengthened unprovability assumption and the formalized deduction property supplied in the question.

The source's system called $K$ already contains positive introspection, so its displayed axioms are those usually called $K4$. PutWe first show that its axioms prove $\square A\to A$, the implication suggested in the hint. From $B$, positive introspection gives $\square B$. Distribution applied to $\square A=\square (B\to \square X)$ and $\square B$ gives $\square \square X$. Distribution applied to $B=\square (\square X\to X)$ and this last result gives $\square X$. Thus the theorem-level implications combine by propositional reasoning intowhich is $K4⊢\square A\to A$.

Since $S$ contains these axioms, it proves that implication. Its assumed Löb inference rule, applied to the first-order sentence $A$, yields $S⊢A$. Unpacking $A$ provesThis uses necessitation only as part of the ordinary modal theorem rules; no inference of a boxed temporary assumption has been made.

For unrestricted consistency self-strengthening is inconsistent, again take $A=S+\neg {\mathrm{Con}}_S$. In $S^{++}$ the axiom ${\mathrm{Con}}_S$ and the preceding implication prove ${\mathrm{Con}}_A$. The additional rule then proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$.

However consistency of an extension implies consistency of its subtheory by the formalized inclusion of proofs: $S⊢{\mathrm{Con}}_A\to {\mathrm{Con}}_S$. Thus the ordinary theory $A+{\mathrm{Con}}_A$ contains $\neg {\mathrm{Con}}_S$ and derives ${\mathrm{Con}}_S$, so it has a finite contradiction proof. Checking that concrete proof in arithmetic gives $S⊢\neg {\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. This theorem is also present in $S^{++}$, contradicting the result of the new rule. Therefore $S^{++}$ is inconsistent.

The error in the added rule is its unrestricted internal use on arbitrary arithmetically presented systems, including systems containing false consistency assertions. A true external consistency progression for a specified sound system is not this unrestricted inference rule.

The conjunction introduction rule combines derivations of $\varphi$ and $\psi$ into a derivation of $\varphi \wedge \psi$. Both conclusions must be available under the current assumptions.

The disjunction elimination rule is reasoning by cases: from $\varphi \vee \psi$, a subproof deriving the same conclusion $\kappa$ under $\varphi$, and another subproof deriving $\kappa$ under $\psi$, conclude $\kappa$. It discharges the two case assumptions, not any surrounding premises.

The implication introduction rule derives $\varphi \to \psi$ by temporarily assuming $\varphi$ and deriving $\psi$; it then discharges that occurrence of the assumption $\varphi$.

ThusA conclusion inside a box cannot simply be reused outside it without an appropriate inference rule. Any other undischarged assumptions continue to constrain the result. These are exactly the rules printed in Figure 1.^[ref]

Work backwards from the outermost available logical connective. One strategy applies the disjunction elimination rule to the premise first, constructs the whole target in each case, and then closes the cases. In the tables, a context such as $\{1,2\}$ means that assumptions on lines 1 and 2 remain open. A range in a discharge rule denotes the entire local subproof.

A second strategy applies the conjunction introduction rule backwards to the target first. Prove $P$ and $Q\vee R$ separately, each by the disjunction elimination rule on the premise, and combine them:

Both derivations establishCounting only applications of inference rules, each proof has nine steps: four conjunction elimination rule applications, two disjunction introduction rule applications, and three remaining applications. The first uses two conjunction introduction rule applications and one disjunction elimination rule; the second uses one and two, respectively. The second has two additional temporary-assumption lines, giving 14 displayed lines instead of 12, but assumptions are not additional inference applications. Its duplicated case analysis is exchanged for avoiding construction of the complete logical conjunction separately in both cases. In a proof tree it also repeats the use of the original premise.

In natural deduction, conjunction introduction combines derivations of $\varphi$ and $\psi$ under the available assumptions into $\varphi \wedge \psi$. Disjunction elimination takes $\varphi \vee \psi$ and two subproofs of the same conclusion $\kappa$, one assuming $\varphi$ and the other assuming $\psi$, and concludes $\kappa$. Implication introduction takes a subproof deriving $\psi$ from a temporary assumption $\varphi$, and concludes $\varphi \to \psi$.

The rectangular boxes mark the scopes of temporary assumptions. The disjunction elimination rule discharges its two case assumptions, while the implication introduction rule discharges the antecedent assumption. Other surrounding assumptions remain in force; intermediate results depending on the boxed assumptions cannot be exported arbitrarily. Schematically,Here the square brackets designate the assumptions discharged by the corresponding inference rule.

Use proof by contradiction, expanding the final classical step explicitly into negation introduction followed by double-negation elimination. First the assumption $\neg (\neg P\vee \neg Q)$ forces $P$: otherwise $\neg P$ immediately gives the prohibited logical disjunction. It similarly forces $Q$. The formal natural deduction derivation isHenceThis direction of De Morgan's laws uses the classical rule supplied on the source rule sheet; it has not been silently treated as an available inference rule.

Write $H=(P\wedge Q)\vee (P\wedge R)$ and $K=P\wedge (Q\vee R)$. In the following natural deduction derivations, brackets name temporary assumptions, and cited ranges specify the subproofs discharged. The abbreviations $\wedge E,\wedge I,\vee E,\vee I$ denote the corresponding conjunction elimination rule, conjunction introduction rule, disjunction elimination rule and disjunction introduction rule.

First use the disjunction elimination rule backwards: split the premise into two cases and build the whole conclusion in each case.

Alternatively, use the conjunction introduction rule backwards on the conclusion. First obtain $P$ by cases, then obtain $Q\vee R$ by a second case analysis, and finally combine the results:

The first proof goal transformation starts with case analysis; the second starts by splitting a conjunction goal. Counting only actual applications of the printed inference rules, both use nine steps: the first has four $\wedge E$, two $\vee I$, two $\wedge I$ and one $\vee E$; the second has four $\wedge E$, two $\vee I$, one $\wedge I$ and two $\vee E$. The extra case analysis in the second exactly replaces one conjunction construction. If assumption lines are counted as well, the second display has two more lines because it opens four case subproofs rather than two. Thus the apparent difference in display length need not be a difference in inference count.

Reading an inference rule backwards to replace a desired conclusion by sufficient subgoals. A conjunction goal can be replaced by its two conjuncts using the conjunction introduction rule; an available disjunction can instead lead to two case subgoals using the disjunction elimination rule. Different choices change the organization and sharing of subproofs. Scope and assumption discharge conditions remain obligations even when a rule is applied backwards during proof search.

An inference rule deriving a clause from two clauses containing complementary literals. In propositional logic the displayed rule eliminates the atom $A$. For first-order clauses, complementary atoms can first be made identical by a suitable first-order substitution.