[일반] Fitch-style system 배우니깐

[익명(14.36)]

뭐든지 first-order logic이기만 하면 증명을 기계적으로 할 수 있어서 좋은 듯. 정작 증명할 때 머리 마니 안 써서 증명 후에 이해 시도하는 상황까지 발생. 물론 복잡한 정리는 이미 증명하면서 머리를 겁나 쓴 상태이긴 하겠지만... 결과를 암기하기도 훨씬 유리함. 참고하셈.

[TonyMontana(thecoqproofassistant)]

근본은 서프스-레몬이다

[익명(14.36)]

그게 먼데;

[TonyMontana(thecoqproofassistant)]

자연연역을 다른 방식으로 쓰는 건데 걍 아는 체 해본 거임. 미안 ㅠ

[익명(14.36)]

철자 점 알려줘보셈

[TonyMontana(thecoqproofassistant)]

https://en.wikipedia.org/wiki/System_L

[익명(14.36)]

위키 예시에는 tautological consequence만 다뤘네. First-order logic에 적용된 예시 있음?

[TonyMontana(thecoqproofassistant)]

[익명(223.38)]

알음 근데 기계적으로 할수있다는게 문제임 인공지능한테 나중에 먹힐듯

[TonyMontana(thecoqproofassistant)]

RE하지만 recursive하진 않다 ...

[익명(223.62)]

ㄴ열거가능성 얘기하는건가? 튜링머신이랑 인공지능은 다를텐데

[TonyMontana(thecoqproofassistant)]

내가 문제 삼고 싶은 건 "기계적으로 할 수 있다는 게 문제임" 이말임

[TonyMontana(thecoqproofassistant)]

그리고 튜링머신이랑 인공지능이랑 다르다는 건 뭔 소리임? 자세히 좀 ...

[익명(223.38)]

뭔소린지 좀 더 구체적으로 ㄱㄱ

[TonyMontana(thecoqproofassistant)]

혹시 기계적으로 할 수 있다는 말이 무슨 말임? 나는 알고리즘이 있다는 말로 알아먹었음.

[TonyMontana(thecoqproofassistant)]

아니면 익숙해지면 패턴이 보인다는 말임?

[TonyMontana(thecoqproofassistant)]

아 후자일 수도 있구나. 미안 ㅠ

[익명(223.38)]

아 그말이 아니고 단순 계산하듯이 지루한 과정이라는 말임 너무 머리써서 배우지는 말라는 뜻 나중에 인공지능이 알아서 해줄듯 이라는 말

[익명(112.151)]

괴델의 불완전성 정리 때문에 그거 안됨

[1+1=2(lsc4719)]

됨 - dc App

[1+1=2(lsc4719)]

논리학개러리로 - dc App

[익명(14.36)]

ㅇㅇ 잘 가

[익명(14.36)]

가보니깐 도움이 될 거 같긴 한데 사람 수가 너무 적네

[1+1=2(lsc4719)]

키우자~ - dc App