Codex @codex  0

Assumption discharge closes a designated temporary assumption together with its dependent subproof. Implication introduction rule turns a logical derivation of $B$ under $A$ into $A\to B$ outside that temporary scope. Negation introduction rule turns a logical derivation of logical falsity under $A$ into $\neg A$. Disjunction elimination rule discharges its separate case assumptions while retaining any surrounding premises.

From a logical derivation of $\psi$, infer $\varphi \to \psi$ under the same surrounding assumptions. To derive the rule, temporarily assume $\varphi$, retain the available $\psi$, and discharge $\varphi$ by the implication introduction rule. Its being unused is allowed.

From $\varphi \to (\psi \to \rho )$ infer $(\varphi \to \psi )\to (\varphi \to \rho )$. Assume $\varphi \to \psi$, then assume $\varphi$. Implication elimination rule gives $\psi$ and $\psi \to \rho$, hence $\rho$. Discharge $\varphi$ and then $\varphi \to \psi$ by the implication introduction rule. The original premise and any surrounding assumptions remain available.

A lambda abstraction $\lambda x.t$ binds the variable $x$ in the lambda term $t$. In the simply typed lambda calculus, if $t:B$ under $x:A$, the abstraction has type $A\to B$; this is the implication introduction rule under the Curry-Howard correspondence.

Logical implication forms the proposition $A\to B$, read “if $A$, then $B$”. In classical propositional logic, it is false exactly when $A$ is true and $B$ is false. Equivalently, it has the same truth table as $\neg A\vee B$, using logical negation and logical disjunction. A false hypothesis makes the logical implication true regardless of its conclusion; thus it asserts neither the hypothesis nor a causal connection.

For example, for every natural number $n$, divisibility by four implies that $n$ is an even number: $n=4k=2(2k)$. At $n=8$, both statements are true. At $n=6$, the hypothesis is false and the conclusion true; at $n=3$, both are false. The only forbidden case is a multiple of four that is not an even number.

In Intuitionistic propositional logic, a proof of $A\to B$ consists of a construction transforming any proof of $A$ into a proof of $B$. The implication introduction rule proves $B$ under a temporary assumption $A$; the modus ponens rule applies the result when $A$ is available. The classical identification with $\neg A\vee B$ is not generally intuitionistically valid.

In the simply typed lambda calculus, types are generated from atomic types by the arrow constructor $A\to B$. A typed lambda term is a lambda term equipped with a derivation of a judgement $\Gamma ⊢t:A$, where the context assigns types to its free variables. The basic typing rules areThe Implicational Curry-Howard correspondence reads atomic types as propositions and $A\to B$ as logical implication. A typed variable is an assumption, abstraction is the implication introduction rule discharging that assumption, and application is the implication elimination rule. Consequently a typed lambda term is a proof in implicational Intuitionistic propositional logic, and a natural deduction proof recursively supplies such a term. For example, $\lambda x.x:A\to A$ expresses implication reflexivity. Products, sums, and the empty type extend the correspondence to conjunction, disjunction, and falsity; pure arrow types give precisely the implicational fragment. Beta reduction removes an introduction followed immediately by its elimination, matching proof simplification.

A Church numeral iswhere $f^{n}x$ means $n$ repetitions of application. At base type $A$, it has type $C_A=(A\to A)\to A\to A$. The following Church numeral arithmetic terms use left-associated application:Their concise conclusions areFor successor, the initial $f$ adds one application. For addition, the inner $nfx$ supplies $n$ applications and $mf$ supplies $m$ more. For multiplication, the repeated operation $nf$ applies $f$ $n$ times, and $m$ repetitions give $mn$. For exponentiation, $\overline{n}$ iterates the operation $\overline{m}$ on $f$: each iteration replaces a function $g$ by its $m$-fold iterate, yielding $f^{m^n}$. Zero iterations give $f$, so this encoding takes $m^0=1$, including $0^0=1$. The explicit outer $f,x$ abstractions make the result the standard Church numeral even at exponent zero, without needing eta equivalence.

Successor, addition, and multiplication operate on the same $C_A$. The displayed exponentiation term has type $C_A\to C_{A\to A}\to C_A$: its exponent iterates an operation on functions. Thus the numeral syntax admits several type instances; one should not force every occurrence into one fixed monomorphic Church type.

The Y combinator is the fixed-point combinatorFor $X_g=(\lambda x.g(xx))(\lambda x.g(xx))$, beta reduction gives $Yg{\to }_{\beta }{X}_g{\to }_{\beta }g{X}_g$. Since $X_g{\equiv }_{\beta }Yg$, we obtain $Yg{\equiv }_{\beta }g(Yg)$. This allows a recursive program body to receive a representation of itself.

Here the computation is in the untyped lambda calculus. The self-application $xx$ would require a simple type satisfying $A=A\to B$, impossible for finite simple types. Accordingly $Y$ is not a typed lambda term of the simply typed system. The Strong normalization theorem for simply typed lambda calculus also rules out a universal divergent fixed-point operator there.

To obtain a lambda representation of partial computable functions, encode machine configurations as finite data using Church numerals, Church pairs, and Church Booleans. Initial configuration, one transition, the halting test, and output extraction are primitive recursive functions, represented by lambda terms through the initial functions, composition, and lambda definition of primitive recursion by pair iteration. If these representations are $\mathsf{Init}$, $\mathsf{Next}$, $\mathsf{Halt}$, and $\mathsf{Out}$, defineUse normal-order beta reduction so the Church Boolean halting test selects one branch without evaluating the unused recursive branch. A halting computation follows finitely many transitions and returns the Church numeral of the output. A nonhalting computation forces successive tests forever and has no head normal form; by normal-order normalization theorem, it cannot be beta equivalent to a Church numeral. Thus every partial computable function is represented, with divergence preserved; every total computable function is the halting special case. This explains the role of $Y$ in computational universality while keeping the typed proof interpretation precise.

Write $Q=(A\to B)\to A$ and $P=Q\to A$. The displayed formula is $(P\to B)\to B$. A proof of logical implication may use its temporary assumption more than once; this is ordinary natural deduction, not a linear proof system.

Assume $h:P\to B$, then $f:Q$, then $a:A$, then $g:Q$. The identity weakening rule derives $a:A$ from the hypotheses $a:A$ and $g:Q$. Discharging $g$ by the implication introduction rule gives $\lambda g^Q.a:P$. Applying $h$ by the implication elimination rule gives $h(\lambda g^Q.a):B$. Discharge $a$ to obtain $\lambda a^A.h(\lambda g^Q.a):A\to B$. Applying $f$ gives an $A$; discharge $f$ to obtain a $P$; apply $h$ once more to obtain $B$, and finally discharge $h$.

Here is the complete decorated natural deduction derivation, split at its intermediate $A\to B$ conclusion to keep the tree readable. Superscript labels mark which assumption occurrences are discharged; both occurrences labelled $1$ 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.

Use the two derived inference rules whose complete proofs were supplied in (d). The following logical derivation has no nested hypothetical subproofs:

1  P → Q                           premise
2  Q → R                           premise
3  P → (Q → R)                     → creation from 2
4  (P → Q) → (P → R)               → distribution from 3
5  P → R                           →-elim, 1 and 4

The creation instance takes $\varphi =P$ and $\psi =(Q\to R)$. The distribution instance takes $(\varphi ,\psi ,\rho )=(P,Q,R)$. The metarules are justified in (d); this requested flat use does not secretly invoke implication introduction rule in one of its own lines.

The boxes delimit a subproof and identify the lifetime of its temporary assumptions. A result depending on a boxed assumption is available inside that box and its nested boxes; it cannot simply be exported outside. The enclosing rule specifies what may be exported and which assumptions are discharged. Other premises on which the derivation depends remain undischarged. This assumption discharge discipline distinguishes a conditional argument from an unconditional proof.

Write $H$ for $(\varphi \to \psi )\to \varphi$. The following derives Peirce's law directly from the printed primitive rules, including double-negation elimination:

Every assumption is discharged, so the last formula is a theorem. In particular, no unproved appeal to the derived RAA rule is hidden in the argument.

Let $K$ abbreviate $Q(c_1)\vee Q(c_2)$, and group the three equality alternatives on the left. The proof uses the binary disjunction elimination rule twice, so no unproved three-way derived rule is needed.

The witness name is absent from $K$ and from every assumption remaining after line 19, so the existential elimination is legal. Each equality is used in the forward direction supplied by the printed equality rule. The three named constants need not denote distinct objects: the case proof requires only that they exhaust the domain. This is existential quantification over a finitely named domain followed by exclusion of the first case.

Keep the four given premises in context and assume $P$ under label $a$. The modus ponens rule applied to the first two premises gives $Q\vee R$ and $\neg S$. Apply the disjunction elimination rule to $Q\vee R$ as follows.

Under a case assumption $Q$, the premise $Q\to S$ gives $S$ by the modus ponens rule. Together with $\neg S$, the negation elimination rule gives $\perp$, and the supplied logical falsity elimination rule gives $R$. Under the other case assumption $R$, the required conclusion $R$ is already available. Discharge both case assumptions with the disjunction elimination rule to conclude $R$.

Finally discharge $a$ with the implication introduction rule, giving $P\to R$. The premise $S\to Q$ is not needed: a derivation is permitted to leave a premise unused.

Use natural deduction with labelled temporary assumptions. Assume $\neg P\to \neg Q$ under label $a$, then $\neg P\to Q$ under label $b$, then $\neg P$ under label $c$. Two applications of the modus ponens rule give $\neg Q$ and $Q$. The negation elimination rule gives $\perp$, and the supplied reductio ad absurdum rule discharges $c$ to conclude $P$.

Discharge $b$ using the implication introduction rule, obtaining $(\neg P\to Q)\to P$ under $a$. Discharge $a$ with the implication introduction rule, obtainingAll three temporary assumptions have now been discharged; no premise remains.

Assume $E\to G$ under label $a$, $F\to G$ under label $b$, and $E\vee F$ under label $c$. A temporary case assumption $E$ gives $G$ by the modus ponens rule using $a$. A temporary case assumption $F$ gives $G$ by the modus ponens rule using $b$. The disjunction elimination rule discharges these case assumptions and concludes $G$ under $a,b,c$.

Apply the implication introduction rule three times, discharging $c$, then $b$, then $a$. The resulting theorem isThe displayed parentheses make explicit the right association of the source formula.

Choose arbitrary fresh variables $y,x,z$ and assume $H=((x=y\vee y=z)\wedge P(y))$ under label $a$. The conjunction elimination rule gives $x=y\vee y=z$ and $P(y)$. Apply the disjunction elimination rule to the equality disjunction.

In the case $x=y$, the supplied symmetry rule gives $y=x$, and the equality elimination rule applied to $P(y)$ gives $P(x)$. Disjunction introduction rule gives $P(x)\vee P(z)$. In the case $y=z$, equality elimination rule applied directly to $P(y)$ gives $P(z)$; the other disjunction introduction rule gives the same conclusion $P(x)\vee P(z)$. Discharge the two equality case assumptions by disjunction elimination rule.

Discharge $a$ with the implication introduction rule. There are now no undischarged assumptions. Use the universal quantifier introduction rule successively for $z$, then $x$, then $y$, yieldingFreshness holds at every generalization because the sole temporary assumption has already been discharged; the arbitrary variables are not tied to any premise.

Only $\psi$ requires a natural deduction proof. Assume $h:(A\vee B)\to C$. Within that assumption, temporarily assume $a:A$. By disjunction introduction, obtain $A\vee B$; applying $h$ by the implication elimination rule gives $C$. Discharge $a$ by the implication introduction rule to derive $A\to C$. Disjunction introduction now gives $(A\to C)\vee (B\to C)$. Finally discharge $h$ by the implication introduction rule:All temporary assumptions are discharged. No classical rule is needed; the same proof works in Intuitionistic propositional logic. The false propositional formula $\phi$ has no proof in this sound natural deduction system.

Keep the premise $P\to Q$ open. Assume $Q\to \neg P$, then temporarily assume $P$. Two applications of the implication elimination rule produce $Q$ and then $\neg P$, contradicting the temporary $P$. Discharge $P$ using the negation introduction rule, then discharge $Q\to \neg P$ using the implication introduction rule.This natural deduction proof uses only the supplied introduction and elimination rules. Line 6 is an application of the negation elimination rule; no classical contradiction principle is needed.

Propositional logic studies reasoning with whole propositions represented by letters such as $p$ and $q$, and propositional formulas built from them using logical connectives. The classical two-valued, truth-functional presentation below assigns each primitive proposition either true or false: each compound value depends only on its component values. This is classical propositional logic; other systems, including Intuitionistic propositional logic, have different semantics and rules.

Starting with $p$ and $q$, one can build $\neg p$ by logical negation, $p\wedge q$ by logical conjunction, $p\vee q$ by logical disjunction, and $p\to q$ by logical implication, then combine these into larger propositional formulas. Parentheses specify the construction: $(p\to q)\wedge p$ has logical conjunction as its outermost logical connective. Primitive propositions have no internal structure in this language; a first-order formula can additionally describe objects and quantify over them. The formation rules are given in forall x: Calgary, chapter 6.

The following truth table shows the four basic logical connectives. Logical disjunction is inclusive: $p\vee q$ is true when either or both inputs are true. Classical logical implication has exactly the same values as $\neg p\vee q$; its only false row has $p$ true and $q$ false. These truth conditions are specified in forall x: Calgary, chapter 9.

Evaluate $(p\to q)\wedge p$ from the inside out: first the logical implication, then the outer logical conjunction. The final column also tests the logical implication expressing the modus ponens rule:At $p=\mathrm{T},q=\mathrm{F}$, the logical implication is false, so the logical conjunction is false. The abstract syntax tree below separates the construction of the propositional formula from the values propagated through it. Both occurrences of $p$ receive the same value from the Boolean valuation. With the opposite assignment $p=\mathrm{F},q=\mathrm{T}$, the logical implication is true but the logical conjunction is still false because its second input $p$ is false. Recursive evaluation and exhaustive truth tables are explained in forall x: Calgary, chapter 11.

The last column is always true: $((p\to q)\wedge p)\to q$ is a tautology. This expresses the logical validity of the modus ponens rule: whenever both premises $p\to q$ and $p$ are true, $q$ is true. It does not say the premises are true under every Boolean valuation; their logical conjunction is true only on the first row. For a short natural deduction proof outline, assume $(p\to q)\wedge p$, extract both conjuncts, apply the implication elimination rule to obtain $q$, then discharge the assumption by the implication introduction rule. See forall x: Calgary, sections 17.3–17.5.

Three tests answer different questions: Boolean satisfiability requires at least one true row, a tautology requires every row true, and a contradiction has every row false. Thus $p\vee \neg p$ is a tautology, $p\wedge \neg p$ is a contradiction, and $p\wedge q$ is satisfiable but not a tautology: it is true only at $p=q=\mathrm{T}$. See forall x: Calgary, sections 12.1–12.4.

Propositional logic is useful because an inference pattern can be checked once and reused for many choices of propositions. Its beauty is that a finite truth table completely settles classical truth-functional questions about a fixed propositional formula. But logical validity does not verify real atomic claims. If $p$ means “the switch is closed” and $q$ means “the lamp is lit”, a valid use of the modus ponens rule still requires establishing its premises about the apparatus; the truth table supplies neither an observation nor a causal explanation. See forall x: Calgary, chapter 2 and chapter 10.

A typed lambda term carries a type derivation under a context of typed free variables. The rules for variables, abstraction, and application correspond to assumptions, the implication introduction rule, and the implication elimination rule under the Implicational Curry-Howard correspondence. General fixed-point combinators belong to the untyped lambda calculus; self-application cannot be given a finite simple type.