2nd/10_Wiki/Topics/Computer_Science_and_Theory/Axiomatic-Systems.md

id, title, category, status, canonical_id, aliases, duplicate_of, source_trust_level, confidence_score, verification_status, tags, raw_sources, last_reinforced, github_commit, tech_stack

id	title	category	status	canonical_id	aliases	duplicate_of	source_trust_level	confidence_score	verification_status	tags	raw_sources	last_reinforced	github_commit	tech_stack
wiki-2026-0508-axiomatic-systems	Axiomatic Systems	10_Wiki/Topics	verified	self	Axiomatic Method Formal Systems Deductive Systems	none	A	0.95	applied	logic foundations formal-methods proof type-theory		2026-05-10	pending	language framework Lean/Coq/Agda Lean4/mathlib

Axiomatic Systems

매 한 줄

"매 finite axiom + inference rule → 매 derivable theorem.". Axiomatic system 의 Euclid (BC 300) → Hilbert (1899 Grundlagen) → Gödel (incompleteness 1931) → 매 2026 의 Lean 4 + mathlib (200k+ formalized theorems, 매 working math 의 formal redo) + LLM-augmented proof assistant (Anthropic Claude / DeepMind AlphaProof).

매 핵심

매 Components

• Primitive symbols / vocabulary.
• Axioms: unproved starting propositions.
• Inference rules (modus ponens, generalization).
• Theorems: derivable from axioms via rules.
• Models / interpretations.

매 Properties

• Consistency: 매 contradiction 의 X (¬(P ∧ ¬P) provable).
• Completeness: every true (in model) statement provable.
• Decidability: algorithm to determine theoremhood.
• Soundness: only true things provable.
• Independence: 매 axiom 의 not derivable from others.
• Categoricity: all models isomorphic.

매 Famous Systems

• Euclidean geometry: 5 postulates (parallel postulate independent → non-Euclidean).
• Peano arithmetic (PA): natural numbers; incomplete (Gödel).
• ZFC set theory: foundation of most math; CH independent (Cohen).
• Group / ring / field: abstract algebra.
• Hilbert system / Natural deduction / Sequent calculus: proof formalisms.
• Type theory (Martin-Löf, Calculus of Constructions): foundation for Coq/Lean/Agda.

매 2026 Computational

• Lean 4 + mathlib: rapid formalization (Tao's PFR, Gowers).
• Coq: CompCert verified compiler, 4-color theorem.
• Isabelle: seL4 microkernel.
• AlphaProof / Claude proof: LLM + Lean tactic search.

매 응용

1. Math research (formalized proof).
2. Formal verification (CompCert, seL4, AWS s2n).
3. Cryptographic protocol proof (EasyCrypt, F*).
4. Smart contract verification.

💻 패턴

Pattern 1 — Lean 4: prove a + 0 = a

theorem add_zero (a : Nat) : a + 0 = a := by
  induction a with
  | zero => rfl
  | succ n ih => simp [Nat.add_succ, ih]

Pattern 2 — Coq: list reversal involutive

Theorem rev_involutive : forall (A : Type) (l : list A),
  rev (rev l) = l.
Proof.
  induction l as [| x xs IH].
  - reflexivity.
  - simpl. rewrite rev_app_distr. simpl. rewrite IH. reflexivity.
Qed.

Pattern 3 — Agda: dependent type proof

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

+-identity : (n : ℕ) → n + zero ≡ n
+-identity zero    = refl
+-identity (suc n) = cong suc (+-identity n)

Pattern 4 — Hilbert-style propositional proof

1. P → (Q → P)                   axiom K
2. (P → (Q → R)) → ((P → Q) → (P → R))   axiom S
3. P                              hypothesis
4. Q → P                          MP 1, 3

Pattern 5 — LLM-assisted proof (Lean tactic suggestion)

def llm_tactic(goal_state):
    return claude.complete(f"""You are a Lean 4 proof assistant.
Given goal:
{goal_state}
Suggest one tactic step. Output only the tactic.""")

매 결정 기준

상황	Approach
Math formalization	Lean 4 + mathlib
Verified compiler / OS	Coq (CompCert, seL4)
Type-theory research	Agda / Lean
Crypto protocol	EasyCrypt / F*
Quick logical sketch	Hilbert-style on paper
LLM-augmented	Lean + Claude tactic search

기본값: Lean 4 for new formalization, Coq for legacy verified systems.

🔗 Graph

• 부모: Mathematical-Logic
• 변형: Type Theory
• 응용: Formal-Verification · Theorem-Proving
• Adjacent: Godel-s-Incompleteness-Theorems · Curry-Howard · Theoretical-Computer-Science

🤖 LLM 활용

언제: tactic suggestion, lemma name search in mathlib, proof sketch translation, error diagnosis. 언제 X: producing final certificate without check (use proof assistant), informal-only "proof" claims.

❌ 안티패턴

• Inconsistent axioms: explosion (anything provable).
• Hidden axiom of choice: constructivism violation in proof claimed constructive.
• Tactic blob without lemma factor: maintenance nightmare.
• No model check: theorem 의 vacuous (no model).

🧪 검증 / 중복

• Verified (Lean 4 docs, mathlib4, Hilbert "Grundlagen", Mendelson "Intro to Math Logic").
• 신뢰도 A.

🕓 Changelog

날짜	변경
2026-05-08	Phase 1
2026-05-10	Manual cleanup — FULL content (Lean/Coq/Agda, 5 patterns)