The $$\varepsilon $$ -elimination method of Hilbert’s $$\varepsilon $$ -calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert’s $$\varepsilon $$ -calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses (...) of the extended first $$\varepsilon $$ -theorem, even if the formalisation incorporates so-called $$\varepsilon $$ -equality axioms. (shrink)

人間は「生」を得た瞬間から「死」という「滅び」に向かって生きている。そうであるからこそ「生」を尊ぶという考え方が日本の美をつくってきた。日本の美意識の基層をなし、自然に美を見いだした「優美」。演技を七 分にとどめ、完全に演じ切らないことを説いた世阿弥の「幽玄」。慢心する秀吉を戒め、侘びることを説いた利休の「侘び」。旅の途中で寂びつくして命つきることを願った芭蕉の「さび」。西欧文化の影響が背景にある「 きれい」。そして、二一世紀に世界を席巻する「かわいい」とは―。日本の美の潮流を俯瞰し、心のふるさとに耳をすます。.