플라톤주의 따라서 진릿값이 정해져 있고, 집합론적 세계인 폰 노이만 유니버스도 엄연히 존재하고, 그러면 뭐 더할나위 없겠지만 불완전성 정리 때문에 그 성질을 제대로 파헤치는 게 불가능하다면 의미가 있는건가 싶습니다.
뭐 불완전성 정리가 형식주의를 좌초시켰니 어쩌니 하는데, 전 다르게 봅니다. 형식주의로 완전성을 추구하려는 시도야 깨졌겠지만, 솔직히 그 부분은 형식주의에 플라톤주의 끼얹은 논리주의가 감당할 몫이고, 형식주의의 증명 기법은 여전히 건재하며 대신 (PA의 비표준 모형에서 +가 "우리가 아는 그 더하기"가 아니듯이) 명제와 명제의 해석은 역시 구분되어야 한다는 형식주의의 핵심을 오히려 강조하고 있다고 저는 보고 있습니다.

명제란 참거짓을 명확히 판별할 수 있는 문장?
연속체 가설은 판별이 불가능하니 명제가 아닌 걸까요?

명제 구문과 그 명제의 해석은 철저하게 분리되어야 하고, 믿을 만한 건 기계적 증명시스템뿐이라고 봅니다. 명제는 WFF이고, WFF는 다시 모호함 없이 기계적으로 처리할 수도, 귀납적으로 해석할 수도 있는 문장입니다.
semantic consequence는 그걸 보이는 과정에서 다시 논리적 추론이 들어가기 때문에 받아들이기 어렵습니다. (어차피 완전성 정리 있잖아요)

진릿값에 관한 나이브한 전제는 어쩔 수 없다 치더라도, 진릿값 함수와 추론규칙을 동시에 받아들이기 위한 건전성은 "참거짓 평가가 선행하고, 추론규칙이 참인 명제의 진릿값을 보존하기에 추론규칙을 받아들임"뿐만 아니라 "추론규칙이 선행하고, 그 위에서 참거짓 평가값(불대수)이 추론규칙에 의해 보존되므로 참거짓 평가를 받아들임" 이런 식으로 쌍대적으로 생각해야 된다고 봅니다.
이렇게 해야 연역정리랑 MP로 자연스레 정의되는 →에 진릿값을 일의적으로 매길 수 있게 됩니다.

물론 전 수학에 있어서 직관주의까지 받아들일 여유는 없기에 배중률은 쓰지만요.