V matematické logice pojem axiomového schématu zobecňuje pojem axiomu .
Režim axiom je vzorec vyjádřené v metajazyka části s axiomatického systém , ve kterém jeden nebo více meta-proměnné objeví. Tyto proměnné, které jsou metalingvistickými konstrukty, představují jakýkoli termín nebo podformulář logického systému , který může (nebo nemusí) vyžadovat splnění určitých podmínek. Takové podmínky často vyžadují, aby některé z proměnných byly volné , nebo aby se některé proměnné neobjevily v podformuláři nebo výrazu.
Množství možných podformulí nebo termínů, které mohou dát metavariabilní hodnotě svou hodnotu, je spočítatelné nekonečné , schéma axiomu proto obecně představuje spočetnou nekonečnou množinu axiomů. Tuto sadu lze obecně definovat rekurzivně . Teorie, kterou lze axiomatizovat bez schématu, je považována za jemně axiomatizovatelnou . Ty jsou považovány za meta-matematicky elegantnější, i když jsou méně praktické pro deduktivní práci.
Dva velmi dobře známé příklady schémat axiomu jsou:
Bylo prokázáno (nejprve Richardem Montagueem ), že tyto vzorce nelze eliminovat. Aritmetika Peana a ZFC proto není definitivně axiomatizovatelná. To platí také pro mnoho dalších axiomů teorií matematiky, filozofie, lingvistiky atd.
Všechny věty o ZFC jsou také teoriemi von Neumann-Bernays-Gödelovy teorie množin , ale ta druhá je překvapivě dost jemně axiomatizovaná. Teorii nových základů lze také jemně axiomatizovat, ale pouze s určitou ztrátou elegance.
Logické metavariable prvního řádu jsou obecně triviálně odstranitelné v logice vyššího řádu , protože metavariable je často prostor věnovaný jakékoli vlastnosti nebo vztahu na prvcích teorie. To je případ výše zmíněných schémat indukce a výměny . Logika vyššího řádu umožňuje kvantifikovaným proměnným mít všechny vlastnosti nebo vztahy jako svoji doménu.