[FRIAM] Quantum Woo Again

[uǝlƃ ↙↙↙]

"'Tonk' is a very exciting and powerful connective" ROFL!

I wish I'd had this quote from Maruyama's paper in hand last Friday: "(intensional differences between extensionally equivalent programs do matter in computer science)". 

Actually made me look up the cut-elimination proof up in Kleene:
"Theorem 48. Given a proof in G1 {in G2) of a sequent in which no variable occurs both free and bound, another proof in G1 (in G2) of the same sequent can be found which contains no cut (no mix). This proof is a pure variable proof. The only logical rules applied in it are ones which were applied in the given proof. (Gentzen's Hauptsatz or normal form theorem, 1934-5·)
Proof, reducing the theorem to a lemma. By Lemmas 34, 37 and 38, it suffices to prove the theorem for G2 assuming the given proof already to have the pure variable property. We do so by induction on the number m of mixes in this 'given proof'. If m > 0, there must occur in it a mix which has no other mix over it. Consider the part of the given proof which terminates with the conclusion Π, Σ_Μ→Φ_Μ, Ω of this mix; call it the 'given part'. Suppose that we can transform this given part so as to obtain another proof in G2 of Π, Σ_Μ→Φ_Μ, Ω without mix; call it the 'resulting part'. Then the replacement of the given part by the resulting part in the given proof gives us a new proof in G2 of the same sequent with only m—1 mixes. Suppose further that the resulting part can be constructed so that it has the pure variable property by itself, and also contains no variable free (bound; as the b of an →∀ or ∃→) that did not so occur in the given part. Then the new proof as a whole will have the pure variable property. Hence we can apply the hypothesis of the induction to conclude that there is a pure variable proof with no mix. To prove the theorem it thus remains to establish the following lemma.

Lemma 39. Given a proof in G2 of Π, Σ_M —> ΦΜ, Ω with a mix as the final step, and no other mix, and with the pure variable property, a proof in G2 of Π, Σ_Μ —> ΦΜ, Ω can be found with no mix, with the pure variable property, and with no variable occurring free {bound; as the b of an →∀ or ∃→) which did not so occur in the given proof. Only logical rules are applied in the resulting proof which are applied in the given proof. (Principal lemma.)
Proof of the principal lemma. We define the left rank a of a mix as the greatest number of sequents, located consecutively one above another at the bottom of any branch terminating with the left premise of the mix, which contain the mix formula Μ in the succedent. The right rank b is defined similarly. The rank r = a+b. (The least possible rank is 2.) The grade g of the mix is the number (≥ 0) of occurrences of logical symbols (⊃, &, V, ¬, ∀, ∃) in the mix formula M."

On 8/11/20 5:04 PM, jon zingale wrote:
> Ha, right!? I feel very fortunate for this Sarah-dipity (and the path
> dependence of grooming one's Google). Thanks for pointing to this paper,
> I was not familiar with Prior's tonk or the failings of local reduction.
> Now I am now enjoying the rabbit hole :)
> 
> Somewhere down the rabbit hole, I find:
> https://web.archive.org/web/20120514090806/http://www.logicandlanguage.net/archives/2005/03/tonk_and_local_1.html


-- 
↙↙↙ uǝlƃ