Drejekors (symbol)
Turnstile |
⊢ |
|
|
højre tack |
Unicode |
U+22A2 |
HTML-kode |
eller |
UTF-16 |
0x22A2 |
|
%E2%8A%A2 |
Mnemonics |
⊢ ⊢ |
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".
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]
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
:
kan læses: "Jeg ved, at A er sand".
På samme måde en betinget erklæring
:
kan læses som:
"Fra
P ved jeg, at
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
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å
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]
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]
- 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]
- I kombinatorik betyder det, at det er en partition af tallet . [13]
- 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 .
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)
Links
Matematiske tegn |
---|
- Plus ( + )
- Minus ( - )
- Multiplikationstegn ( · eller × )
- Divisionstegn ( : eller / )
- Obelus ( ÷ )
- Rodtegn ( √ )
- Faktoriel ( ! )
- Integraltegn ( ∫ )
- Nabla ( ∇ )
- Lighedstegn ( = , ≈ , ≡ osv. )
- Ulighedstegn ( ≠ , > , < osv. )
- Proportionalitet ( ∝ )
- Klameparenteser ( ( ) , [ ] , ⌈ ⌉ , ⌊ ⌋ , { } , ⟨ ⟩ )
- Lodret streg ( | )
- Skråstreg, skråstreg ( / )
- Omvendt skråstreg, omvendt skråstreg ( \ )
- Uendelighedstegn ( ∞ )
- Gradtegn ( ° )
- Slagtilfælde ( ′ , ″ , ‴ , ⁗ )
- Stjerne ( * )
- Procent ( % )
- Ppm ( ‰ )
- Tilde ( ~ )
- Karet ( ^ )
- Circumflex ( ˆ)
- Plus-minus ( ± )
- Minus-plus tegn ( ∓ )
- Decimalseparator ( , eller . )
- Slut på bevistegn ( ∎ )
|
|