Logika, metalogika a metametalogika

Cíl je navrhnout kalkul použitelný nejen pro logiku, ale pro metalogiku, popř. pro metametalogiku. Návrh tohoto kalkulu vypadá následovně: Odvozovací systém pracuje s pravidly. Odvozovací systém umí pouze zaměnit proměnnou za jinou proměnnou, popř. výraz, a jsou-li splněny předpoklady pravidla a je-li o to žádán, pak vkládá do odvozených pravidel důsledek pravidla. Nic jiného odvozovací systém nedělá.

Pravidla logiky mají pouze důsledky. Jejich předpoklady jsou prázdné, a tedy vždy splněné. První pravidlo logiky je definice pravdy:

TI: A |- [\TRUE]

Proměnná A je proměnná seznamu výroků. Lomítko označuje konstantu. Seznam výroků má formu [a, b, c, ...]. Podle této definice je pravda to, co lze odvodit z každé teorie. Druhé pravidlo je definice nepravdy:

FI: [\FALSE] |- A

Nepravda je tedy to, z čeho lze odvodit každou teorii. Pokus o definici negace vypadá následovně:

NE: [not not a] |- [a]

Tato definice je zatím poněkud diskutabilní. Korektní definice logické spojky and, or, implikace a ekvivalence jsou tyto:

CI: [a, b] |- [a and b]
CE: [a and b] |- [a, b]
DI1: [a] |- [a or b]
DI2: [b] |- [a or b]
DE: [a or b, not b] |- [a]
II: [b] |- [a -> b]
MP: [a -> b, a] |- [b]
MT: [a -> b, not b] |- [not a]
EI: [(a -> b) and (b -> a)] |- [a <-> b]
EE: [a <-> b] |- [a -> b, b -> a]

Axiomy klasické výrokové logiky jsem vtělil do těchto logických pravidel:

PP1: |- [a -> (b -> a)]
PP2: |- [(a -> (b -> c)) -> ((a -> b) -> (a -> c))]
PP3: |- [(not a -> not b) -> (b -> a)]

Axiomy klasické predikátové logiky prvního řádu jsou tyto:

GQI: [SUB(a, x, t)] |- [forall(x, SUB(a, x, t))]
GQE: [forall(x, a)] |- [SUBST(a, x, t)]
EQI: [SUB(a, x, t)] |- [exists(x, SUB(a, x, t))]

SUB zde znamená substituci všech výskytů. Chybí tam ještě obecný případ eliminace existenčního kvantifikátoru. Pro jeho definování je zřejmě nutné zavést nějaký další metalogický prvek.

Zatímco dokazatelnost jsem značil |-, oddělovač předpokladu a důsledku značím ||=. Nemyslím tím sémantický důsledek, který se značí |=, a který nepoužívám. Následuje sada pravidel, které definují, co je dokazatelnost. Následující pravidlo říká, že ze souboru tvrzení lze dokázat jeho podsoubor:

It: A, B, C |- B

Toto pravidlo je jen obecnější forma známého pravidla [a] |- [a]. Můžeme-li něco dokázat, pak můžeme dokázat i o nějaký podsoubor méně:

OM: A |- B, C, D ||- A |- B, D

Pořadí tvrzení v seznamu můžeme zaměnit:

OI: A |- B, C, D, E, F ||- A |- B, E, D, C, F

Dokazatelné ze stejných předpokladů můžeme spojit:

Co: A |- B AND A |- C ||- A |- B, C

Kromě dokazatelnosti by bylo možné uvést i pravidla pro nedokazatelnost (značím |/-). Toto je jen návrh:

Ap1: [\TRUE] |- A ||- A |/- [\FALSE]
Ap2: A |/- B AND C |- A ||- C |/- B
Ap3: A |/- B ||- A |/- [\FALSE]
Ap4: A |/- B AND A |/- C ||- A |/- B, C
Ap5: A |/- B, C, D, E, F ||- A |/- B, E, D, C, F

Dále je možné definovat pravidla, která z definovaných pravidel umožňují odvodit nová pravidla. Jinými slovy: pravidla definující logiku pravidel. Je těžké rozhodnout, zda se ještě jedná o pravidla metalogické, nebo jsou to pravidla metametalogická. Záleží na použití. První pravidlo říká, že pravidla jsou tranzitivní:

MLTr: (A ||- B) AND (B ||- C) ||- (A ||- C)

Je-li pravidlo odvozující z pravidla A pravidlo B a z pravidla B pravidlo A, jsou pravidla záměnná:

MLSUB: (A ||- B) AND (B ||- A) AND C ||- SUB(C, A, B, I)

Proměnná I je proměnná za množinu přirozených čísel, které jsou indexy proměnných, které jsou substituovány. Metalogické AND a OR jsou komutativní:

MLCC: (A AND B) ||- (B AND A)
MLCD: (A OR B) ||- (B OR A)

Nadto platí:

MLDI: A ||- (A OR A)

Metalogické AND a OR mohou být za určitých okolností eliminovány:

MLDE: (A OR B) ||- A
MLCE: (A AND A) ||- A

Pravidlo lze pomocí AND zpřísnit:

MLCI: A ||- (A AND B)

Prázdný předpoklad je vždy splněn:

MLE1: A ||- (||- A)
MLE2: (||- A) ||- A

Nádavkem ještě pravidla o dokazatelnosti a předpokladech pravidel:

MLJo: (A ||- B |- C) AND (D ||- B |- E) ||- (A AND D ||- B |- C, E)
MLPr: (A ||- B |- C) AND (D ||- C |- E) ||- (A AND D ||- B |- E)

Bohužel, uvedený metalogický systém nedovoluje odvodit pravidla, která však odvoditelná jsou. Je to např. pravidlo o dedukci a jeho důsledek pravidlo o důkazu sporem. Lze je však dodefinovat:

Ded: A, [b], C |- [d] AND CLOSED(b) ||- A, C |- [b -> d]
Dis: A, [not b] |- \FALSE ||- A |- [b]

CLOSED(x) je relace, která je splněná, pokud je formule x uzavřená. Zatím je vše jenom v zárodku a bude třeba na tom ještě zapracovat.

David Hilbert o ignorabimus

Wir dürfen nicht denen glauben, die heute mit philosophischer Miene und überlegenem Tone den Kulturuntergang prophezeien und sich in dem Ignorabimus gefallen. Für uns gibt es kein Ignorabimus, und meiner Meinung nach auch für die Naturwissenschaft überhaupt nicht. Statt des törichten Ignorabimus heiße im Gegenteil unsere Losung: Wir müssen wissen, Wir werden wissen.

Neměli bychom věřit těm, kdo dnes s filosofickým nádechem a nadřazeností prorokují úpadek kultury a domýšlivě přijímají princip ignorabimus. Pro nás neexistuje žádné ignorabimus a podle mého názoru neexistuje ani pro přírodovědce. Místo bláhového ignorabimus, budiž naopak naším předsevzetím: Musíme vědět, budeme vědět.

Celý text je tady: http://www.jdm.uni-freiburg.de/JdM_files/Hilbert_Redetext.pdf
Vzácný zvukový proslovu je zde: http://math.sfsu.edu/smith/Documents/HilbertRadio/HilbertRadio.mp3

Plútarchos o matematice a mechanice

První, kdo zaměřil pozornost k oblíbené a slavné mechanice, byli Audoxos a Archytas, když dali pestrost a půvab abstraktní geometrii. Při logicky a konstruktivně nesnadném řešení problému si vypomáhali názorem na příkladech z mechaniky; tak například problém dvou středních úměrných, který je v mnoha příkladech základním prvkem pro kresliče, vyřešil oba pomocí mechanické konstrukce, přičemž z křivek a kuželoseček sestrojili tzv. mesolab. Avšak Platón jejich metody s rozhořčením odmítal, protože prý ničí a ruší největší přednost geometrie, která první uniká z oblasti nehmotných a abstraktních jevů do smyslového světa a znova se zaměstnává tělesy, která již sama o sobě vyžadují mnoho namáhavé řemeslnické činnosti. Tak byla mechanika oddělena od geometrie a také byla po dlouhý čas přezírána i filozofií a pokládána za odvětví válečné techniky.

Plútarchos – Životopisy slavných Řeků a Římanů

Problém dvou středních úměrných lze napsat do rovnice: 1/x = x/y = y/2. Zkonstruovat řešení pomocí pravítka a kružítka není možné.

Plútarchos

O málo světlých stránkách řeckého náboženství svědčí nejen samotná Iliada, ale i tento popis událostí při Xerxově vpádu:

τούτους ἰδὼν Εὐφραντίδης ὁ μάντις, ὡς ἅμα μὲν ἀνέλαμψεν ἐκ τω̂ν ἱερω̂ν μέγα καὶ περιφανὲς πυ̂ρ, ἅμα δὲ πταρμὸς ἐκ δεξιω̂ν ἐσήμηνε, τὸν Θεμιστοκλέα δεξιωσάμενος ἐκέλευσε τω̂ν νεανίσκων κατάρξασθαι καὶ καθιερευ̂σαι πάντας ὠμηστῃ̂ Διονύσῳ προσευξάμενον: οὕτω γὰρ ἅμα σωτηρίαν τε καὶ νίκην ἔσεσθαι τοι̂ς ̔́Ελλησιν. ἐκπλαγέντος δὲ του̂ Θεμιστοκλέους ὡς μέγα τὸ μάντευμα καὶ δεινόν, οἱ̂ον εἴωθεν ἐν μεγάλοις ἀγω̂σι καὶ πράγμασι χαλεποι̂ς, μα̂λλον ἐκ τω̂ν παραλόγων ἤ τω̂ν εὐλόγων τὴν σωτηρίαν ἐλπίζοντες οἱ πολλοὶ τὸν θεὸν ἅμα κοινῃ̂ κατεκαλου̂ντο φωνῃ̂ καὶ τοὺς αἰχμαλώτους τῳ̂ βωμῳ̂ προσαγαγόντες ἠνάγκασαν, ὡς ὁ μάντις ἐκέλευσε, τὴν θυσίαν συντελεσθη̂ναι.

Πλούταρχος – βιοι παραλλελοι

Ve chvíli, kdy je věštec Eufrantides spatřil, vzplála oběť velkým a jasným plamenem a zároveň bylo dáno znamení kýchnutím, které se ozvalo z pravé strany; Eufrantides podal proto Themistoklovi pravici a poručil mu, aby všechny tři jinochy zasvětil bohu a po modlitbě je věnoval masožravému Dionýsovi; tak se prý dostane Řekům záchrany a zároveň vítězství. Themistoklés se zděsil hrozné a neobyčejné věštby, lid však, který, jak tomu bývá ve velkém nebezpečí a za svízelných poměrů, očekával záchranu spíše od věcí nadpřirozených než rozumných, vzýval hromadně boha, přivlekl zajatce k oltáři a vynutil si, aby oběť byla vykonána podle věštcova příkazu.

Plútarchos – Životopisy slavných Řeků a Římanů