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:
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]
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.
Žádné komentáře:
Okomentovat