턴스타일(기호)

수학 논리학과 컴퓨터 과학에서 기호 ${\(\displaystyle\vdash)$ 는 $\vdash$ 위에서 볼 때 전형적인 개찰구와 비슷하기 때문에 개찰구라는 이름을 얻었다.티(tee)라고도 하며 종종 "수율", "프로브", "만족" 또는 "엔테일"로 읽힌다.

해석

개찰구는 이항 관계를 나타냅니다.다른 컨텍스트에서 다음과 같은 해석이 있습니다.

인식론에서 Per Martin-Löf(1996)는 다음과 같이 $:$ 기호(\ $displaystyle\vdash)$ 를 $\vdash$ 분석한다.[T]Frege의 Urteilsstrich, 판단 스트로크 [ ], 내용 스트로크 [--]의 조합은 어설션 ^[1]기호로 불리게 되었습니다.일부 $내용$ A에 대한 판단을 위한 Frege 표기법

\displaystyle \vdash A

그러면 읽을 수 있다

A가 ^[2]사실인 건 $알아$ .

같은 맥락에서 조건부 주장

P\vdash Q

다음과 같이 읽을 수 있습니다.

$P$ 부터, 나는 Q를 $안다$ .

금속학에서, 형식 언어에 대한 연구; 개찰구는 통사적 결과(또는 "유도성")를 나타냅니다.즉, 특정 공식 ^[3]시스템의 변환 규칙(즉, 구문)에 따라 한 문자열이 한 단계로 다른 문자열에서 파생될 수 있음을 나타냅니다.그래서 표현은

P\vdash Q

Q가 시스템 내의 P에서

파생

되는 것을

의미

합니다.

파생성에 대한 그것의 사용과 일관되게, 앞에 아무것도 없는 식 뒤에 오는 """은 공리 집합을 사용하여 규칙에서 식을 도출할 수 있는 정리를 나타낸다.그래서 표현은

{\displaystyle\vdashQ}

즉

, Q는 시스템 내의 정리입니다.

증명 이론에서 개찰구는 "가능성" 또는 "파생 가능성"을 나타내기 위해 사용됩니다.예를 들어, $만약$ T가 형식 $이론$ 이고 S가 이론의 언어에서 특정한 문장이라면,

T\vdash S

S가 ^[4]

T

로부터 증명 가능함을

의미

합니다.이 용법은 명제 미적분에 관한 기사에서 입증되었다.입증성의 구문적 결과는 이중 턴스타일 기호

{\

{\

displaystyle \models

로 나타나는 의미적 결과와 대조되어야 한다. 사람들은 S

{\

displaystyle

S

}

가

S

가능한 경우 T

{\

displaystyle

T

}

T\models S

T

T\models S

S {\

displaystyle

S

T\models S

의

의미적

결과라고

말한다

.

(Displaystyle

T

)

는

T

맞다.

(Displaystyle

S

)

도

S

맞다.명제 로직의 경우 의미론적 결과 δ

\displaystyle \models }

와

\models

파생성

\vdash

δ\

displaystyle \vdash

}가

\vdash

서로 동등함을 나타낼 수 있다.즉, 명제의 로직은 건전합니다

\vdash

(<

displaystyle

\

vdash

>

\models

）

。

완전

합니다

(<

displaystyle

\

models

>

）

。{

displaystyle

\

vdash

^[5] ）。

순차 미적분학에서 턴스틸은 시퀀스를 나타내기 위해 사용된다. $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ 1, $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ B $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ 1, $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ B $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ \ $displaystyle A_{1},$ \ $dots, A_{m},$ \ $vdash, B_{1},$ \ $dots, B_{n}$ 는 $A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}$ 모든 선행 $A_{1},\,\dots ,A_{m}$ A $A_{1},\,\dots ,A_{m}$ , $A_{1},\,\dots ,A_{m}$ { $A$ }, \ dots, \ $dots$ , \ dots, A { $1},$ A, A, A, A, A, $B_$ {dots}, A, A, A, A, A, dots, display, A, A, dots, dots, dots, A,{ $n}}$ 은 $B_{1},\,\dots ,B_{n}$ (는) 참이어야 합니다 $.$
타이핑 ^[6]^[7]람다 미적분에서는 턴스틸이 타이핑 판단에서 타이핑 가정을 분리하기 위해 사용된다.
로 G⊢ F{G\vdash F\displaystyle}에서 함수 기호 G나를 표시하는데 사용되는 범주론, 쳐진 개찰구(⊣{\displaystyle \dashv}),에서 ⊣ G{\displaystyle F\dashv G}F과 마찬가지로 함수 기호 G.[8]모어는 구조 함수 F은 왼쪽 수반할 수 없는 회전문(⊢{\displaystyle \vdash})을 나타내기 위해 사용된다sr $펑터$ ^[9]F에 인접한다.
APL에서 이 기호는 "오른쪽 택"이라고 불리며 $XyY$ 와 $θY$ 가 $모두$ $Y$ 인 양가의 오른쪽 항등함수를 나타냅니다.역기호 「"」는 「왼쪽 택」이라고 불리며, $XyY$ 는 $X$ , $yY$ 는 ^[10]^[11] $Y$ 라고 하는 $유사$ 한 왼쪽 항등식을 나타낸다.
콤비네이터학에서 $\lambda \vdash n$ n \ $displaystyle$ \ $lambda$ \ $vdash$ n $은$ $\lambda \vdash n$ $θ$ ^[12]가 정수 n 의 파티션임을 의미합니다.
Hewlett-Packard의 HP-41C/CV/CX 및 HP-42S 시리즈의 계산기에서는 기호(FOCAL 문자 집합의 코드 포인트 127)는 "추가 문자"라고 불리며 레지스터의 기존 내용을 대체하는 대신 다음 문자가 알파벳 레지스터에 추가됨을 나타내기 위해 사용됩니다.이 기호는 다른 HP 계산기에서 사용되는 HP Roman-8 문자 세트의 변형에서도 지원됩니다(코드 포인트 148).
Casio fx-92 Collége 2D 및 fx-92+ Spéciale Collége 계산기에서 ^[13]기호는 모듈로 연산자를 나타냅니다. $5$ $5\vdash 2$ (\ $displaystyle$ 5 $\vdash$ 2)를 $5\vdash 2$ $Q=2;R=1$ 하면 Q $Q=2;R=1$ ; R $=$ (\ $displaystyle$ Q $= 2$ ; $R$ $）$ 。다른 CASIO 계산기(예를 들어 벨기에 변형인 fx-92B Spéciale Collége 및 fx-92B Collége 2D 계산기^[14](여기서 소수 구분자는 쉼표가 아닌 점으로 표시됨)에서는 모듈로 연산자가 대신 δR로 표시됩니다.

타이포그래피

TeX에서 턴스타일 기호 $\vdash$ {\(\ $displaystyle \vdash)$ 은 $\vdash$ 명령에서 가져옵니다.\vdash.

유니코드에서는 턴스타일 기호())를 오른쪽 택이라고 하며 코드 포인트 U+22A2에 ^[15]있습니다.(코드 포인트 U+22A6는 어설션 부호())라고 불립니다).

U+22A2 right RIGHT TACK ( & RightTee ; , & vdash ; )
- = 개찰구
- =는 생산량을 증명합니다.
- = 환원 가능
U+22A3 left LEFT TACK (&dashv;, &LeftTee;)
- = 역회전 개찰구
- = 비고정, 산출되지 않음
U+22AC does증명되지 않음(&nvdash;)
- [22A2] 0338$]

타이프라이터에서 턴스타일은 세로 막대( )와 대시(–)로 구성할 수 있습니다.

LaTeX에는 여러 가지 방법으로 이 표지판을 발행하고 그 아래 또는 위에 올바른 ^[16]위치에 라벨을 부착할 수 있는 턴스타일 패키지가 있습니다.

유사 자모양

§ (U+A714) 수식자 문자(왼쪽 줄기의 중간 톤 바)
§ (U+251C) 박스 도면 라이트 수직 및 우측
§ (U+314F) 한글 문자 A
δ (U+0370) 그리스 대문자 헤타
§ (U+0371) 그리스어 작은 글자 헤타
ⱶ ( U + 2C75 )라틴 대문자 하프 H
§ (U+2C76) 라틴어 소문자 하프 H
§ (U+23AC) 우측 컬리 브래킷 미들피스

「」를 참조해 주세요.

메모들

^ 마틴-뢰프 1996, 6, 15페이지
^ 마틴-뢰프 1996, 페이지 15
^ "Chapter 6, Formal Language Theory" (PDF).
^ Troelstra & Schwichtenberg 2000
^ Dirk van Dalen, 논리 및 구조(1980), 스프링어, ISBN 3-540-20879-8.1장, 섹션 1.5를 참조하십시오.
^ "Peter Selinger, Lecture Notes on the Lambda Calculus" (PDF).
^ 슈미트 1994
^ "adjoint functor in nLab". ncatlab.org.
^ @FunctorFact (5 July 2016). "Functor Fact on Twitter" (Tweet) – via Twitter.
^ "A Dictionary of APL". www.jsoftware.com.
^ 아이버슨 1987
^ Stanley, Richard P. (1999). Enumerative Combinatorics. Vol. 2 (1st ed.). Cambridge: Cambridge University Press. p. 287.
^ fx-92 Spéciale Collège Mode d'emploi (PDF). CASIO COMPUTER CO., LTD. 2015. p. 12.
^ "Remainder Calculations - Casio fx-92B User Manual [Page 13] ManualsLib". www.manualslib.com. Retrieved 2020-12-24.
^ "Unicode standard" (PDF).
^ "CTAN: /tex-archive/macros/latex/contrib/turnstile". ctan.org.

레퍼런스

Frege, Gottlob (1879). "Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens". Halle. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
Iverson, Kenneth (1987). "A Dictionary of APL". {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
Martin-Löf, Per (1996). "On the meanings of the logical constants and the justifications of the logical laws" (PDF). Nordic Journal of Philosophical Logic. 1 (1): 11–60. (Université degli Studi di Siena, 1983년 4월)의 짧은 코스에 대한 강의 노트.
Schmidt, David (1994). The Structure of Typed Programming Languages. MIT Press. ISBN 0-262-19349-3.
Troelstra, A. S.; Schwichtenberg, H. (2000). Basic Proof Theory (2nd ed.). Cambridge University Press. ISBN 978-0-521-77911-1.

[1] 마틴-뢰프 1996, 6, 15페이지

[2] 마틴-뢰프 1996, 페이지 15

[3] "Chapter 6, Formal Language Theory" (PDF).

[4] Troelstra & Schwichtenberg 2000

[5] Dirk van Dalen, 논리 및 구조(1980), 스프링어, ISBN 3-540-20879-8.1장, 섹션 1.5를 참조하십시오.

[6] "Peter Selinger, Lecture Notes on the Lambda Calculus" (PDF).

[7] 슈미트 1994

[8] "adjoint functor in nLab". ncatlab.org.

[9] @FunctorFact (5 July 2016). "Functor Fact on Twitter" (Tweet) – via Twitter.

[10] "A Dictionary of APL". www.jsoftware.com.

[11] 아이버슨 1987

[12] Stanley, Richard P. (1999). Enumerative Combinatorics. Vol. 2 (1st ed.). Cambridge: Cambridge University Press. p. 287.

[13] fx-92 Spéciale Collège Mode d'emploi (PDF). CASIO COMPUTER CO., LTD. 2015. p. 12.

[14] "Remainder Calculations - Casio fx-92B User Manual [Page 13] ManualsLib". www.manualslib.com. Retrieved 2020-12-24.

[15] "Unicode standard" (PDF).

[16] "CTAN: /tex-archive/macros/latex/contrib/turnstile". ctan.org.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

Search

턴스타일(기호)

네임스페이스

더

목차

해석

타이포그래피

유사 자모양

「」를 참조해 주세요.

메모들

레퍼런스

Search

턴스타일(기호)

해석

타이포그래피

유사 자모양

「 」를 참조해 주세요.

메모들

레퍼런스

「」를 참조해 주세요.