---
id: wiki-2026-0508-axiomatic-systems
title: Axiomatic Systems
category: 10_Wiki/Topics
status: verified
canonical_id: self
aliases: [Axiomatic Method, Formal Systems, Deductive Systems]
duplicate_of: none
source_trust_level: A
confidence_score: 0.95
verification_status: applied
tags: [logic, foundations, formal-methods, proof, type-theory]
raw_sources: []
last_reinforced: 2026-05-10
github_commit: pending
tech_stack:
  language: Lean/Coq/Agda
  framework: 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

```lean
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

```coq
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

```agda
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)

```python
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) |