1
Overview
▶
1.1
What Has Been Built
1.2
How To Read The Blueprint
1.3
The Current Frontier
1.4
Formalization Note
2
First-Order Logic Core
▶
2.1
Languages, Terms, And Formulas
2.2
Derivability
2.3
Structures And Satisfaction
2.4
Sentences, Theories, And Bounded Syntax
2.5
A Model-Theoretic Example
2.6
Formalization Note
3
Compactness And Completion
▶
3.1
Compactness As A Finitary Principle
3.2
Compactness For Theories
3.3
Controlled Unions
3.4
Chains Of Consistent Extensions
3.5
Maximal Consistent Extensions
3.6
Why This Matters Later
3.7
Formalization Note
4
Colimits And Language Extensions
▶
4.1
Directed Systems And Their Colimits
4.2
Maps Of Languages
4.3
Symbol Support And Filtered Languages
4.4
Proof Transport And Reducts
4.5
Reflection Along Injective Language Maps
4.6
Fresh Constants And Generalization
4.7
Role In Henkinization
4.8
Formalization Note
5
Henkinization
▶
5.1
Adjoining Witness Constants In One Step
5.2
Iterating The Construction
5.3
The Infinite Henkin Language
5.4
Finite-Stage Representatives
5.5
Witness Sentences And Enough Constants
5.6
The One-Step Theory Extension
5.7
Consistency Of One Henkin Step
5.8
Passing To The Limit Theory
5.9
Enough Constants In The Limit
5.10
Complete Henkin Extensions
5.11
Present Boundary
5.12
Formalization Note
6
Status And Next Frontier
▶
6.1
What The Current Port Delivers
6.2
What Is Not Yet Present
6.3
The Next Frontier
6.4
How The Blueprint Should Grow
Dependency graph
Flypitch Lean 4
zj
1
Overview
1.1
What Has Been Built
1.2
How To Read The Blueprint
1.3
The Current Frontier
1.4
Formalization Note
2
First-Order Logic Core
2.1
Languages, Terms, And Formulas
2.2
Derivability
2.3
Structures And Satisfaction
2.4
Sentences, Theories, And Bounded Syntax
2.5
A Model-Theoretic Example
2.6
Formalization Note
3
Compactness And Completion
3.1
Compactness As A Finitary Principle
3.2
Compactness For Theories
3.3
Controlled Unions
3.4
Chains Of Consistent Extensions
3.5
Maximal Consistent Extensions
3.6
Why This Matters Later
3.7
Formalization Note
4
Colimits And Language Extensions
4.1
Directed Systems And Their Colimits
4.2
Maps Of Languages
4.3
Symbol Support And Filtered Languages
4.4
Proof Transport And Reducts
4.5
Reflection Along Injective Language Maps
4.6
Fresh Constants And Generalization
4.7
Role In Henkinization
4.8
Formalization Note
5
Henkinization
5.1
Adjoining Witness Constants In One Step
5.2
Iterating The Construction
5.3
The Infinite Henkin Language
5.4
Finite-Stage Representatives
5.5
Witness Sentences And Enough Constants
5.6
The One-Step Theory Extension
5.7
Consistency Of One Henkin Step
5.8
Passing To The Limit Theory
5.9
Enough Constants In The Limit
5.10
Complete Henkin Extensions
5.11
Present Boundary
5.12
Formalization Note
6
Status And Next Frontier
6.1
What The Current Port Delivers
6.2
What Is Not Yet Present
6.3
The Next Frontier
6.4
How The Blueprint Should Grow