Main derivation
S01 · definition
Before
\text{proof term: fixed version, imports, environment }E,\ \Gamma,\ \text{kernel}After
\text{ST: atoms }P\neq Q,\ \Gamma_0=\varnothing,\ S=P\land Q\to Q\land P,\ \text{six rules}Conditions: none
Rule: mko_proof_term · Uses: G1, G2, G3, G4
Leaf basis: mko_proof_term + def_intro
The MKO says that 'proof term' is meaningful only after the version, imports, environment and local context are fixed. This guide fixes a teaching counterpart: the environment E_ST contains only the atoms P and Q, the starting context Γ0 is empty, the target proposition is S=P∧Q→Q∧P, and the role of the checker is played by the six rules of G2: a judgment holds only if it can be derived rule by rule from them. Every typing conclusion below is a conclusion in ST; statements about Lean are handled separately in S10.
S02 · definition
Before
t
After
t=\lambda h{:}P\land Q.\,\langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangleConditions: none
Rule: def_intro · Uses: S01, G3
Leaf basis: def_intro + def_unfold
Name the term and preview what each part is meant to establish: λh:P∧Q introduces a hypothesis named h of type P∧Q, read as 'assume a proof h of P∧Q'; fst h and snd h extract proofs of P and of Q from h; ⟨·,·⟩ packs two proofs into a proof of a conjunction, and the order of the components fixes the order of the conjuncts. Under propositions-as-types, a proof of an implication is a function that turns proofs of the premise into proofs of the conclusion. The Lean 4 surface counterpart is `fun h : P ∧ Q => And.intro h.right h.left` (or `fun h => ⟨h.2, h.1⟩`), given here only as a reading aid.
S03 · implies
Before
\Gamma_1=\Gamma_0,\ h{:}P\land QAfter
\Gamma_1\vdash h:P\land Q
Conditions: h{:}P\land Q\in\Gamma_1
Rule: st_var · Uses: S02, G2
Leaf basis: st_var
The λ-binder says in which context the body is checked: Γ1 is Γ0 extended by h:P∧Q. By the Var rule, h:P∧Q is listed in Γ1, so Γ1⊢h:P∧Q. What this part establishes: inside the body, h may be used as a proof of P∧Q.
S04 · implies
Before
\Gamma_1\vdash h:P\land Q
After
\Gamma_1\vdash \mathrm{snd}\,h:QConditions: A=P,\ B=Q
Rule: st_and_elim · Uses: S03, G2
Leaf basis: st_and_elim
Apply ∧E2 to S03 with A=P and B=Q: snd h extracts the second component and has type Q. This part establishes 'a proof of Q obtained from the hypothesis'. The type of snd h is read off from the type of h; it is not chosen freely.
S05 · implies
Before
\Gamma_1\vdash h:P\land Q
After
\Gamma_1\vdash \mathrm{fst}\,h:PConditions: A=P,\ B=Q
Rule: st_and_elim · Uses: S03, G2
Leaf basis: st_and_elim
Apply ∧E1 to S03: fst h extracts the first component and has type P. Now Γ1 has both a proof of P and a proof of Q, and both depend only on the hypothesis h.
S06 · implies
Before
\Gamma_1\vdash \mathrm{snd}\,h:Q,\ \ \Gamma_1\vdash \mathrm{fst}\,h:PAfter
\Gamma_1\vdash \langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:Q\land PConditions: a=\mathrm{snd}\,h,\ A=Q,\ b=\mathrm{fst}\,h,\ B=P
Rule: st_and_intro · Uses: S04, S05
Leaf basis: st_and_intro
Apply ∧I with first component a=snd h (type A=Q) and second component b=fst h (type B=P), giving A∧B=Q∧P. The order of the conjuncts is fixed by the order of the components: the type of the first component becomes the left conjunct. This part establishes 'a proof of Q∧P from the hypothesis P∧Q'.
S07 · implies
Before
\Gamma_0,\ h{:}P\land Q\vdash \langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:Q\land PAfter
\Gamma_0\vdash \lambda h{:}P\land Q.\,\langle \mathrm{snd}\,h,\ \mathrm{fst}\,h\rangle:P\land Q\to Q\land PConditions: x=h,\ A=P\land Q,\ B=Q\land P
Rule: st_imp_intro · Uses: S06, S03
Leaf basis: st_imp_intro + imp_intro
Apply →I with x=h, A=P∧Q and B=Q∧P: the hypothesis h is discharged and the conclusion lives in Γ0, where h no longer appears. The binder's annotation P∧Q becomes the antecedent of the implication and the body's type Q∧P becomes its consequent. This is →-introduction (imp_intro) read through propositions-as-types: obtaining Q∧P inside the scope of the assumption P∧Q gives P∧Q→Q∧P.
S08 · implies
Before
T(t)=P\land Q\to Q\land P,\ \ S=P\land Q\to Q\land P
After
T(t)\equiv S
Conditions: none
Rule: st_type_eq · Uses: S07, G3
Leaf basis: st_type_eq + eq_refl_symm_trans
The MKO formula T(t)=P asks that the derived type be the proposition itself (here the proposition is called S to avoid a clash with the atom P). Compare symbol by symbol: antecedent P∧Q against P∧Q, consequent Q∧P against Q∧P; they are identical, so T(t)≡S in ST. Lean compares types up to definitional equality, a wider relation; ST uses syntactic identity only, so no conversion is used here.
S09 · implies
Before
\Gamma_0\vdash t:T(t),\ \ T(t)\equiv S
After
t\ \text{is a proof term for }S\ \text{in ST}Conditions: none
Rule: mko_proof_term · Uses: S07, S08, mko_proof_term
Leaf basis: mko_proof_term + modus_ponens + eq_replace
The MKO definition asks for two things: the term's type is the proposition, and the checker of the fixed environment accepts the judgment. In ST the checker is the rule table: each of S03 to S07 is one rule of G2, forming a complete derivation of Γ0⊢t:T(t), and S08 identifies T(t) with S, so Γ0⊢t:S is derivable, the ST counterpart of 'the kernel accepts Γ⊢t:P'. Hence t is a proof term for S in ST; that is all this step claims.
S10 · implies
Before
t\ \text{proof term in ST};\ \text{Lean not run}After
\text{Lean counterpart: candidate term, no kernel verdict, no receipt}Conditions: none
Rule: mko_receipt · Uses: S09, G4, mko_receipt
Leaf basis: mko_receipt + modus_ponens
By the MKO, only a saved term checked by the specified kernel in the specified environment forms a receipt. G4 records that Lean was not run, and no term was saved or checked. So the Lean 4 counterpart `fun h : P ∧ Q => And.intro h.right h.left` has the status of a candidate proof term only: no kernel acceptance is claimed and there is no receipt. The ST derivation cannot replace a kernel verdict, because the two are different systems (Lean also has universes, definitional equality and an elaborator). Even if a kernel later accepted it, that would prove only the formal judgment; whether the proposition faithfully expresses the intended claim and whether the imports contain improper axioms still need separate review.
S11 · implies
Before
\text{rule table of ST}After
\text{each outer term form is concluded by exactly one rule}Conditions: none
Rule: case_analysis · Uses: G2
Leaf basis: case_analysis + def_unfold
Go through the six rules and record the outer form of the subject in each conclusion: Var, a variable; ∧I, a pair ⟨a,b⟩; ∧E1, fst p; ∧E2, snd p; →I, λx:A.b; →E, an application f a. Six rules, six pairwise distinct forms, and every term has exactly one outer form. A derivation of Γ⊢u:A ends with a rule whose conclusion is Γ⊢u:A, so its last rule is the unique rule for u's outer form, that rule's premises must have been derived above it, and A must have the shape the rule prescribes. This proves Lemma L_inversion.
S12 · implies
Before
t'=\lambda h{:}P\land Q.\,\langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangleAfter
\Gamma_0\nvdash t':P\land Q\to Q\land P
Conditions: none
Rule: L_tprime_untyped · Uses: G3, L_tprime_untyped
Leaf basis: L_inversion + st_type_eq + contradiction
By Lemma L_tprime_untyped (proved in S12.1 to S12.4), t′ cannot have type S in ST. So t′ is not a proof term for S, even though it uses the same hypothesis and the same two projections.
S13 · implies
Before
\Gamma_1\vdash \mathrm{fst}\,h:P,\ \ \Gamma_1\vdash \mathrm{snd}\,h:QAfter
\Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:P\land QConditions: a=\mathrm{fst}\,h,\ A=P,\ b=\mathrm{snd}\,h,\ B=Q
Rule: st_and_intro · Uses: S04, S05
Leaf basis: st_and_intro
See what t′ actually proves: with the components in the order fst h, snd h, ∧I gives P∧Q, not Q∧P. The only difference is the order of the components, and it changes the type.
S14 · implies
Before
\Gamma_0,\ h{:}P\land Q\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:P\land QAfter
\Gamma_0\vdash t':P\land Q\to P\land Q
Conditions: x=h,\ A=P\land Q,\ B=P\land Q
Rule: st_imp_intro · Uses: S13
Leaf basis: st_imp_intro + imp_intro
Apply →I to S13 and discharge h: t′ is a proof term for P∧Q→P∧Q, a different proposition. So whether a term proves S depends on its exact type, not on which hypotheses or projections it uses.
S15 · implies
Before
\Gamma_0\vdash t:S,\ \Gamma_0\nvdash t':S,\ \text{Lean not run}After
t\ \text{proves }S\ \text{in ST};\ t'\ \text{does not};\ \text{no Lean receipt}Conditions: none
Rule: and_intro_elim · Uses: S09, S10, S12, S14
Leaf basis: and_intro_elim
Combine the three conclusions: t is a proof term for S in ST (S09); t′ is not (S12), and proves P∧Q→P∧Q instead (S14); on the Lean side there is only a candidate term, with no kernel verdict and no receipt (S10).
Substeps and lemmas
S12.1 · implies
Before
\Gamma_0\vdash t':P\land Q\to Q\land P\ \ (\text{assumed})After
\Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:Q\land PConditions: none
Rule: L_inversion · Uses: G3, L_inversion
Leaf basis: L_inversion + st_type_eq
For contradiction, assume Γ0⊢t′:S has a derivation. The outer form of t′ is λ, so by L_inversion the last rule is →I; in its conclusion type A→B, A is the binder annotation P∧Q, and A→B≡P∧Q→Q∧P gives B≡Q∧P. So the premise Γ0,h:P∧Q⊢⟨fst h, snd h⟩:Q∧P is derivable, that is, Γ1⊢⟨fst h, snd h⟩:Q∧P.
S12.2 · implies
Before
\Gamma_1\vdash \langle \mathrm{fst}\,h,\ \mathrm{snd}\,h\rangle:Q\land PAfter
\Gamma_1\vdash \mathrm{fst}\,h:QConditions: none
Rule: L_inversion · Uses: S12.1, L_inversion
Leaf basis: L_inversion + st_type_eq
A pair is concluded only by ∧I, whose conclusion type A∧B has A equal to the type of the first component. A∧B≡Q∧P gives A≡Q, so the premise Γ1⊢fst h:Q must be derivable.
S12.3 · implies
Before
\Gamma_1\vdash \mathrm{fst}\,h:QAfter
\Gamma_1\vdash h:Q\land B\ \text{for some type }BConditions: none
Rule: L_inversion · Uses: S12.2, L_inversion
Leaf basis: L_inversion
The form fst is concluded only by ∧E1, whose premise is Γ1⊢h:A∧B with conclusion type A. Here A≡Q, so for some type B the judgment Γ1⊢h:Q∧B is derivable.
S12.4 · implies
Before
\Gamma_1\vdash h:Q\land B
After
Q\land B\equiv P\land Q\Rightarrow Q\equiv P\ \ (\text{contradiction})Conditions: P\not\equiv Q
Rule: contradiction · Uses: S12.3, G1, G2, L_inversion
Leaf basis: st_var + st_type_eq + contradiction
A variable is concluded only by Var, so h:Q∧B must be exactly the entry for h in Γ1; Γ1 lists h once, with type P∧Q, so Q∧B≡P∧Q. Componentwise comparison by st_type_eq gives Q≡P, contradicting that P and Q are distinct atoms (G1). So the assumption of S12.1 fails and Γ0⊢t′:S is not derivable. S12.1 to S12.4 together prove Lemma L_tprime_untyped.