콘텐츠로 바로가기
HY_TECH_BASE

Propositional & Predicate Logic

컴퓨팅 사고의 가장 원자적인 논리 단위인 명제 논리와 변수 및 양화자를 포함한 서술어 논리를 정의하고, 선언적 스펙 정의와 인공지능 추론의 기초를 다루는 학습 노드입니다.

sys.entry
M

Me

hyunyoun's Blog

posts6 min read

1. Overview

명제 및 서술어 논리(Propositional & Predicate Logic, PPL)는 참(True)과 거짓(False)이라는 이진 상태를 사용하여 복잡한 사고 체계를 수학적으로 모델링하는 학문입니다.

컴퓨터는 본질적으로 논리 기계입니다. 학습자는 참/거짓으로 판별되는 문장의 결합인 명제 논리(Propositional Logic), 그리고 객체 간의 관계와 속성을 다루는 **서술어 논리(Predicate Logic)**의 물리적 규칙을 배웁니다. 이를 통해 프로그램 내부의 복잡한 조건문을 엄밀하게 최적화하고, 인공지능의 지식 표현이나 하드웨어의 논리 회로 설계가 갖춰야 할 논리적 무결성을 확보하는 능력을 갖춥니다.

2. Scope & Boundaries

In-Scope

  • Propositional Connectives: AND(∧), OR(∨), NOT(¬), Implication(→), IFF(↔)의 진리표와 연산 역학
  • Logical Equivalences: 드 모르간의 법칙, 분배 법칙 및 항진식(Tautology) 판별
  • Predicates & Quantifiers: 존재 양화사(∃)와 보편 양화사(∀)의 물리적 선언 및 범위(Scope)
  • Rules of Inference: 전건 긍정(Modus Ponens), 후건 부정(Modus Tollens) 등 논리적 추론 시퀀스

Out-of-Scope

  • 비정형 언어로 된 철학적 논리학 (전문 인문학 영역)
  • 퍼지 논리(Fuzzy Logic) 등 비이진 논리계 (AI 특수 영역)

Boundaries

  • PPL vs. Boolean Algebra: 불 대수가 주로 '회로 전압과 비트 연산'이라는 물리적 구현에 집중한다면, PPL은 '의미론적 문장들 사이의 구조적 진위 여부'라는 추상적 논증에 집중합니다.

3. Counterexample

  • 단순히 "if-else 문을 중첩해서 쓰는 것"은 PPL 학습이 아닙니다. 왜 $A \rightarrow B$라는 논리 구조에서 $B$가 참이라고 해서 $A$가 반드시 참인 것은 아닌지(전건 긍정의 역설) 그 물리적 방향성을 설명할 수 있어야 하고, 전체 집합이 정의되지 않은 상태에서 **보편 양화사(∀)**를 남용할 때 발생하는 증명상의 허점을 지적할 수 있어야 합니다.

4. Prerequisites

  • 집합론 및 관계 (Basic): 원소의 포함 관계와 교집합/합집합 개념 이해가 필수입니다. (01-01 STR)

5. Learning Map

  1. Atomic Truths: 더 이상 쪼개지지 않는 명제의 진리값을 정의하고 연산하는 법을 익힙니다.
  2. Formula Synthesis: 여러 명제를 결합하여 복합적인 논리식을 구성하고 간소화합니다.
  3. Generalization Physics: 변수와 양화사를 도입해 보편적인 규칙을 수학적으로 기술합니다.
  4. Valid Inference: 공리와 전제로부터 결론을 물리적으로 도출하는 추론 엔진을 구축합니다.

6. Learning Topics

Basic

Core: 명제 논리와 진리 연산 (Propositional Foundations)

  • Why to Learn: 프로그램의 분기 조건을 오류 없이 설계하고 논리적 오류를 사전에 차단하기 위함입니다.
  • What to Learn:
    • 논리 연산자: ∧, ∨, ¬, ⊕(XOR)의 물리적 진리표
    • 조건문(Implication): P→QP \rightarrow Q의 진위 판단 물리 (거짓인 유일한 케이스 분석)
    • 역(Converse), 이(Inverse), 대우(Contrapositive)의 관계와 논리적 동치성
  • How to Learn:
    • 복잡한 3중 중첩 if문을 논리식으로 변환한 뒤 진리표를 작성해 중복 조건 제거 실습
    • 대우 명제를 이용해 직접 증명이 어려운 명제를 우회 증명하는 기법 연습
  • Implement: 입력된 논리식의 진리표를 자동으로 생성하는 분석 스크립트

Core: 논리적 동치와 정규형 (Equivalence & Normal Forms)

  • Why to Learn: 논리식을 기계가 처리하기 쉬운 표준 규격으로 변환하여 연산 효율을 높이기 위해서입니다.
  • What to Learn:
    • 주요 동치 법칙: 결합, 분배, 흡수, 멱등 법칙의 물리적 정당성
    • 논리 정규형: CNF(Conjunctive Normal Form)와 DNF(Disjunctive Normal Form)의 구조
    • 만족 가능성 문제(SAT): 논리식을 참으로 만드는 변수 조합 탐색 기초
  • How to Learn:
    • 복잡한 불 대수 식을 CNF로 변환하여 SAT Solver에 입력 가능한 형태로 정제 실습
    • 벤 다이어그램과 칸토어의 증명 기법을 이용해 논리식의 동치 여부 시각화
  • Implement: 드 모르간의 법칙을 활용해 논리식을 최소 항으로 간소화하는 최적화 엔진

Practical

Core: 서술어 논리와 양화 물리 (Predicate Dynamics)

  • Why to Learn: 단순 상수를 넘어 변수가 포함된 데이터 집합의 보편적 성질을 정의하기 위함입니다.
  • What to Learn:
    • 자유 변수(Free Variable) vs 결합 변수(Bound Variable)의 물리적 스코프
    • 양화사(∀,∃\forall, \exists)의 적용 범위와 부정 규칙 (¬∀xP(x)≡∃x¬P(x)\neg\forall x P(x) \equiv \exists x \neg P(x))
    • 서술어의 중첩: "모든 사용자에게 하나 이상의 권한이 있다"와 같은 명제 모델링
  • How to Learn:
    • 데이터베이스의 SQL EXISTS나 ALL 구문이 서술어 논리의 양화사와 어떻게 매핑되는지 분석
    • 요구사항 명세서의 자연어를 서술어 논리 기호로 변환하여 예외 케이스(Edge case) 추출 연습
  • Implement: 객체 간의 관계를 서술어 형식으로 저장하고 양화사 쿼리를 수행하는 논리 데이터 모델

Advanced

Core: 증명 기법과 자동 추론 (Proof Theory)

  • Why to Learn: 프로그램의 설계가 논리적으로 결함이 없음을 수학적으로 입증하고 보장하기 위해서입니다.
  • What to Learn:
    • 추론 규칙: 분해법(Resolution rule)의 물리적 원리와 연쇄 반응
    • 직접 증명, 귀류법(Proof by Contradiction), 수학적 귀납법의 물리적 시퀀스
    • 자동 정리 증명(ATP)의 기초: 기계가 논리를 따라 결론에 도달하는 메커니즘
  • How to Learn:
    • 귀류법을 사용하여 "루트 2는 무리수이다"와 같은 명제를 단계별 논리 붕괴로 증명 실습
    • 단순한 공리계(Axiom system)를 설정하고 새로운 정리를 추론 규칙만으로 유도해보는 연습
  • Implement: 주어진 전제들로부터 특정 결론이 도출 가능한지 확인하는 전진 추론(Forward Chaining) 시스템

7. Terminology

Term (EN / ko, abbr) 1문장 정의 단계(기본/권장/실무/심화) 역할/맥락 관련 개념 유사/대비/함께 사용 오해 포인트 Evidence(Primary/Secondary/Industry) Flags(core)
Tautology (항진식) 모든 변수의 진리값 조합에 관계없이 항상 참이 되는 논리적 절대 물리입니다. 기본 무결성 검증 Contradiction SAT '당연한 말'과 혼동 P1:CS2023/BasicLogic core
Implication (함축) 전제가 참일 때 결론도 참임을 정의하는 조건부 논리 연결성 물리입니다. 추천 인과 모델링 If-Then Biconditional 일상적 '인과'와 혼동 P1:CS2023/BasicLogic core
Quantifier (양화사) 서술어가 적용되는 대상의 범위를 '모든' 혹은 '어떤'으로 한정하는 물리적 지시어입니다. 실무 범위 정의 Universal / Existential Scope 변수 선언과 혼동 P1:CS2023/BasicLogic core
Normal Form (정규형) 논리 연산을 최적화하기 위해 정해진 구조적 규격(CNF/DNF)으로 식을 고정하는 것입니다. 심화 연산 최적화 Canonical Form SAT Solver '정규화'와 혼동 P1:CS2023/BasicLogic core

8. References

Primary

Secondary

  • [Logic and Structure] Dirk van Dalen — Mathematical logic standard.
  • [Logic in Computer Science] Michael Huth — Practical tool-based logic.

Industry

  • [SAT Solvers in Software Verification] — Industry application of logic.
  • [Knowledge Representation in AI] — Predicate logic in expert systems.

9. Final Checklist

Primary

  • 복잡한 명제 논리식을 '드 모르간의 법칙'과 '분배 법칙'을 사용하여 최소 연산 형태로 물리적 간소화가 가능한가? (P1)
  • 서술어 논리에서 양화사가 중첩되었을 때(∀∃\forall \exists vs ∃∀\exists \forall), 그 선후 관계가 명제의 의미를 어떻게 물리적으로 변화시키는지 서술 가능한가? (P1)

Secondary

  • 진리표를 작성하지 않고도 특정 논리식이 '진리값 보존 추론'에 의해 참임을 대수적으로 증명할 수 있는가?
  • CNF(논리곱 표준형)가 왜 컴퓨터의 자동 증명 시스템(Resolution)에서 물리적으로 효율적인 구조인지 논리적으로 소통 가능한가?

Industry

  • 비즈니스 정책(Policy)이 담긴 자연어 요구사항을 논리 기호로 전사하여, 정책 간의 충돌이나 모순이 발생하는 지점을 수학적으로 탐지 가능한가? (SFIA)
  • 보안 규칙 설계 시, '보편 양화사'의 필터링 조건과 '존재 양화사'의 허용 조건이 결합된 화이트리스트 논리를 무결하게 설계할 수 있는가?

Concepts & Tags

#logic#propositional-logic#predicate-logic#quantifiers#proof-theory