Vändkors (symbol)

Spärr
⊢
◄ ⊞ ⊟ ⊠ ⊡ ⊢ ⊣ ⊤ ⊥ ⊦ ►
Egenskaper
namn höger stift
Unicode U+22A2
HTML-kod ⊢ eller ⊢
UTF-16 0x22A2
URL-kod %E2%8A%A2
Mnemonics ⊢
⊢

Vändkors  − Inom matematisk logik och datavetenskap kallas symbolen en "vändkors" på grund av dess likhet med en typisk vändkors , när den ses ovanifrån. Det kallas också "tee" och läses ofta som "ger", "bevisar", "tillfredsställer" eller "medför".

I TeX erhålls vändkorssymbolen från kommandot \vdash . I Unicode kallas vändkorset ( \vdash ) för "högerknapp" och är i kodposition U+22A2 [1] . Kodposition U+22A6 kallas för påståendetecknet ( \vdash ). På en skrivmaskin kan ett vändkors bestå av en vertikal stång (|) och ett streck (-). LaTeX har ett vändkorspaket som producerar denna karaktär i många fall och kan placera tecken under eller ovanför den på rätt ställen. [2]

Betydelse

Vändkorset är en binär relation . Dess tolkning av är olika i olika sammanhang:

:

kan läsas: "Jag vet att A är sant".

I samma veva ett villkorligt uttalande :

kan läsas som:

"Från P vet jag att Q " betyder att Q är härledbart från P i systemet. Enligt dess användning för härledning, följt av ett uttryck utan att något föregår det, betecknar det en sats , det vill säga uttrycket kan härledas från reglerna med hjälp av den tomma uppsättningen av axiom . Som sådant uttrycket betyder att Q är ett teorem i systemet. betyder att S är bevisbart från T . [5] Denna användning demonstreras i artikeln om propositionell logik . Den syntaktiska konsekvensen av bevisbarhet bör kontrasteras med den semantiska konsekvensen som betecknas med den dubbla vändkorssymbolen . Det står att det är den semantiska konsekvensen av , eller , när alla möjliga utvärderingar som är sanna också är sanna. För propositionell logik kan det visas att semantisk konsekvens och härledning är likvärdiga med varandra. Det vill säga, propositionell logik är sund ( antyder ) och fullständig ( implicerar ). [6]

med funktoren G . [9] I sällsynta fall används vändkorset ( ), som i , för att indikera att funktorn G är direkt intill funkorn F . [tio]

  • I APL kallas symbolen "right tack" och representerar den ambivalenta rätta identitetsfunktionen, där och , och är . Den omvända symbolen kallas "left tack" och representerar en liknande vänsteridentitet, där  är och  är . [11] [12]
  • I kombinatorik betyder det att det är en partition av talet . [13]
  • I Hewlett-Packards räknare i serierna HP-41C och HP-42S [ kallas tecknet (vid kodpunkt 127) i FOCAL-teckenuppsättningen ) "Add Character" och används för att indikera att följande tecken kommer att läggas till i alfaregistret, istället för att ersätta det befintliga innehållet i registret. Detta tecken stöds också (vid kodpunkt 148) i en modifierad variant av typsnittet HP Roman som används i andra HP-räknare.
  • I Casios fx-92 College 2D och fx-92+ Speciale College serier räknare, [14] står symbolen för moduloperatorn ; ingången kommer att visas , där Q är kvoten och R är resten . I andra CASIO-räknare (som de belgiska varianterna - fx-92B Speciale College och fx-92B College 2D-räknare [15] - där decimalavgränsaren representeras av en punkt istället för ett komma), betecknas modulo-operatorn som .

Se även

Anteckningar

  1. ↑ Unicode-standard . Hämtad 16 maj 2021. Arkiverad från originalet 13 maj 2011.
  2. ↑ CTAN Comprehensive TEX Archive Network, Directory - makron/latex/contrib/turnstile . Hämtad 16 maj 2021. Arkiverad från originalet 17 maj 2021.
  3. ↑ Martin-Lof, 1996 , s. 6, 15
  4. ↑ Kapitel 6, Formell språkteori . Hämtad 16 maj 2021. Arkiverad från originalet 4 april 2018.
  5. ↑ Troelstra & Schwichtenberg, 2000
  6. ↑ Dirk van Dalen, Logic and Structure (1980), Springer, ISBN 3-540-20879-8 . Se kapitel 1, avsnitt 1.5.
  7. ↑ Peter Selinger, föreläsningsanteckningar om lambdakalkylen . Hämtad 16 maj 2021. Arkiverad från originalet 6 maj 2021.
  8. ↑ Schmidt, 1994
  9. ↑ adjoint funktor i nLab . Hämtad 16 maj 2021. Arkiverad från originalet 13 maj 2021.
  10. ↑ FunctorFact. Functor Fact på Twitter . [tweet] . Twitter (5 juli 2016) .
  11. ↑ Iverson, APL-ordbok . Hämtad 16 maj 2021. Arkiverad från originalet 25 april 2020.
  12. ↑ Iverson, 1987
  13. ↑ Stanley, Richard P. Enumerative Combinatorics. — 1:a. - Cambridge: Cambridge University Press, 1999. - Vol. Vol. 2. - S. 287.
  14. ↑ fx-92 Special College Mode d'emploi . - CASIO COMPUTER CO., LTD., 2015. - P. 12. Arkiverad 16 april 2021 på Wayback Machine
  15. ↑ Återstående beräkningar - Casio fx-92B Användarmanual [Sida 13 | ManualsLib] . www.manualslib.com . Hämtad 24 december 2020. Arkiverad från originalet 16 maj 2021.

Länkar