Matematické Fórum

check_drummer · 22. 05. 2017 16:17

Ahoj,
inspirován jiným vléknem zde, zadávám tento dotaz. Tvrzení, která budeme zkoumat, jsou myšlena čistě formálně - tj. jako syntaktické výroky. Uvažujme, že se pohybujeme v nějakém obecném tělese T (tj. t je dáno jako nějaká běžná množina axiomů popisujících těleso).
1) Je (v T) dokazatelé $1/0 = 1/0$ ?
20 Je (v T) dokazatelné $(1/0 = 1/0)'$ (tj. negace předchozího výroku)?

Upozorňuji, že mi jde o syntaktickou dokazatelnost (ve smyslu "odovozování řetězců z jiných řetězců" - kde tyto řetězce pokládáme za dokazatelné výroky), tj. tvrzení, že "nulou dělit nelze" samo o sobě nelze považovat za "důkaz".

Nabízím řešení k diskusi:

Autor skryl část textu. Zobrazit/skrýt!

check_drummer

Ahoj,
jeví se mi to tak, že platí jedno z následujících:

1) Znak pro dělení není součástí jazyka okruhu a tedy výraz 1/0 nemá smysl a tudíž ani uvedené výroky smysl nemají a tedy nemá smysl se bavit o jejich dokazatelnosti.

2) Znak pro dělení je sice součástí jazyka okruhů, ale některé výrazy nejsou povoleny, např. výrazy a/0, případně obecně výrazy a/b, kde je dokazatelné, že b=0.

Ponámka: Kdyby platil bod 1, pak bychom spoustu pěkných tvrzení nemohli formulovat, resp. museli bychom je složitě opisovat pomocí znaku násobení. Ale pro naše účely bych si v tom případě vybral nějakou jinou strukturu, např. s funkcí log a zkoumal bych třeba ("nedefinovaný") výraz log(0) - čímž bych bod 1 převedl na bod 2 (případně na bod 3).

3) Jsou povoleny i výrazy 1/0 (v syntaktickém smyslu, tj. jako "řetězce") a výroky, ve kterých se tyto výrazy vyskytují, lze zkoumat standardními postupy týkajícími se "dokazatelností". Tady se ale obávám, že by bylo možné dokázat nejen, že 1/0=1/0, ale např. i substitucí 1/0 do nějaké platné identity, např. že $(1/0+2)^2=(1/0)^2+2.(1/0).2+2^2$ . No ale proč ne? :-)
Ale v tomto případě tedy z vlastností predikátu rovnosti nebude dokazatelné $(1/0 = 1/0)'$ .

A jak to bude v bodě 3 s modelem (ve kterém by platilo 1/0=1/0)? O tom jsem nepřemýšlel, tak v krátkosti: Možná by ten model mohl mít samostatné individuum pro výraz 1/0. Případně žádný takový model uvedené struktury neexistuje - což by pak ale asi znamenalo, že je v té struktuře dokazatelné každé tvrzení, protože je platné ve všech modelech. :-) Takže struktura bez modelu je nezajímavá (sporná).

Tak asi tak, stále se nebráním diskusi. :-)

Wotton · 01. 09. 2021 18:08 — Editoval Wotton (01. 09. 2021 18:29)

Krásné, trochu mě to potrápilo, ale nakonec mám zdá se odpověď:

Beru to z pohledu logiky (v tělesech jsem jaště slabší).

Je třeba se zamyslet nad tím, co znamená výraz $a / b$ . Tento výraz je vlastně zkratka za takový prvek univerza $z$ pro který platí: $z = a / b \land \forall x (x = a / b \Rightarrow x = z)$ , pokud takový prvek existuje.

Zcela syntakticky správně by pak rovnice $a / b = c / d$ měla vypadat $\exists x \exists y ((x = a / b \land \forall u (u = a / b \Rightarrow x = u)) \land (y = c / d \land \forall v (v = c / d \Rightarrow y = v)) \land x = y)$
po dosazení za $a$ $b$ $c$ $d$ pak (při nějaké standardní axiomatizaci fonktoru $/$ ) je pak zjevně dokazatelná negace.

pokud bys ale nechtěl přistoupit na až tak hluboký stupeň formalizace, tak ti nezbyde než konstatovat, že výraz $1 / 0$ (z důvodu uvedeným výše) nedává smysl, tudíž nelze o rovnosti $1 / 0 = 1 / 0$ vůbec uvažovat.

Wotton · 01. 09. 2021 18:16

↑ Wotton:
a teď mi k tomu došlo, že to je krásná ukázka toho, že neplatí ekvivalence výroků $1 / 0 \neq 1 / 0$ a $\neg (1 / 0 = 1 / 0)$ . (první je vyvratitelný a druhý dokazatelný - při standardní axiomatizaci dělení)

MichalAld · 01. 09. 2021 23:22

Já na takové složitosti nejsem, ale z mého pohledu je ten operátor / prostě zobrazení definované podle

c=a/b => a = b*c

a pokud taková čísla nelze najít, tak prostě není definován.

No a když bychom chtěli množinu těch čísel rozšířit, podobně, jako jsme vymysleli imaginární čísla, že by se řeklo, že třeba

$x = 1 / 0$

tak se hned dostaneme ke sporům, protože pak by muselo platit, že

x = 1/0
5x = 5/0

takže

x * 0 = 1
5 * x * 0 = 5

Jenže my potřebujeme aby bylo násobení komutativní a asociativní, takže pravé strany se musí rovnat,

x * 0 = 1
x * (0 * 5) = 5

A máme tu ten spor. Takže takový symbol nemůžeme jednoduše zavést, narozdíl od té odmocniny z -1, pro kterou všechno krásně funguje.

Takže jestli tomu rozumím správně, tak předpokladem, že výraz 1/0 můžeme vytvořit si zavedeme do systému spor, a pak už v něm lze obecně dokázat i vyvrátit kde co...
Takže podle mě je jediný správný únik ten, že to prostě nesmíme udělat.

Wotton · 02. 09. 2021 14:33

↑ MichalAld:
to ale nelze tak jednoduše udělat, dokud se bavíme jen o syntax jak chtěl na začátek kolega.

Matematické Fórum

#1 22. 05. 2017 16:17

Dokazatelnost podivné (ne)rovnosti

#2 27. 05. 2017 16:00 — Editoval check_drummer (27. 05. 2017 16:04)

Re: Dokazatelnost podivné (ne)rovnosti

#3 01. 09. 2021 18:08 — Editoval Wotton (01. 09. 2021 18:29)

Re: Dokazatelnost podivné (ne)rovnosti

#4 01. 09. 2021 18:16

Re: Dokazatelnost podivné (ne)rovnosti

#5 01. 09. 2021 23:22

Re: Dokazatelnost podivné (ne)rovnosti

#6 02. 09. 2021 14:33

Re: Dokazatelnost podivné (ne)rovnosti

Zápatí