Seven trees in one

DOI10.1016/0022-4049(95)00098-HMaRDI QIDQ1901018zbMATH OpenFDO

Publication date 22 September 1996

Published in Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/9405205

finite binary trees intuitionistic set theory objective number theory polynomials provability semirings seven-tuples of trees very explicit bijection

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Combinatorial identities, bijective combinatorics (05A19) Trees (05C05) Semirings (16Y60) Topoi (18B25)

Abstract: Following a remark of Lawvere, we explicitly exhibit a particularly elementary bijection between the set T of finite binary trees and the set T^7 of seven-tuples of such trees. "Particularly elementary" means that the application of the bijection to a seven-tuple of trees involves case distinctions only down to a fixed depth (namely four) in the given seven-tuple. We clarify how this and similar bijections are related to the free commutative semiring on one generator X subject to X=1+X^2. Finally, our main theorem is that the existence of particularly elementary bijections can be deduced from the provable existence, in intuitionistic type theory, of any bijections at all.

Review text

This is a pilot project inside ``objective number theory, as envisaged and begun by Lawvere and Schanuel. More precisely, if a complex number \(T\) satisfies the equation \(T = T^2 + 1\), then it also satisfies \(T^6 = 1\), and hence \(T^7 = T\). But this particular entailment may not only be seen on the level of numbers, but on the level of sets, meaning that an explicit bijection between sets \(T\) and \(T^2 + 1\) (=cartesian product of \(T\) with itself, with an added new base point) entails an explicit bijection between \(T^7\) and \(T\). An explicit bijection between \(T\) and \(T^2 + 1\) exists for instance when \(T\) is the set of (binary) trees; for, a (binary) tree is either just a root, or splits naturally into a pair of subtrees (by removing the root). The author establishes now a very explicit bijection between the set \(T^7\) of seven-tuples of trees and the set \(T\) of trees itself, and also makes sense to the phrase ``very explicit; one way to make sense to it is as provability in intuitionistic set theory with an added axiom. -- For the general program of objective number theory, see the contributions by Lawvere and Schanuel in: Category theory, Proc. Int. Conf., Como 1990 [\textit{F. W. Lawvere}, Lect. Notes Math. 1488, 279-281 (1991; Zbl 0745.18002); \textit{S. H. Schanuel}, ibid. 379-385 (1991; Zbl 0748.18005)].

Recommendations

Cites work

Cited in

(11)

This page was built for publication: Seven trees in one

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1901018)