HOTIAN’S ARROW / 풀이 01
기호식과 나란히,
다섯 번의 증명.
같은 전제에서 같은 결론까지.
왼쪽의 근거와 오른쪽의 원을 함께 읽습니다.
다섯 문제의 완성 풀이를 차례로 살펴보세요. 각 문제에서 ‘차례로 재생’을 누르면 전제를 놓는 순간부터 한 줄씩 다시 따라갈 수 있습니다.
p → q, p ∴ q
02q → r, q ∴ r
첫 연결: p → q와 p에서 q를 얻습니다.
이 q로 다음 조건을 이어 갑니다.
● p ○ ¬p찬 원은 긍정형, 빈 원은 부정형입니다.
한 행은 ‘또는’여러 행은 행 전체를 묶어 ‘그리고’로 읽습니다.
두 행 · 같은 축 · 반대 원 한 쌍그 한 쌍을 제외한 나머지 원을 새 행에 모읍니다. 기존 행은 남깁니다.
전건긍정 · MP
조건을 두 번 이어 r에 도달하기
p라는 사실에 두 조건문을 차례로 적용하여 q를 거쳐 r을 얻습니다.
두 풀이 모두 r에 도달했습니다. 각 줄의 근거와 도식의 결과 행을 확인해 보세요.
SYMBOLIC PROOF
일반 기호 증명
- 1
p → q
전제 1
도식에서는 ¬p ∨ q
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 2
q → r
전제 2
도식에서는 ¬q ∨ r
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 3
p
전제 3
- 4
q
전건긍정 MP · 1, 3줄
p→q와 p가 있으므로 q를 얻습니다.
- 5
r
전건긍정 MP · 2, 4줄
q→r에 방금 얻은 q를 적용하여 r을 얻습니다.
r
위 전제와 근거에서 얻은 결론입니다.
추론 2 / 2회
전제 3개는 추론 횟수에 포함하지 않습니다.
VERTICAL LINES & CIRCLES
Hotian’s Arrow
원래 전제 3개를 남겨 둡니다. 목표 r는 전제에 추가하지 않습니다.
다섯 축이 잘리지 않도록 도식 안에서 가로로 이동할 수 있습니다.
2행의 ¬q와 4행의 q 한 쌍을 선택합니다. 새 행의 r이 목표와 같습니다.
r
마지막 행이 이미 r이므로 결론 확인을 추가 추론으로 세지 않습니다.
해소 2 / 2회
도식 표기 변환 2회 · 전제를 OR 행으로 옮기는 과정
도식의 근거를 식으로 읽기
- q1·3행에서 p의 반대 원 한 쌍 · 1행의 ¬p와 3행의 p 한 쌍을 선택합니다. 나머지 q를 새 행에 놓습니다.
- r2·4행에서 q의 반대 원 한 쌍 · 2행의 ¬q와 4행의 q 한 쌍을 선택합니다. 새 행의 r이 목표와 같습니다.
p와 p→q에서 q를 얻고, 그 q와 q→r에서 r을 얻습니다. 한 번 얻은 결과는 다음 추론의 근거가 됩니다.
양쪽 모두 두 번의 추론으로 끝나며, 기호식은 전건긍정을, 도해는 p축과 q축의 상보쌍을 드러냅니다.
후건부정 · MT
결과의 부정에서 조건을 거슬러 가기
¬r에서 ¬q를, 다시 ¬p를 얻는 후건부정을 두 번 적용합니다.
두 풀이 모두 ¬p에 도달했습니다. 각 줄의 근거와 도식의 결과 행을 확인해 보세요.
SYMBOLIC PROOF
일반 기호 증명
- 1
p → q
전제 1
도식에서는 ¬p ∨ q
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 2
q → r
전제 2
도식에서는 ¬q ∨ r
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 3
¬r
전제 3
- 4
¬q
후건부정 MT · 2, 3줄
q→r과 ¬r에서 ¬q를 얻습니다.
- 5
¬p
후건부정 MT · 1, 4줄
p→q와 ¬q에서 ¬p를 얻습니다.
¬p
위 전제와 근거에서 얻은 결론입니다.
추론 2 / 2회
전제 3개는 추론 횟수에 포함하지 않습니다.
VERTICAL LINES & CIRCLES
Hotian’s Arrow
원래 전제 3개를 남겨 둡니다. 목표 ¬p는 전제에 추가하지 않습니다.
다섯 축이 잘리지 않도록 도식 안에서 가로로 이동할 수 있습니다.
1행의 q와 4행의 ¬q 한 쌍을 선택하면 ¬p가 남습니다.
¬p
¬p의 단일 행이 목표를 그대로 나타냅니다.
해소 2 / 2회
도식 표기 변환 2회 · 전제를 OR 행으로 옮기는 과정
도식의 근거를 식으로 읽기
- ¬q2·3행에서 r의 반대 원 한 쌍 · 2행의 r과 3행의 ¬r 한 쌍을 선택하면 ¬q가 남습니다.
- ¬p1·4행에서 q의 반대 원 한 쌍 · 1행의 q와 4행의 ¬q 한 쌍을 선택하면 ¬p가 남습니다.
q→r인데 r이 성립하지 않으면 q도 성립하지 않습니다. 같은 규칙을 p→q에 한 번 더 적용하면 ¬p를 얻습니다.
기호식의 두 후건부정은 도해에서 r축과 q축의 상보쌍을 차례로 해소하는 두 단계에 대응합니다.
경우분석 · ∨E
어느 경우에서도 r을 얻기
p인 경우와 q인 경우를 따로 증명한 뒤, 두 임시 가정을 해제하여 r을 얻습니다.
두 풀이 모두 r에 도달했습니다. 각 줄의 근거와 도식의 결과 행을 확인해 보세요.
SYMBOLIC PROOF
일반 기호 증명
- 1
p ∨ q
전제 1
- 2
p → r
전제 2
도식에서는 ¬p ∨ r
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 3
q → r
전제 3
도식에서는 ¬q ∨ r
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 4p인 경우 · 이 범위에서만 사용
p
임시 가정
첫 번째 경우에서만 p를 가정합니다. 이 줄은 추론 횟수에 포함하지 않습니다.
- 5
r
전건긍정 MP · 2, 4줄
p인 경우에는 p→r로부터 r을 얻습니다. 이 r은 아직 첫 번째 가정의 범위 안에 있습니다.
- 6q인 경우 · 이 범위에서만 사용
q
임시 가정
두 번째 경우에서는 별도로 q를 가정합니다. 첫 번째 경우의 p를 가져오지 않습니다.
- 7
r
전건긍정 MP · 3, 6줄
q인 경우에도 q→r로부터 r을 얻습니다.
- 8
r
선언 제거·경우 분석 ∨E · 1, 5, 7줄
p∨q이고 두 경우 모두 r에 도달했습니다. 두 임시 가정을 해제하고 범위 밖에서 r을 결론 냅니다.
p인 경우 / q인 경우 · 두 임시 가정 해제
r
임시 가정이 모두 해제된 결론입니다.
추론 3 / 3회 · 임시 가정 2 / 2줄
전제 3개는 추론 횟수에 포함하지 않습니다.
VERTICAL LINES & CIRCLES
Hotian’s Arrow
원래 전제 3개를 남겨 둡니다. 목표 r는 전제에 추가하지 않습니다.
다섯 축이 잘리지 않도록 도식 안에서 가로로 이동할 수 있습니다.
4행의 q와 3행의 ¬q 한 쌍을 선택합니다. 남은 r∨r는 r와 같으므로 r 원 하나를 놓습니다.
r
최종 r행은 어느 경우인지 고르지 않고 얻은 결과입니다.
해소 2 / 2회
도식 표기 변환 2회 · 전제를 OR 행으로 옮기는 과정
도식의 근거를 식으로 읽기
- q ∨ r1·2행에서 p의 반대 원 한 쌍 · 1행의 p와 2행의 ¬p 한 쌍을 선택합니다. 나머지 q와 r은 같은 새 행에 놓여 q∨r가 됩니다.
- r4·3행에서 q의 반대 원 한 쌍 · 4행의 q와 3행의 ¬q 한 쌍을 선택합니다. 남은 r∨r는 r와 같으므로 r 원 하나를 놓습니다.
p∨q는 두 경우 중 적어도 하나가 성립한다는 뜻입니다. 두 경우에서 각각 r을 얻었으므로, 어느 쪽인지 정하지 않아도 r을 결론 낼 수 있습니다. p와 q를 함께 사실로 추가한 것은 아닙니다.
기호식은 두 가정의 범위와 ∨E의 해제를 보여 주고, 도해는 q∨r라는 중간 행을 거치는 두 번의 해소를 보여 줍니다.
연언 도입 · ∧I
같은 사실에서 두 결과를 함께 얻기
p를 두 조건문에 각각 적용하여 q와 r을 얻고, 두 결과를 q∧r로 묶습니다.
두 풀이 모두 q ∧ r에 도달했습니다. 각 줄의 근거와 도식의 결과 행을 확인해 보세요.
SYMBOLIC PROOF
일반 기호 증명
- 1
p → q
전제 1
도식에서는 ¬p ∨ q
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 2
p → r
전제 2
도식에서는 ¬p ∨ r
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 3
p
전제 3
- 4
q
전건긍정 MP · 1, 3줄
p→q와 p에서 q를 얻습니다.
- 5
r
전건긍정 MP · 2, 3줄
같은 전제 p를 p→r에도 적용하여 r을 얻습니다.
- 6
q ∧ r
연언 도입 ∧I · 4, 5줄
q와 r을 모두 증명했으므로 q∧r로 묶습니다.
q ∧ r
위 전제와 근거에서 얻은 결론입니다.
추론 3 / 3회
전제 3개는 추론 횟수에 포함하지 않습니다.
VERTICAL LINES & CIRCLES
Hotian’s Arrow
원래 전제 3개를 남겨 둡니다. 목표 q ∧ r는 전제에 추가하지 않습니다.
다섯 축이 잘리지 않도록 도식 안에서 가로로 이동할 수 있습니다.
q ∧ r
4행의 q와 5행의 r을 함께 읽으면 q∧r입니다. 두 행을 보존하며, 이 묶기는 새로운 해소가 아닙니다.
q ∧ r
해소로 얻은 두 독립된 행을 한 번 함께 읽어 목표 q∧r를 표시합니다.
해소 2 / 2회 · 목표 읽기 1 / 1회
도식 표기 변환 2회 · 전제를 OR 행으로 옮기는 과정
도식의 근거를 식으로 읽기
- q1·3행에서 p의 반대 원 한 쌍 · 1행의 ¬p와 3행의 p 한 쌍에서 q를 얻습니다. 사용한 3행은 그대로 남습니다.
- r2·3행에서 p의 반대 원 한 쌍 · 2행의 ¬p와 원래 3행의 p 한 쌍에서 r을 얻습니다. q와 r은 서로 다른 결과 행입니다.
- q ∧ r4행의 q와 5행의 r을 함께 읽으면 q∧r입니다. 두 행을 보존하며, 이 묶기는 새로운 해소가 아닙니다.
전제 p는 첫 추론에 사용한 뒤에도 남아 있어 두 번째 조건문에 다시 적용할 수 있습니다. q와 r을 함께 얻었다는 것은 q∧r이며, 도해에서는 서로 다른 두 행으로 읽습니다.
기호식의 ∧I에 해당하는 마지막 묶기는 도해에서 두 행의 AND 읽기로 표시하며, 해소 2회와 목표 읽기 1회를 구분합니다.
복합 추론
분기에서 합류한 뒤 다음 조건으로
q∨r의 두 경우에서 공통 결과 s를 얻은 뒤, s→t를 한 번 적용합니다.
두 풀이 모두 t에 도달했습니다. 각 줄의 근거와 도식의 결과 행을 확인해 보세요.
SYMBOLIC PROOF
일반 기호 증명
- 1
p → (q ∨ r)
전제 1
도식에서는 ¬p ∨ q ∨ r
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 2
q → s
전제 2
도식에서는 ¬q ∨ s
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 3
r → s
전제 3
도식에서는 ¬r ∨ s
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 4
s → t
전제 4
도식에서는 ¬s ∨ t
조건문을 OR 행으로 옮긴 같은 뜻의 표기 - 5
p
전제 5
- 6
q ∨ r
전건긍정 MP · 1, 5줄
p→(q∨r)와 p에서 q∨r를 얻습니다.
- 7q인 경우 · 이 범위에서만 사용
q
임시 가정
첫 번째 경우에서 q를 가정합니다.
- 8
s
전건긍정 MP · 2, 7줄
q인 경우에는 q→s에서 s를 얻습니다.
- 9r인 경우 · 이 범위에서만 사용
r
임시 가정
두 번째 경우에서는 별도로 r을 가정합니다.
- 10
s
전건긍정 MP · 3, 9줄
r인 경우에도 r→s에서 s를 얻습니다.
- 11
s
선언 제거·경우 분석 ∨E · 6, 8, 10줄
q∨r의 두 경우가 모두 s로 이어집니다. 두 임시 가정을 해제하여 전역 결과 s를 얻습니다.
q인 경우 / r인 경우 · 두 임시 가정 해제 - 12
t
전건긍정 MP · 4, 11줄
합류한 결과 s에 s→t를 적용하여 t를 얻습니다.
t
임시 가정이 모두 해제된 결론입니다.
추론 5 / 5회 · 임시 가정 2 / 2줄
전제 5개는 추론 횟수에 포함하지 않습니다.
VERTICAL LINES & CIRCLES
Hotian’s Arrow
원래 전제 5개를 남겨 둡니다. 목표 t는 전제에 추가하지 않습니다.
다섯 축이 잘리지 않도록 도식 안에서 가로로 이동할 수 있습니다.
8행의 s와 4행의 ¬s 한 쌍에서 t를 얻습니다.
t
q∨r의 두 가능성을 거쳐 얻은 t행이 목표와 같습니다.
해소 4 / 4회
도식 표기 변환 4회 · 전제를 OR 행으로 옮기는 과정
도식의 근거를 식으로 읽기
- q ∨ r1·5행에서 p의 반대 원 한 쌍 · 1행의 ¬p와 5행의 p 한 쌍을 선택하여 q∨r를 새 행에 놓습니다.
- r ∨ s6·2행에서 q의 반대 원 한 쌍 · 6행의 q와 2행의 ¬q 한 쌍에서 r∨s를 얻습니다. 아직 r과 s를 각각 얻은 것은 아닙니다.
- s7·3행에서 r의 반대 원 한 쌍 · 7행의 r과 3행의 ¬r 한 쌍을 선택합니다. 중복된 s는 하나로 적어 s행을 얻습니다.
- t8·4행에서 s의 반대 원 한 쌍 · 8행의 s와 4행의 ¬s 한 쌍에서 t를 얻습니다.
조건문이 내놓는 결과 자체가 q∨r처럼 분기일 수 있습니다. 두 경우에서 같은 s를 얻었다면 가정을 해제하고 합류한 뒤 s→t를 적용하면 됩니다. 각 경우에서 t까지 따로 반복할 필요는 없습니다.
기호식은 두 임시 가정의 범위를 명시하고, 도해는 q∨r에서 r∨s를 거쳐 s와 t를 얻는 네 번의 해소를 보여 줍니다.
다섯 풀이를 마치고
같은 결론을,
두 가지 기록으로 읽었습니다.
기호 증명에서는 각 줄의 식과 근거를 확인했습니다. 줄타기에서는 원래 전제를 남겨 둔 채, 같은 축의 반대 원 한 쌍으로 새 행을 얻었습니다. 결론이 두 문장일 때에는 두 행을 함께 읽었습니다.
이 풀이에서 규칙과 단계를 세는 방법
왼쪽은 전건긍정(MP), 후건부정(MT), 경우분석(∨E), 연언 도입(∧I)을 사용합니다. 후건부정은 익숙한 추론 규칙 하나로 셉니다. 경우분석의 임시 가정은 별도로 표시하며, 두 경우를 합치는 줄에서 그 가정을 해제합니다.
오른쪽은 조건문을 OR 행으로 옮기는 표기 변환, 두 행에서 새 행을 얻는 해소, 여러 목표 행을 함께 읽는 과정을 구분합니다. 전제 표기는 양쪽에 동시에 나타나며, 화면의 재생 간격은 각 기록을 읽기 위한 시간입니다.
‘한 줄씩’은 각 방식의 다음 기록을 하나씩 보여 줍니다. 임시 가정 한 줄과 추론 한 회는 구분해서 셉니다. 문제마다 적힌 횟수는 여기에 제시한 풀이의 횟수입니다.
규칙 확인: 자연연역과 경우분석 · 명제논리의 해소 규칙