A deduktív Wiki elmélet
A formális rendszer (formális elmélet, axiomatikus elmélet, axiomatika, deduktív rendszer) az elmélet szigorú formalizálásának eredménye. amely teljes absztrakciót feltételez az alkalmazott nyelv szavaival kapcsolatban, és az elméletben ezeknek a szavaknak a használatára vonatkozó valamennyi feltételt kifejezetten az axiómák és szabályok fejezik ki, amelyek lehetővé teszik, hogy egy mondatot másoktól származtassanak [1].
A formális rendszer olyan absztrakt objektumok gyűjteménye, amelyek nem kapcsolódnak a külvilághoz, ahol a szimbólumkészlet szigorúan szintaktikai értelmezésére vonatkozó szabályok bemutatásra kerülnek, anélkül, hogy figyelembe vesszük a szemantikai tartalmat, vagyis a szemantikát. Szigorúan leírt formális rendszerek jelentek meg, miután Hilbert problémája merült fel. Az első FS megjelent a könyvek kiadása után Russell és Whitehead "Formális rendszerek" [tisztázni]. Ezt az FS-t bizonyos követelményeknek mutatták be.
Alapvető rendelkezések [. ]
A formális elmélet határozott, ha [2]:
- Megadható egy véges vagy megszámlálható szimbólumkészlet. A szimbólumok véges szekvenciáit az elmélet kifejezésének nevezik.
- Van egy kifejezésmódok egy részhalmaza.
- A képletek egy részhalmaza, az úgynevezett axiómák, különválasztják.
- A képletek közötti kapcsolatok véges sorozata, a következtetés szabályainak nevezik.
Általában van egy hatékony eljárás, amely lehetővé teszi számunkra, hogy ezzel a kifejezéssel határozzuk meg, hogy ez egy képlet. Gyakran előfordul, hogy egy képletkészlet egy induktív definícióval van megadva. Rendszerint ez a készlet végtelen. A szimbólumok és a képletek halmaza együttesen határozza meg a formális elmélet nyelvét vagy aláírását.
Mindegyik R származtatási szabályra és minden egyes A képletre hatásosan megoldódik, hogy a választott képletek R-rel kapcsolatban vannak-e az A. képlet szerint. Ha igen, akkor az A szabályt az említett képlet azonnali következménye adja.
A származék bármelyik olyan képletsorozat, amelynél a szekvencia minden formulája vagy egy axióma vagy egy korábbi képlet közvetlen következménye az egyik következtetési szabály szerint.
A képletet tételnek nevezik. ha van egy következtetés, amelyben ez a képlet az utolsó.
Olyan elmélet, amelynek létezik egy hatékony algoritmus, amely lehetővé teszi, hogy ezzel a formulával felismerje, hogy a következtetése létezik-e megoldhatónak; különben az elméletet eldönthetetlennek nevezik.
Olyan elmélet, amelyben nem minden képlet tétel, teljesen következetes.
Fogalommeghatározás és fajták [| ]
A deduktív elméletet akkor kell figyelembe venni, ha:
- Az ábécé (készlet) és a kifejezés (szavak) kialakításának szabályai ebben az ábécében kerülnek meghatározásra.
- A formulák kialakulására vonatkozó szabályokat (helyesen szerkesztett, helyes kifejezések) adják meg.
- A képletek csoportjától a T tételek (bizonyítható képletek) részhalmaza valamilyen módon megkülönböztethető.
A deduktív elméletek fajtái [| ]
Attól függően, hogy a tételek sorozata hogyan épül fel:
Axiómák és következtetési szabályok hozzárendelése [| ]
Az axiómák egy részhalmaza megkülönböztetődik a képletekben, és véges számú következtetési szabályt definiálnak, amelyek segítségével (és csak segítségükön keresztül) új tételek alakíthatók ki az axiómákból és az előzőleg előterjesztett tételekből. Az összes axiómák szintén a tételek közé tartoznak. Néha (például Peano axiomatikájában) az elmélet végtelen számú axiómát tartalmaz, amelyet egy vagy több axióma-séma ad. Az axiómákat néha "rejtett meghatározásoknak" nevezik. Ily módon formális elmélet definiálható (formális axiomatikus elmélet, formális (logikai) kalkulus).
Csak az axiómák hozzárendelése [| ]
Csak az axiómák vannak megadva, a következtetés szabályai általában ismertek.
Példák [| ]
Csak kimeneti szabályok megadása [| ]
Nincs axióma (az axiómák halmaza üres), csak a következtetés szabályait adják meg.
Tény, hogy az így adott elmélet egy különleges eset egy formális, de saját nevével: a természetes következtetés elmélete.
A deduktív elméletek tulajdonságai [| ]
Összhang [| ]
Egy olyan elmélet, amelyben egy sor tétel lefedi a képletek egész sorát (minden képlet tétel, "igazmondás") ellentmondásosnak. Ellenkező esetben az elméletet következetesnek hívják. Az elmélet ellentmondásos természetének eloszlása a formális logika egyik legfontosabb és néha legbonyolultabb feladata. Az inkonzisztencia tisztázása után az elméletnek, mint általában, nincs további elméleti vagy gyakorlati alkalmazása.
Teljesség [| ]
Az elméletet teljesnek nevezik. ha egy mondatban (zárt képlet) F vagy F maga származtatható. vagy tagadása # x00AC; F. Ellenkező esetben az elmélet nem bizonyítható állításokat tartalmaz (olyan állításokat, amelyeket maga az elmélet sem bizonyíthat és nem is vitathat), és nem teljes.
Axiómák függetlensége [| ]
Az elmélet külön axióma függetlennek tekinthető. Ha ez axióma nem származhat a maradék axiómákból. A függő axióma lényegében redundáns, és eltávolítása az axióni rendszerből semmilyen módon nem érinti az elméletet. Az elmélet teljes axiómáinak rendszere független. ha mindegyik axiómája független.
Megoldhatóság [| ]
Az elmélet megoldható. Ha a tétel fogalma hatékonyan működik benne. azaz létezik egy hatékony folyamat (algoritmus), amely lehetővé teszi bármelyik képlet véges számú lépésben annak meghatározását, hogy ez egy tétel vagy sem.
A legfontosabb eredmények [| ]
- A 30-as években. A XX. Században Kurt Gödel megmutatta, hogy az elsőrendű elméletek egész osztálya hiányos. Továbbá az elmélet konzisztenciáját alátámasztó képlet szintén nem származhat önmagában az elmélet segítségével (lásd Gödel hiányossági tételeit). Ez a következtetés nagy jelentőséggel bír a matematika számára, mivel a formális aritmetika (és minden olyan elmélet, amely alfejezetként tartalmazza) az első rend ilyen elmélete, ezért hiányos.
- Ennek ellenére a valóságos zárt mezők elmélete [en] kiegészítéssel, szorzással és rendelési kapcsolatban teljes (Tarski-Seidenberg tétel).
- A szerző bizonyítja, hogy nincs olyan algoritmus, amely a predikátum logikájának bármely formulájára megállapítja, hogy a képlet logikailag érvényes-e vagy sem.
- A kimutatások kalkulációja konzisztens, teljes, megoldható elmélet.