Rozsudek (matematická logika) - Judgment (mathematical logic)
V matematické logice je úsudek (nebo úsudek ) nebo tvrzení výrokem nebo výrokem v metajazyku . Například typické úsudky v logice prvního řádu by byly, že řetězec je dobře vytvořený vzorec , nebo že je věta pravdivá . Podobně může úsudek tvrdit výskyt volné proměnné ve výrazu objektového jazyka nebo prokazatelnost výroku . Obecně platí, že úsudkem může být jakékoli induktivně definovatelné tvrzení v metateorii .
Rozsudky se používají při formování dedukčních systémů : logický axiom vyjadřuje úsudek, premisa pravidla závěru se tvoří jako posloupnost úsudků a jejich závěrem je také úsudek (hypotézy a závěry důkazů jsou tedy úsudky). Charakteristickým rysem variant dedukčních systémů ve stylu Hilberta je, že kontext se nemění v žádném z jejich pravidel odvození, zatímco jak přirozená dedukce, tak sekvenční počet obsahují některá pravidla měnící kontext. Takže pokud nás zajímá pouze v derivability z tautologie , nikoliv hypotetické soudy, pak můžeme formalizovat systém odpočtů Hilbert styl takovým způsobem, že jeho pravidla závěru obsahovat pouze rozsudky poměrně jednoduchého formuláře. Totéž nelze udělat s dalšími dvěma systémy dedukcí: jelikož se kontext mění v jejich pravidlech závěrů, nelze je formalizovat, aby bylo možné se vyhnout hypotetickým úsudkům - a to ani v případě, že je chceme použít pouze k prokázání odvoditelnosti tautologií .
Tato základní rozmanitost mezi různými kameny umožňuje takový rozdíl, že stejná základní myšlenka (např. Věta o dedukci ) musí být prokázána jako metateorem v dedukčním systému ve stylu Hilberta, zatímco v přirozené dedukci může být výslovně deklarována jako pravidlo závěru .
V teorii typů se používají některé analogické pojmy jako v matematické logice (což vede ke spojení mezi těmito dvěma poli, např. Korespondence Curry – Howard ). Abstrakci v pojmu úsudku v matematické logice lze využít také při založení teorie typů.
Viz také
Reference
- Martin-Löf, Per (1996). „O významech logických konstant a důvodech logických zákonů“ (PDF) . Severský žurnál filozofické logiky . 1 (1): 11–60. ISSN 0806-6205 .
- Dybjer, Peter. "Intuicionistická teorie typů" . V Zalta, Edward N. (ed.). Stanfordská encyklopedie filozofie .
- Pfenning, Frank ; Davies, Rowan (srpen 2001). "Rozsudková rekonstrukce modální logiky". Matematické struktury v informatice . 11 (4): 511–540. CiteSeerX 10.1.1.43.1611 . doi : 10.1017 / S0960129501003322 .
externí odkazy
- "Rozsudky ve formálních systémech" . Všechno 2 .
- Pfenning, Frank (jaro 2004). „Přírodní odpočet“ (PDF) . 15-815 Automatické prokazování věty .
- Martin-Löf, Per (1983). "O významu logických konstant a odůvodnění logických zákonů" . Siena Přednášky .