Drejekors (symbol)

Turnstile

⊢

◄

⊞

⊟

⊠

⊡

⊢

⊣

⊤

⊥

⊦

►

Egenskaber

Navn

højre tack

Unicode

U+22A2

HTML-kode

⊢ eller ⊢

UTF-16

0x22A2

URL-kode

%E2%8A%A2

Mnemonics

&RightTee;
&vdash;

Drejekors − Inden for matematisk logik og datalogi kaldes symbolet for en "turnstile" på grund af dets lighed med en typisk turnstile , set fra oven. Det omtales også som "tee" og læses ofte som "giver", "beviser", "tilfredsstiller" eller "medfører". $\vdash$

I TeX hentes drejekorssymbolet fra kommandoen \vdash . I Unicode kaldes drejekorset ( \vdash ) "højre knap" og er i kodeposition U+22A2 [1] . Kodeposition U+22A6 kaldes påstandstegnet ( \vdash ). På en skrivemaskine kan et drejekors bestå af en lodret stang (|) og en bindestreg (-). LaTeX har en drejekorspakke, der producerer denne karakter i mange tilfælde og er i stand til at placere tegn under eller over den på de rigtige steder. [2] $\vdash$

Betydning

Drejekorset er en binær relation . Dens fortolkning af er forskellig i forskellige sammenhænge:

I epistemologi analyserer Per Martin-Lough (1996) symbolet på denne måde: ”...Kombination af Freges dømmekraft | og et strejf af indhold - det blev kendt som et tegn på godkendelse. [3] Freges notation for dom af noget indhold A $\vdash$

\vdash A

kan læses: "Jeg ved, at A er sand".

På samme måde en betinget erklæring

P\vdash Q

kan læses som:

"Fra P ved jeg, at Q "

I metalogisk , i konstruktionen af formelle sprog , repræsenterer en drejekors en slutning (eller "deducibility"). Dette betyder, at det viser, at en streng kan fås fra en anden i ét trin i henhold til transformationsreglerne (dvs. syntaks ) for et givet formelt system . [4] Som sådan er udtrykket

P\vdash Q

betyder, at Q kan udledes af P i systemet. Ifølge dets brug for udledning, efterfulgt af et udtryk uden noget forudgående angiver det en sætning , det vil sige, at udtrykket kan udledes fra reglerne ved hjælp af det tomme sæt af aksiomer . Som sådan udtrykket

\vdash

\vdash Q

betyder, at Q er en sætning i systemet.

I bevisteori bruges drejekorset til at betegne "bevisbarhed" eller "afledningsevne". For eksempel, hvis T er en formel teori , og S er en konkret sætning i teorisproget, så

T\vdash S

betyder, at S kan bevises fra T . [5] Denne brug er demonstreret i artiklen om propositionel logik . Den syntaktiske konsekvens af bevisbarhed bør kontrasteres med den semantiske konsekvens, der er angivet med det dobbelte drejekorssymbol . Det siger, at det er den semantiske konsekvens af , eller , når alle mulige evalueringer , der er sande, også er sande. For propositionel logik kan det påvises, at semantisk konsekvens og udledning er ækvivalente med hinanden. Det vil sige, at propositionel logik er sund ( antyder ) og fuldstændig ( antyder ). [6]

\modeller

S

T

T\models S

T

S

\modeller

\vdash

\vdash

\modeller

\modeller

\vdash

I den maskinskrevne lambdaregning bruges drejekorset til at adskille maskinskrivningsantagelser fra maskinskrivningsdomme. [7] [8]
I kategoriteori bruges den omvendte drejekors ( ), som i , til at indikere, at funktoren F forbliver adjoint $\dashv$ $F\dashv G$

med funktoren G . [9] I sjældnere tilfælde bruges drejekorset ( ), som i , til at indikere, at funktoren G er direkte stødende op til funktoren F . [ti] $\vdash$ $G\vdash F$

I APL kaldes symbolet "right tack" og repræsenterer den ambivalente højre identitetsfunktion, hvor og , og er . Det omvendte symbol kaldes "venstre tack" og repræsenterer en lignende venstre identitet, hvor er og er . [11] [12] $X\vdash Y$ $\vdash Y$ $Y$ $\dashv$ $X\dashv Y$ $x$ $\dashv Y$ $Y$
I kombinatorik betyder det, at det er en partition af tallet . [13] $\lambda \vdash n$ $\lambda$ $n$
I Hewlett-Packards HP-41C og HP-42S serie lommeregnere kaldes tegnet (ved kodepunkt 127) i FOCAL-tegnsættet ) "Add Character" og bruges til at angive, at følgende tegn vil blive tilføjet til alfa-registret i stedet for at erstatte det eksisterende indhold af registret. Dette tegn er også understøttet (ved kodepunkt 148) i en modificeret variant af HP Roman -skrifttypen , der bruges i andre HP-beregnere.
I Casios fx-92 College 2D- og fx-92+ Speciale College-serieregnere [14] står symbolet for modulusoperatoren ; inputtet vises , hvor Q er kvotienten og R er resten . I andre CASIO-beregnere (såsom de belgiske varianter - fx-92B Speciale College og fx-92B College 2D-beregnere [15] - hvor decimalseparatoren er repræsenteret med en prik i stedet for et komma), er modulo-operatoren angivet som . $5\vdash 2$ $Q=2;R=1$ $\div R$

Se også

Noter

↑ Unicode-standard . Hentet 16. maj 2021. Arkiveret fra originalen 13. maj 2011. (ubestemt)
↑ CTAN Comprehensive TEX Archive Network, Directory - makroer/latex/contrib/turnstile . Hentet 16. maj 2021. Arkiveret fra originalen 17. maj 2021. (ubestemt)
↑ Martin-Lof, 1996 , s. 6, 15
↑ Kapitel 6, Formel sprogteori . Hentet 16. maj 2021. Arkiveret fra originalen 4. april 2018. (ubestemt)
↑ Troelstra & Schwichtenberg, 2000
↑ Dirk van Dalen, Logic and Structure (1980), Springer, ISBN 3-540-20879-8 . Se kapitel 1, afsnit 1.5.
↑ Peter Selinger, Forelæsningsnoter om lambdaregningen . Hentet 16. maj 2021. Arkiveret fra originalen 6. maj 2021. (ubestemt)
↑ Schmidt, 1994
↑ adjoint functor i nLab . Hentet 16. maj 2021. Arkiveret fra originalen 13. maj 2021. (ubestemt)
↑ FunctorFact. Functor Fact på Twitter . [tweet] . Twitter (5. juli 2016) . (ubestemt)
↑ Iverson, APL-ordbog . Hentet 16. maj 2021. Arkiveret fra originalen 25. april 2020. (ubestemt)
↑ Iverson, 1987
↑ Stanley, Richard P. Enumerative Combinatorics. — 1. - Cambridge: Cambridge University Press, 1999. - Vol. Vol. 2. - S. 287.
↑ fx-92 Speciale College Mode d'emploi . - CASIO COMPUTER CO., LTD., 2015. - S. 12. Arkiveret 16. april 2021 på Wayback Machine
↑ Resterende beregninger - Casio fx-92B Brugervejledning [Side 13 | ManualsLib] . www.manualslib.com . Hentet 24. december 2020. Arkiveret fra originalen 16. maj 2021. (ubestemt)

Drejekors (symbol)

Betydning

Se også

Noter

Links