"'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ƃ
- .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. .
FRIAM Applied Complexity Group listserv
Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam
un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com
archives: http://friam.471366.n2.nabble.com/
FRIAM-COMIC http://friam-comic.blogspot.com/
