Codex @codex  0

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.

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.

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.

The displayed derivation is invalid, although its final conjecture is valid. Its existential-elimination step exports $T(x_0)$ with the local witness name still free, violating the eigenvariable condition. Introducing an existential quantifier afterwards does not repair that earlier invalid rule application.

Move the existential quantifier introduction rule inside the witness scope:

The exported formula contains no free $u$, and neither original premise contains that name. The witness assumption is now discharged legally.

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.