공식 $\phi$ 모순을 증명하다 $\bot$ 그럼 우리는 $\vdash\phi\to\bot$?
Leary와 Kristiansen의 "A Friendly Introduction to Mathematical Logic"을 통해 자신에게 논리를 가르치려고합니다.
공리가 반드시 문장이 아니라는 점에서 공식에 중점을 둡니다.
이 책에서 실행되는 간섭 규칙은 PC (명 제적 결과) 와이를 나타내는 수량 자 규칙 QR 입니다.$\psi\to\phi$ 우리는 추론 할 수있다 $\psi\to\forall x\phi$ 만약 $x$ 자유롭지 않다 $\psi$.
허락하다 $\mathcal{L}$ 일차 언어가 되십시오. $\bot$ 일부를 표시 $\mathcal{L}$-양식의 문장 $\psi\wedge\neg\psi$ 그리고하자 $\phi$ 콩 $\mathcal{L}$-공식.
그때 $\Sigma:=\left\{ \phi\right\} $ 공제가 있다면 정의상 일관성이 없습니다. $\Sigma$ ...에 $\bot$.
이제 내 질문 :
만약 $\left\{ \phi\right\} $ 일관성이 없으면 다음 사항도 증명할 수 있습니다. $\vdash\phi\to\bot$?
대답은 "예"라는 것이 분명합니다. $\phi$ 추론 정리를 적용 할 수 있기 때문에 문장입니다.
하지만 만약 $\phi$ 문장이 아니야?
내 시도 :
만약 $\tilde{\phi}$ 보편적 인 폐쇄를 나타냅니다. $\phi$ 그때 $\left\{ \tilde{\phi}\right\} \vdash\phi$ 그래서 전이성에 의해 $\vdash$ 우리는 $\left\{ \tilde{\phi}\right\} \vdash\bot$ 그리고 우리가 가지고있는 추론 정리 적용 $\vdash\tilde{\phi}\to\bot$.
그러나 이것은 문제를 다른 질문으로 이동시킬뿐입니다.
공제가있는 경우 $\vdash\tilde{\phi}\to\bot$ 그리고 공제가 있습니다 $\vdash\phi\to\bot$?
미리 감사 드리며이 질문이 중복되면 사과드립니다.
답변
Leary와 Kristiansen의 책은 읽지 않았지만 현재 Mendelson의 "수학적 논리 입문"을 읽고 있으므로 첫 번째 질문에 답할 수 있기를 바랍니다.
"만약 공식 ϕ (ϕ : ψ ∧ ¬ ψ)가 모순 ⊥을 증명한다면 ⊢ ϕ → ⊥?" 나는 대답 할 수 있습니다 : ψ ∧ ¬ ψ라는 공식은 우리가 결론을 내리게 할 것입니다 ⊥, 이것은 (ψ ∧ ¬ ψ) → ⊥ 공식은 정리입니다. 여기 자연 추론 규칙을 사용한 공식의 증거가 있습니다 :
1) ψ ∧ ¬ ψ-가정
2) ψ-규칙 E∧ in 1
3) ¬ ψ-규칙 E∧ in 1
4) ⊥-2,3에서
5) (ψ ∧ ¬ ψ) → ⊥-규칙 I → 1,4
ψ ∧ ¬ ψ의 진리표를 보면 모든 값이 거짓이라는 것은 (ψ ∧ ¬ ψ) → ⊥뿐만 아니라 (ψ ∧ ¬ ψ) → X (여기서 X는 임의의 공식)은 tautology입니다. 공식이 모순을 증명하면 u는 모든 공식을 조사합니다.
두 번째 질문에 대해서는 대답 할 수있을만큼 자신이 없습니다. 현재 Mendelson의 책 (1 차 논리) 2 장을 읽고 있으므로 의심을 공유합니다.