연역논증할때 쓰는 이런 식구조를 뭐라고 함?

[익명(219.250)]

저렇게 조건식같은 논리연산을 연역논증할때 

순서대로 추론규칙을 적용해가면서 마지막에 길다란 바 밑으로 결론을 도출하는 저런 형태의 식 구조를 뭐라고 함?

어디서는 논리 형식(logical form)이라고 하기도 하는거같은데 맞는지 모르겠음

제발 알려줘

이거 궁금해서 미칠지경임

[러셀(salvaveritate)]

무슨 형식이 아니라, 보통 '구문론적 도출'을 의미하기 위해 쓰이는 기호임. 턴스타일(turnstile) 부호라고 부르는 게 일반적. 내가 알기로는 프레게의 <<개념표기법>>에서 유래한 기호.

[익명(219.250)]

정확한 정의 너무 감사합니다요 ㅠㅠ 근 3일동안 구글링해도 원하는 답이 안나왔는데 덕분에 속시원하게 해결됐음

[러셀(salvaveritate)]

참고로 턴스타일은 문장 연결사가 아니라 집합과 집합 사이의 관계를 나타내는 메타언어적 표현(술어?)임. 하지만 보통 P, P → Q ⊢ Q에서와 같이 중괄호를 생략해서 쓰고, 실제로는 {P, P → Q} ⊢ {Q}라는, 두 문장집합 사이의 관계를 나타내는 문장을 의도했다고 이해하면 좋음.

[강화학습(116.42)]

ㅇㅇ 턴스타일이 들어있는 문장은 논리식이 될 수 없음. 턴스타일을 넣는 순간 그 논리 규칙을 기술한 한국어, 영어 등 문장과 동급이 됨.

[강화학습(116.42)]

컴퓨팅 논리 쪽에서는 resolution이라 함

[강화학습(116.42)]

저 기호 말고 저 꺼무에 나온 초등학교 덧셈처럼 푸는 방식 ㅇㅇ