Hát a Wiki egy kicsit elnagyoltan fogalmaz.
A régi görögök különbséget tettek a mindenki által evidensnek tartott kiindulópontok, az axiomák és az adott, éppen folyó vita céljaira elfogadott igazságok között (ezek az aktuális követelmények, vagy posztulátumok). Ez utóbbiakban a vita résztvevőinek nem kellett egyöntetűen hinniük, de kiváncsiak lehettek, hogy mire lehet velük jutni, ha fegyelmezetten végigvitték légyen a dolgokat.
Ma már a priori semmiben nem hiszünk. gligeti szavaival élve "mindent szana-szét relativizáltunk". Ennek megfelelően már nincs különbség axioma és posztulátum között, ahogy Gergő73 is megjegyzi.
Másrészről pedig a modern bizonyításelmélet kétféle "kiinduló igazságot" ismer:
(1) Bizonyos jelsorozatokat, amelyek nem "igazak" csak ki lehet indulni belőlük. (axiomák)
(2) Transzformációs szabályokat, amelyekkel a kiinduló jelsorozatokat manipulálni lehet, ill. a már "levezetett" jelsorozatokat tovább lehet masszírozni.
A jelsorozatoknak nincs jelentése. A jelek, amelyekből állnak a jelsorozatok adottak.
A nyelv amelyen elmondjuk, hogy mik a jelek, mik az axiomák és mik a transzformációs szabályok a metanyelv, amely nem tartozik az "elmélethez".
A levezetett jelsorozatokat lehet tételeknek nevezni.
Pl. Hofstadter (Gödel Escher Bach) a következő példát hozza:
Jelek: M, I, U.
Transzformációs szabályok:
(a) Ha xI egy tétel, akkor xIU is egy tétel. (x tetszőleges jelekből álló sorozat.)
(b) Ha Mx egy tétel, akkor Mxx is egy tétel.
(c) Ha III szerepel egy tételben, akkor III kicserélhető U-ra.
(d) Ha UU szerepel egy tételben, akkor elhagyható.
Axioma:
MI
Példa tétel és bizonyítása:
MUIIU
Axioma: MI
Innen (b) révén: MII.
Innen (b) révén: MIIII.
MIIII-ből MIIIIU, minthogy (a).
Innen (c) szerint MUIU.
Ennek megfelelően és mégegyszer (b): MUIUUIU.
És végül, erre (d)-t alkalmazva: MUIIU,
amit bizonyítani kellett.
- Ha az axiomák és a transzformációs szabályok "jelentenek" valamit , akkor megkérdezhető, hogy a levezetett tételek jelentése a várakozásoknak megfelel-e.
- Ha a jelek között van olyan, amelyet a bennfoglaló jelsorozat "tagadásaként" interpretálunk, akkor az elmélettel kapcsolatban feltehető a kérdés, hogy levezethető-e benne egyszerre egy tétel is és a tagadása is. Ha ez lehetséges, akkor felhúzzuk a szemöldökünket.
- A szemöldökfelhúzás nem része egyetlen elméletnek sem.
- Ha a jeleknek van jelentése, akkor megkérdezhető, hogy minden jelentéssel bíró jesorozat azok között a tételek között van-e, amelyek levezethetőek.
- Tovább most ne menjünk, mert nem fogok tudni aludni.