증명 전 단계에 Exists x.p(x)가 등장한다면,

[ㅇㅇㅇ(121.180)]

어떤 c를 소개하고 p(c)를 도입하여 증명을 전개할 수 있는 이유가 뭘까요?

[lp(185.182)]

질문의 뜻이 잘 이해가 안 가는데요, 혹시 "∃ x. P(x) 가 보장하는 것은 "어떤" x 가 P(x) 라는 것 뿐이고 x가 무엇인지는 알 수 없는데, 어떻게 x를 c로 특정할 수 있는가?" 라는 의문인가요?

[lp(185.182)]

그 경우 eigenvalue 조건이 존재하기 때문에 규칙의 악용이 불가능하다는 것이 일반적인 답이 아닐까 싶습니다.

[lp(185.182)]

그리고 sequent calculus를 기준으로 보자면 Γ, ∃x.P(x) ⊢ Δ 를 증명하기 위해 ∃L 규칙을 사용해서 새로운 open goal로 Γ, P(c) ⊢ Δ 를 얻더라도 결국 증명의 결론에는 c가 포함되지 않기 때문에, 뜬금없이 c에 대한 사실을 증명하는 것은 아니지요.

[lp(185.182)]

다만 전제가 ∃x.P(x)이고 P(c)로 끝나는 Fitch Calculus 증명 같은 경우는 좀 애매한 감이 있긴 합니다. 이런 쪽은 calculus의 soundness theorem이 자유변수를 어떻게 다루는지를 봐야 할 것 같네요.

[ㅇㅇㅇ(121.180)]

그렇군요. 제가 궁금했던 부분은 마지막 댓글에서 설명하신 부분에 더 가깝습니다. 제가 궁금한 것은 c가 실재하는지의 여부는 중요하지 않다는건가요?

[ㅇㅇㅇ(121.180)]

형식만 보는 거니 그렇지 않을 것 같긴 하네요.