Matematik odhalil, že slovo „rovná se“ má v matematice více než jeden význam. To vede ke zmatkům v oblasti počítačové technologie

V matematice jsou některé dost mlhavé pojmy, které je těžké pochopit, ale mysleli jsme si, že význam pojmu „rovná se“ jsme zvládli.

Ukázalo se, že matematici se ve skutečnosti nemohou shodnout na definici toho, co činí dvě věci rovnými, a to by mohlo způsobit určité potíže počítačovým programům, které se stále častěji používají ke kontrole matematických důkazů.

Tento akademický spor se táhne už desítky let, ale nakonec se dostal na přetřes, protože počítačové programy používané k „formalizaci“ nebo kontrole důkazů musí mít jasné, konkrétní instrukce, nikoli nejednoznačné definice matematických pojmů, které se dají interpretovat nebo se opírají o kontext, který počítače nemají.

Britský matematik Kevin Buzzard z Imperial College London na tento problém narazil při spolupráci s počítačovými programátory a to ho přimělo přehodnotit definice „to se rovná tomu“, aby „zpochybnil různá rozumně znějící hesla o rovnosti“.

„Před šesti lety,“ píše Buzzard ve svém preprintu zveřejněném na serveru arXiv, „jsem si myslel, že matematické rovnosti rozumím. Myslel jsem si, že je to jeden dobře definovaný pojem… Pak jsem začal zkoušet dělat magisterskou úroveň matematiky v počítačovém teorému a zjistil jsem, že rovnost je poněkud trnitější pojem, než jsem si myslel.“

Znaménko rovnosti (=) se dvěma rovnoběžkami, které elegantně znázorňují paritu mezi objekty umístěnými na obou stranách, vymyslel velšský matematik Robert Recorde v roce 1557. Zpočátku se příliš neujalo, ale časem Recordův geniálně intuitivní symbol nahradil latinský výraz „aequalis“ a později položil základy informatiky. Přesně 400 let po svém vynálezu byl znak rovnosti poprvé použit jako součást počítačového programovacího jazyka FORTRAN I v roce 1957.

Koncept rovnosti má však mnohem delší historii, která sahá přinejmenším do starověkého Řecka. A moderní matematici v praxi používají tento pojem „spíše volně“, píše Buzzard.

Ve známém použití znaménko rovnosti nastavuje rovnice, které popisují různé matematické objekty, jež představují stejnou hodnotu nebo význam, což lze dokázat pomocí několika přehození a logických transformací ze strany na stranu. Například celé číslo 2 může popisovat dvojici objektů, stejně jako 1 + 1.

Druhá definice rovnosti se však mezi matematiky používá již od konce 19. století, kdy vznikla teorie množin.

Teorie množin se vyvíjela a s ní se rozšířila i definice rovnosti matematiků. Množinu jako {1, 2, 3} lze považovat za „rovnou“ množině jako {a, b, c} díky implicitnímu chápání, které se nazývá kanonický izomorfismus a které porovnává podobnosti mezi strukturami skupin. „Tyto množiny se navzájem shodují zcela přirozeným způsobem a matematici si uvědomili, že by bylo opravdu výhodné, kdybychom je také nazývali rovnými,“ řekl Buzzard Alexi Wilkinsovi z časopisu New Scientist.

Matematik Buzzard však píše, že chápání kanonického izomorfismu jako rovnosti nyní způsobuje matematikům, kteří se snaží formalizovat důkazy – včetně desítky let starých základních pojmů – pomocí počítačů, „skutečné potíže“. „Žádný z dosud existujících počítačových systémů nezachycuje způsob, jakým matematici jako Grothendieck používali symbol rovnosti,“ řekl Buzzard Wilkinsovi s odkazem na Alexandra Grothendiecka, předního matematika 20. století, který se při popisu rovnosti opíral o teorii množin.

Někteří matematici se domnívají, že by měli jen předefinovat matematické pojmy tak, aby formálně ztotožňovaly kanonický izomorfismus s rovností. Buzzard s tím nesouhlasí. Myslí si, že nesoulad mezi matematiky a stroji by měl přimět matematiky, aby znovu promysleli, co přesně myslí pod tak základními matematickými pojmy, jako je rovnost, aby jim počítače rozuměly.

„Když je člověk nucen napsat, co tím vlastně myslí, a nemůže se schovávat za tak špatně definovaná slova,“ píše Buzzard. „Člověk někdy zjistí, že si musí dát práci navíc, nebo dokonce přehodnotit způsob, jakým by měly být určité myšlenky prezentovány.“

Autor: Lukáš Drahozal

Zdroj: arxiv.org, newscientist.com