Bedømmelse (matematisk logik) - Judgment (mathematical logic)

For andre anvendelser, se dom (disambiguation) .

I matematisk logik er en dom (eller dom ) eller påstand en erklæring eller opsigelse i metasproget . For eksempel vil typiske vurderinger i førsteordens logik være, at en streng er en velformet formel , eller at en proposition er sand . Tilsvarende kan en dom hævde forekomsten af ​​en fri variabel i et udtryk for objektets sprog eller bevisligheden af ​​en proposition . Generelt kan en dom være en hvilken som helst induktivt definerbar påstand i metateorien .

Domme anvendes til formalisering af deduktionssystemer : et logisk aksiom udtrykker en dom, forudsætningerne for en slutningsregel dannes som en sekvens af domme, og deres konklusion er også en dom (således er hypoteser og konklusioner af bevis domme). Et karakteristisk træk ved varianterne af deduktionssystemer i Hilbert-stil er, at konteksten ikke ændres i nogen af ​​deres slutningsregler, mens både naturlig fradrag og sekventiel beregning indeholder nogle kontekstændrende regler. Således, hvis vi kun er interesserede i afledbarheden af tautologier og ikke hypotetiske domme, så kan vi formalisere Hilbert-stil-deduktionssystemet på en sådan måde, at dets slutningsregler kun indeholder vurderinger af en ret simpel form. Det samme kan ikke gøres med de to andre deduktionssystemer: Da kontekst ændres i nogle af deres slutningsregler, kan de ikke formaliseres, så hypotetiske vurderinger kunne undgås - ikke engang hvis vi ønsker at bruge dem kun til at bevise afledelighed af tautologier .

Denne grundlæggende mangfoldighed blandt de forskellige beregninger tillader en sådan forskel, at den samme grundlæggende tanke (f.eks. Deduktionssætning ) skal bevises som et metateorem i Hilbert-stil fradragssystem, mens det eksplicit kan erklæres som en slutningsregel ved naturlig deduktion .

I typeteori bruges nogle analoge forestillinger som i matematisk logik (hvilket giver anledning til forbindelser mellem de to felter, f.eks. Korry-Howard-korrespondance ). Abstraktionen i begrebet dom i matematisk logik kan også udnyttes i fundamentet for typeteori.

Se også

Referencer

  • Martin-Löf, Per (1996). "Om betydningen af ​​de logiske konstanter og begrundelsen for de logiske love" (PDF) . Nordisk tidsskrift for filosofisk logik . 1 (1): 11–60. ISSN   0806-6205 .
  • Dybjer, Peter. "Intuitionistisk type teori" . I Zalta, Edward N. (red.). Stanford Encyclopedia of Philosophy .
  • Pfenning, Frank ; Davies, Rowan (august 2001). "En fordømmende rekonstruktion af modalogik". Matematiske strukturer inden for datalogi . 11 (4): 511-540. CiteSeerX   10.1.1.43.1611 . doi : 10.1017 / S0960129501003322 .

eksterne links