그러면 명제가 참인지 거짓인지 어떻게 판별해요?

[기괴공학도(mecheng98)]

형님들 조언대로 자연어로 나타내겠습니다.

"x_1, ..., x_n은 독립변수이다",

"y는 종속변수이다",

"c는 상수이다"

고 선언되었다고 칩시다.

그러면 명제 phi(x_1, ..., x_n, y, c)가 참인지 거짓인지를 어떻게 정의하나요?

[기괴공학도(mecheng98)]

저도 참인지 거짓인지는 알 수 있지만, 이 규칙을 기호로 나타내면 어떻게 될지 궁금하네요.

[lp(24.3)]

조금 넘겨짚어 보자면, 단순히 free/bound variable의 문제 뿐만 아니라 전반적인 1차논리의 메타이론을 형식적으로 다루는 방법을 찾으시는 것 같습니다. 예를 들어 substitution이 논리식의 진리치를 보존한다는 정리를 형식적 proof calculus 내부에서 기술하고 증명하는 방법 같은 것 말이죠. 제 생각이 맞나요?

[기괴공학도(mecheng98)]

아니요. 그건 포기했어요. 수리논리학에서는 독립변수와 종속변수를 다루지 않는 것 같은데, 어떻게 독립변수와 종속변수가 있는 논리식을 해석을 줄 수 있도록 엄밀하게 번역하는 방법이 궁금하네요. 그래서 기호로 나타내면 어떻게 되는지 궁금하다 했고요.

[lp(24.3)]

지금 보니 제가 잘못 읽은 것 같은데, free/bound variable이 아니라 dependent/independent variable인가요? 통계학이나 실험설계에 나오는?

[기괴공학도(mecheng98)]

네!!

[lp(24.3)]

음... 귀납추론을 다루는 논리도 다양하게 있다고 듣긴 했지만 저는 아는 게 없네요.

[기괴공학도(mecheng98)]

그러면 독립변수와 종속변수를 다루는 저만의 해석을 올리면 검토해주실 수 있나요?

[기괴공학도(mecheng98)]

아니면 만들어주셔도 되고요...

[lp(24.3)]

해당 분야에 제반지식이 전혀 없어서 아마 봐도 잘 모를 것 같네요; 그리고 1차논리의 메타이론을 형식적으로 기술하는 것 자체는 사실 그렇게 어렵지 않습니다. Calculus of Inductive Constructions 같이 더 강력한 증명체계에 embedding을 하면 되지요. 물론 메타정리를 형식적으로 증명하는 건 전혀 다른 문제지만요.

[기괴공학도(mecheng98)]

알겠습니다.