(A → B) ⊢ (¬A ∨ B)
A→C, B→C, A∨B ⊢ C
∃x(Ax∧Bx) ⊢ ∃xAx∧∃xBx
∀x(Ax→Bx) ⊢ ∀xAx→∀xBx
∀x(Ax→Bx) ⊢ ∃xAx→∃xBx
⊢ (A→B)→((B→C)→(A→C))
⊢ A∨¬A
⊢ ¬¬A → A
⊢ A → ¬¬A
⊢ (A → B) ∨ (B → A)
⊢ (¬∀xAx) → (∃x¬Ax)
⊢ (¬∃x¬Ax) → (∀xAx)
∀x∀yAxy ⊣⊢ ∀y∀xAxy
∃x∃yAxy ⊣⊢ ∃y∃xAxy
∀x(Ax∧Bx) ⊣⊢ ∀xAx∧∀xBx
∃x(Ax∨Bx) ⊣⊢ ∃xAx∨∃xBx
∃x(Ax→B) ⊣⊢ ∀xAx→B
Natural Deduction (Fitch-style)
출력
이곳에 결과가 표시됩니다.
전제가 2개 이상일 때는 쉼표(,)로 구분합니다.
괄호 생략 우선순위: 1. ¬ 2. ∧ 3. ∨ 4. → (오른쪽 결합)
[예]
¬Fx → ¬Gab ∨ ∀y Ry ∧ Sy
≡ ((¬Fx) → ((¬Gab) ∨ (∀y Ry ∧ Sy)))
P ∧ Q ∧ R ∧ S
≡ (P ∧ (Q ∧ (R ∧ S)))
명제 기호: A-Z
술어 기호: A-Z
상항 기호: a-t
변항 기호: u-z
항 기호가 부족할 경우 숫자를 활용하세요.
[예] a, a1, a2, x1, x2, w123, z14230
술어 기호와 명제 기호에는 숫자 기능을 지원하지 않으므로 중복 사용을 금지합니다.
[금지] Px → (P ∨ ¬Px), Px → (Pxy ∨ ¬Px)
[허용] Px → (Q ∨ ¬Px), Px → (Qxy ∨ ¬Px)
rule
