Matematické Fórum

check_drummer napsal(a):

MichalAld napsal(a):

Platí výrok P, existuje důkaz, že platí výrok P?

Ještě k tvému dotazu: V logice je potřeba přesbně rozlišovat pojmy. Např. co to znamená, že "existuje důkaz, že platí výraok P"? V logice jsou dva pojmy "výrok je platný" a "výrok je dokazatelný", ale nevím co myslíš tím, že "existuje důkaz, že výrok platí".

No třeba jestli lze dokázat, že nějaká konkrétní diofantická rovnice nemá řešení.

Tak tuto tvoji lavinu......

check_drummer napsal(a):

Eratosthenes napsal(a):

>> já říkám, že z toho, že lze dokázat tvrzení "číslo n je sudé nebo číslo n je liché" plyne, že lze dokázat tvrzení "číslo n je sudé" nebo lze dokázat tvrzení "číslo n je liché".

Nelze.

Musíš si zvolit konkrétní číslo n, pokud je to myšleno pr ovšechna n, pak už to není výraz tvaru P nebo Q, protože je kolem těch výroků jeešetě obecný kvantifikátor.

Eratosthenes napsal(a):

>> Nejdřív dokážu G. větu o úlnosti a pak to tvrzení o kterém píšu výše...

To bys musel G. větu o úlnosti dokázat bez použití P => P. A to se myslím nepodaří,

Proč bych nemohl použít při důkazu věty o úplnosti tvrzení P=>P?

Eratosthenes napsal(a):

>> Jestli to dobře chápu, tak MichalAld se ptá na to, zda z toho, že výrok P platí, tak je výrok P dokazatelný, což je něco jiného než že platí (nebo že je dokazatelný)

Už je z toho trochu guláš. Co znamená, že výrok "platí"? Zaplatí za mě v hospodě? Asi ne.

Znamená to tedy, že je pravdivý, anebo že je dokazatelný?  Obecně se má za to, že je to jedno, ale není.

Každý dokazatelný výrok je pravdivý. Ale ne každý pravdivý výrok je dokazatelný - viz např. axiom.

Že je výrok dokazatelný znamená že existje jeho důkaz. Že platí (nebo že je splnitelný) znamená, že platí (je splnitelný) v každém modelu.

A platí věta - to je právě ta Godelova věta o úplnosti - že výrok je dokazatelný právě když platí (je splnitelný). Axiom samozřejmě dokazatelný je, triviálně - důkaz obsahuje jen jeden člen.

... už vážně vzdávám.

↑ MichalAld:
No úplně ta otázda diofantický rovnic nesouvisí s tou platností, ale ok.... Ale možná jsi to myslel jako speciální případ.

Samozřejmě že o nějaké konrétní diofantické rovnici můžeš dokázat že nemá řešení, např. x^2=-2 nemá pro x celé řešení....

Ale tobě šlo asi o to zda pro každou diofanticku rovnici, která nemá řešení, existuje důkaz, že nemá řešení, že? To si myslím, že asi ne a že to souvisí s tou větou o neúplnosti... Sice jsi psal že ta se týká hluboké logiky, ale de facto se týká také přirozeých čísel, takže to spolu může dost souviset...

Ono je to možná tak, že existují rovnice, které ve standardním modelu přirozeých čísel řešení nemají, ale v nějakém nestandardním modelu řešení mají....

check_drummer napsal(a):

Samozřejmě že o nějaké konrétní diofantické rovnici můžeš dokázat že nemá řešení, např. x^2=-2 nemá pro x celé řešení....

No jo, u některých rovnic lze dokázat, že řešení nemají, u jiných zase se řešení podařilo najít. Jako třeba
[mathjax]x^3 + y^3 + z^3 = 29[/mathjax], řešení je (3, 1, 1)

nebo
[mathjax]x^3 + y^3 + z^3 = 30[/mathjax],
řešení je a = −283 059 965, b = −2 218 888 517, c = 2 220 422 932

ale třeba u rovnice
[mathjax]x^3 + y^3 + z^3 = 33[/mathjax]
se to prý zatím neví.

check_drummer napsal(a):

Ale tobě šlo asi o to zda pro každou diofanticku rovnici, která nemá řešení, existuje důkaz, že nemá řešení, že? To si myslím, že asi ne a že to souvisí s tou větou o neúplnosti... Sice jsi psal že ta se týká hluboké logiky, ale de facto se týká také přirozeých čísel, takže to spolu může dost souviset...

Ono je to možná tak, že existují rovnice, které ve standardním modelu přirozeých čísel řešení nemají, ale v nějakém nestandardním modelu řešení mají....

Jako rozumím tomu, že nerozhodnutelné tvrzení může být něco ve stylu "pro každou diofantickou rovnici lze rozhodnout o tom, jestli má řešení..."

Ale pro jednu konkrétní? Třeba pro tu poslední co jsem uvedl? Rovnice nemůže zároveň mít a nemít řešení, je nesmysl, aby to bylo nerozhodnutelné tvrzení a mohli jsme si ho zvolit. Buďto taková 3 čísla existují, nebo neexistují. Otázka je, jestli to lze dokázat (že neexistují). Protože podle té Matijasevičovy věty (jestli to chápu správně) to dokázat nejde. Takže to nevíme. Ale to neznamená, že si to můžeme zvolit.

MichalAld napsal(a):

Ale pro jednu konkrétní? Třeba pro tu poslední co jsem uvedl? Rovnice nemůže zároveň mít a nemít řešení, je nesmysl, aby to bylo nerozhodnutelné tvrzení a mohli jsme si ho zvolit. Buďto taková 3 čísla existují, nebo neexistují. Otázka je, jestli to lze dokázat (že neexistují). Protože podle té Matijasevičovy věty (jestli to chápu správně) to dokázat nejde. Takže to nevíme. Ale to neznamená, že si to můžeme zvolit.

To, že řešení nemá ještě neznamená, že existuje důkaz že tomu tak je....
A co je zajímavější, nemusí mít řešení ve standardním modelu celých čísel, ale může mít řešení v nestandardním modelu celých čísel.... A pak to tvrzení dokázat nepůjde z principu ...
Myslím si, že taková rovnice, která nemá řešení, ale o které to nepůjde dokázat, existovat bude, bude to nějaká variace na téma věty o neúplnosti...

↑ MichalAld:
Ještě bys měl vědět co znamená, že tvrzení platí, jakou používáš definici?

Co myslíš poznámkou, že "nerozhodnutelné tvrzení znamená, že si to můžeme zvolit"?

Myslím, že axiomy se nedokazují, že se prostě považují za platné.

check_drummer napsal(a):

↑ MichalAld:
Co myslíš poznámkou, že "nerozhodnutelné tvrzení znamená, že si to můžeme zvolit"?

Já znám jen jedinné nerozhodnutelné tvrzení, a to je to všeobecně známé o existenci množiny, co svou mohutností leží mezi spočetnou množinou a kontinuem.

No a protože to nelze ani dokázat ani vyvrátit, můžeme se svobodně rozhodnout, jeslti taková množina existuje nebo neexistuje a přidat to jako další axiom. Sice to nic užiteného nepřinese, ale udělat to můžeme.

Zatímco si nedokážu představit, že bychom mohli svobodně přidat tvrzení, že řešení nějaké diofantické rovnice existuje, když neumíme dokázat, že neexistuje.

↑ Eratosthenes:
Napiš jakou používáš definici pojmu "důkaz" (Edit: nebo přesněji řečeno "důkaz výroku P"), z toho vyplyne, jak je to s tou dokazatelností axiomů.

check_drummer napsal(a):

↑ Eratosthenes:
Napiš jakou používáš definici pojmu "důkaz", z toho vyplyne, jak je to s tou dokazatelností axiomů.

Tím se dostáváme k dalšímu kroku:

check_drummer napsal(a):

↑ Eratosthenes:
Přesně tak než si nastaduješ základní pojmy z logiky (myslím skutečnou logiku ne tu středoškolskou) je tato debata neplodná...

No, já jsem se kdysi základy té "skutečné logiky" nastudovat snažil, ale prostě to nešlo. Pořídil jsem si jakousi učebnici, o které jsem se na předsásce dověděl, že je to „jedna z nejlepších moderních prací o logice”.

Vlastní text knihy začínal naprosto neuvěřitelnou definicí, která jakékoli logice (moderní, nemoderní, formální i neformální) zasazuje hned zpočátku zcela smrtící úder. Ve snaze definovat naprosto vše, začíná „definicí“ symbolu: „Pojmom symbol rozumieme a) spočetnú množinu symbolov… A aby bylo úplně jasno, slovenský překladatel v první překladatelské poznámce vysvětluje: Termínom „spočetná množina” sa rozumie spočetne nekonečná množina, tj. množina, ktorá je je ekvivalentná s množinou všetkých prirodzených čísiel”. Bezprostředně poté pod písmenem b) pak následuje obšírná definice levé a pravá závorky.

Kromě logického kruhu s nejmenším možným "poloměrem" tady máme symbol definovaný pomocí spočetné množiny. To prostě nevymyslíš. Takže aby ses nedostal do logického kruhu, musel bys před touto "definicí" vybudovat teorii spočetných množin bez jediného symbolu. Tak jsem tuto "nejlepší knihu" zavřel, podložil jsem s ní skříň a začal pátrat po něčem nejblíže horším. Skončil jsem podobně.

Nejdál jsem se dostal asi po pátém pokusu, kde byl důkaz "definován" takto:

Důkaz tvrzení A z předpokladů [mathjax]P_1;...;P_n[/mathjax] je posloupnost tvrzení [mathjax]B_1;...;B_m[/mathjax] taková, že:
a)  [mathjax]B_m=A[/mathjax]
b) pro každé [mathjax]i<m[/mathjax] platí, že [mathjax]B_i[/mathjax] je buď
- jeden z předpokladů [mathjax]P_j[/mathjax] nebo
- [mathjax]B_i[/mathjax] vznikne z předchozích [mathjax]B_1;...;B_{i-1}[/mathjax] uplatněním nějakého odvozovacího pravidla.

Takže totéž v bleděmodrém. Definice důkazu používá k indexování množinu přirozených čísel včetně jejího uspořádání. To všechno tedy musíš sestrojit předtím, a to bez jediného důkazu, protože ten je definován až zde.

Další skříň se mi přestala viklat a protože se mi už žádná neviklala, nic dalšího už jsem nesháněl a napsal jsem si logiku sám.

Podle mě musíš definici důkazu vzdát a použít metadefinici a metapojmy, které bz tím pádem měly být co nejjednoduší. Takže

Metadefinice - důkaz: důkaz formule F je výpis formulí vzniklých přepisem předpokladů aplikováním odvozovacích pravidel tak, že poslední formulí je formule F.

↑ check_drummer:

check_drummer napsal(a):

↑ Eratosthenes:

Teď je otázka jestli mezi ty předpoklady [mathjax]P_1;...;P_n[/mathjax] dovolíš zařadit i axiomy (resp. jestli je tam zařazuješ vždy). Pokud ano, pak z této definice důkazu plyne, že axiom je dokazatelný. Pokud tam axiomy nepovolíš zařadit, tak pak ale pokud je dokazatelné tvrzení A=>P, kde A je axiom, tak ale z toho odvozovacím pravidlem neodvodíš tvrzení P...

Axiomy podle mě mezi předpoklady zařadit musíš, protože jedno z odvozovacích pravidel přirozené dedukce je, že je-li odvoditelná implikace A=>P, pak je z A odvoditelné P (modus ponens). Takže je-li A axiom, musí být "přesunutelný" z implikace do předpokladů.

check_drummer napsal(a):

↑ Eratosthenes:
Ale obecně se i na metaúrovni tak nějak předpokládá, že máme "k dispozici" "libovolně mnoho" prvků (např. proměnných), tedy "potenciální nekonečno", podle mě si na metaúrovni s potenciálním nekonečnem vystačíš.

Toto je v pořádku. Když napíšeš "Matadefinice: ...bla,bla,bla... libovolně mnoho objektů... bla,bla,bla...", tak je to OK. Je to metadefinice, takže používá metapojmy, které (i když je to poněkud paradoxní) jsou intuitivní. Ale měly by být jednoduché natolik, aby jim rozumělo i dítě.

Definice každého pojmu obsahuje další pojmy, které by měly být definovány předtím. Jenže odněkud se začít musí, takže úplně všechno se precizně matematicky definovat nedá. Věděl to už Euklides, jenom nevěděl, jak z toho ven. Dnes už bychom to ale vědět měli.   

check_drummer napsal(a):

↑ Eratosthenes:
I když je pravda že včera jsem se dozvěděl, že model (pojem v logice) je množina, která je taky intuitivně chápaná a i tak může být nekonečná....

A to už je právě prů*er. V důsledku to totiž znamená, že v základech logiky, která má být jazykem precizní deduktivní matematiky, stojí intuitivní teorie množin, tedy i známé paradoxy, které najednou nevadí. To znamená, že axiomatickou teorii množin můžeme zahodit a vrátit se ke Cantorovi. Takže intuitivní a formální logika je principiálně úplně totéž a jediný rozdíl je v tom, že ta formální je zavalena tunami zcela zbytečného formalismu.

Někde jsem kdysi četl, že celá nádherná stavba matematiky stála na hromadě písku a že teprve formální logika jí poskytla pevné základy. Připadá mi to komické. Po mých zkušenostech s učebnicemi formální logiky si totiž myslím, že ta "skutečná" logika udělala jedinou věc. Celou budovu sice postavila na betonové základy, ale ty základy posadila do stejného písku, na kterém dřív stálo přízemí bez těch základů...

↑ MichalAld:

Z hlediska formální logiky (bohužel) ano.

Jak jsem psal výše, důkaz nějakého tvzení (formule F) je výpis formulí vzniklých přepisem předpokladů aplikováním odvozovacích pravidel tak, že poslední formulí je formule F.

Formule F: Prvočíslo má jen dva dělitele - jedničku a samo sebe.

Důkaz formule F: Prvočíslo má jen dva dělitele - jedničku a samo sebe.

Protože "dokazované"  tvrzení je axiom, přepisovat nic netřeba - je to předpoklad a dokazovaná formule zároveň, takže konec důkazu.

Podle mě je to na palici, ale z hlediska formální logiky je to bohužel tak.

Mně když dají linkovaný papír, píšu nejraději napříč linkami. Proto jsem kdesi výš napsal, že axiom je nedokazatelný, protože tento bizár podle mě důkaz není. Tím jsem prokázal absolutní neznalost základů logiky, takže mě neber moc vážně...

PS: Teď mě napadá - když i axiomy lze podle formální logiky dokázat, jak vlastně formální logika rozezná axiomy od ostatních (běžných) tvrzení (třeba matematických vět)?