내 풀이가 맞는지
한 줄씩 확인하세요.

입력 규칙

조건문은 ->, 연언은 &, 선언은 대문자 V로 입력하세요. V는 선언 기호로 쓰므로 명제문자 이름에는 넣지 않습니다.

규칙 이름은 -> 제거, & 도입, V 제거처럼 씁니다. ->E, VI, ~I 같은 약어도 쓸 수 있습니다. 인용번호 칸에는 1,2 또는 3-5를 적으세요. 인용 목록은 1,2,3, 2,3,1,, 1,3,2처럼 순서를 바꿔도 됩니다. 범위의 시작·끝 번호는 3-5처럼 작은 번호부터 적으세요.

보조증명이 여러 개라면

가정 시작을 누르면 한 단계 안쪽에서 새 가정을 시작합니다. 행 추가는 그 깊이를 유지하고, 다음 경우는 같은 깊이에서 다른 가정을 시작합니다. 수식 왼쪽의 세로선으로 깊이를 확인하세요.

->로 가정 닫기 또는 ~로 가정 닫기를 누르면 결론 행과 보조증명 범위가 자동으로 채워집니다. 두 경우를 마쳤다면 두 경우 결론을 누르세요. 행 번호 옆의 ‹·›로 깊이를 조정할 수도 있습니다. 삭제된 행을 인용하던 번호는 ?로 표시됩니다.

보편 도입 · 임의 이름 상자

임의 이름 시작을 누르고 수식 칸에 u처럼 새 이름 하나를 쓰세요. 그 안에서 필요한 식을 얻은 뒤 ∀로 이름 상자 닫기를 누르고 결론에 Ax Px처럼 일반화한 식을 입력하세요. 인용 범위는 자동으로 채워집니다. 상자 없이 마지막 행 하나를 인용하는 방식도 허용합니다.

일반화하는 이름은 전제·열린 가정에 없어야 합니다. ∃ 제거로 고른 임시 이름이나 그 선택에 의존하는 이름은 임의로 일반화할 수 없습니다.

존재 제거 · 세 가지 입력 방식

교재 약식은 존재문 한 행을 인용하고 새 이름으로 대입한 식을 적습니다. 예: ∃x Px에서 Pa. 이 임시 이름은 앞선 행·전제·목표 결론에 없어야 합니다.

보조증명을 쓰려면 가정 시작으로 Pa를 가정하고, 이름 a가 남지 않은 결론을 얻은 뒤 ∃로 가정 닫기를 누르세요. 인용의 ?를 존재문 행 번호로 바꾸세요. 존재문과 ∀x(Px -> C)를 함께 인용하는 교재의 엄밀한 형식도 가능합니다.

보편 제거·보편제거·전칭 제거·전칭제거는 같습니다. 소문자 v는 변항, 대문자 V는 선언입니다. 이름·변항은 소문자 한 글자(숫자 첨자 가능), 술어는 대문자 한 글자로 씁니다.