Completeness.lean`

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Countable Henkin completeness for the target proof calculus.

theorem OAI.PartitionConsistency.Formula.liftRen_id line 14
theorem OAI.PartitionConsistency.Formula.liftRen_comp line 18
theorem OAI.PartitionConsistency.Formula.rename_id line 23
theorem OAI.PartitionConsistency.Formula.rename_comp line 34
theorem OAI.PartitionConsistency.Formula.instantiate_rename line 49
Source documentation
Instantiation after renaming the free variables extends that renaming by one chosen variable; this is the capture-avoidance identity for witnesses.
```
@[simp] theorem instantiate_rename {n m} (φ : Formula (n + 1))
    (r : Fin n → Fin m) (t : Fin m) :
    (φ.rename (liftRen r)).instantiate t = φ.rename (Fin.snoc r t) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.liftRen, OAI.PartitionConsistency.Formula.instantiate
theorem OAI.PartitionConsistency.Formula.rename_snoc_castSucc_last line 57
theorem OAI.PartitionConsistency.Formula.rename_instantiate line 64
theorem OAI.PartitionConsistency.Derives.eq_symm line 76
theorem OAI.PartitionConsistency.Derives.eq_trans line 82
theorem OAI.PartitionConsistency.Derives.mem_congr line 89
def OAI.PartitionConsistency.Completeness.ContextConsistent line 105
Source documentation
Consistency of an open context, with its displayed finite variable supply.
```
def ContextConsistent {n} (Γ : Set (Formula n)) : Prop := ¬ Derives Γ .bot
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Derives
theorem OAI.PartitionConsistency.Completeness.lift_consistent line 109
Source documentation
Enlarging the variable supply is conservative for a nonempty supply. A retraction substitutes an existing variable for every extra variable.
```
theorem lift_consistent {n m} {Γ : Set (Formula n)} (hn : 0 < n) (hnm : n ≤ m)
    (hΓ : ContextConsistent Γ) :
    ContextConsistent (Formula.rename (Fin.castLE hnm) '' Γ) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Completeness.ContextConsistent, OAI.PartitionConsistency.Formula.rename
theorem OAI.PartitionConsistency.Completeness.consistent_decision line 122
Source documentation
One of the two decisions can always be added without contradiction.
```
theorem consistent_decision {n} {Γ : Set (Formula n)} (hΓ : ContextConsistent Γ)
    (φ : Formula n) :
    ContextConsistent (insert φ Γ) ∨ ContextConsistent (insert φ.neg Γ) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Completeness.ContextConsistent
structure OAI.PartitionConsistency.Completeness.Condition line 135
Source documentation
Henkin conditions are genuine consistent first-order contexts. No satisfiability or model-existence assertion occurs in their definition.
```
structure Condition where
…
```
instance OAI.PartitionConsistency.Completeness.Condition.(instance at line 144) line 144
Source documentation
A stronger condition may have more variables and more assumptions.
```
instance : Preorder Condition where
…
```
Mentions: OAI.PartitionConsistency.Completeness.Condition
def OAI.PartitionConsistency.Completeness.Condition.emb line 161
Source documentation
The canonical embedding of the old variables into a stronger condition.
```
def emb {q p : Condition} (h : q ≤ p) : Fin p.size → Fin q.size := Fin.castLE h.choose
```
Mentions: OAI.PartitionConsistency.Completeness.Condition
theorem OAI.PartitionConsistency.Completeness.Condition.emb_val line 163
theorem OAI.PartitionConsistency.Completeness.Condition.transport line 167
Source documentation
Derivations are preserved by extension of conditions.
```
theorem transport {q p : Condition} (h : q ≤ p) {φ : Formula p.size}
    (hd : Derives p.context φ) : Derives q.context (φ.rename (emb h)) :=
…
```
Mentions: OAI.PartitionConsistency.Completeness.Condition, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Derives, OAI.PartitionConsistency.Completeness.Condition.emb
def OAI.PartitionConsistency.Completeness.Condition.grow line 171
theorem OAI.PartitionConsistency.Completeness.Condition.grow_le line 175
def OAI.PartitionConsistency.Completeness.Condition.add line 178
theorem OAI.PartitionConsistency.Completeness.Condition.add_le line 182
theorem OAI.PartitionConsistency.Completeness.Condition.bound line 192
Source documentation
A condition can always accommodate a given finite tuple of variable codes.
```
theorem bound (p : Condition) {n} (v : Fin n → ℕ) :
    ∃ q : Condition, q ≤ p ∧ ∃ w : Fin n → Fin q.size, ∀ i, (w i).val = v i := by
…
```
Mentions: OAI.PartitionConsistency.Completeness.Condition
theorem OAI.PartitionConsistency.Completeness.snoc_castSucc line 205
Source documentation
Extending the variable map by a new last variable is the binder lift.
```
@[simp] theorem snoc_castSucc {n m} (w : Fin n → Fin m) :
    Fin.snoc (Fin.castSucc ∘ w) (Fin.last m) = Formula.liftRen w := by
…
```
Mentions: OAI.PartitionConsistency.Formula.liftRen
def OAI.PartitionConsistency.Completeness.Condition.exWitness line 214
Source documentation
Adding a fresh local witness is consistent when existence is derivable. This is justified by the eigenvariable rule, not by a model assumption.
```
def exWitness (p : Condition) (φ : Formula (p.size + 1))
    (hφ : Derives p.context (.ex φ)) : Condition where
…
```
Mentions: OAI.PartitionConsistency.Completeness.Condition, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Derives
theorem OAI.PartitionConsistency.Completeness.Condition.exWitness_le line 221
def OAI.PartitionConsistency.Completeness.Condition.allCounterexample line 228
Source documentation
A negated universal has a consistent fresh counterexample context.
```
def allCounterexample (p : Condition) (φ : Formula (p.size + 1))
    (hφ : Derives p.context (Formula.all φ).neg) : Condition where
…
```
Mentions: OAI.PartitionConsistency.Completeness.Condition, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Derives
theorem OAI.PartitionConsistency.Completeness.Condition.allCounterexample_le line 236
def OAI.PartitionConsistency.Completeness.decisions line 246
Source documentation
All finite tuples are explicitly included, so this construction treats all parameters, not just sentences or quantifier-free formulas.
```
def decisions {n} (φ : Formula n) (v : Fin n → ℕ) : Set Condition :=
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Completeness.Condition
def OAI.PartitionConsistency.Completeness.exWitnesses line 250
def OAI.PartitionConsistency.Completeness.allCounterexamples line 255
theorem OAI.PartitionConsistency.Completeness.decisions_dense line 260
theorem OAI.PartitionConsistency.Completeness.exWitnesses_dense line 270
theorem OAI.PartitionConsistency.Completeness.allCounterexamples_dense line 287
abbrev OAI.PartitionConsistency.Completeness.GenericFilter line 304
def OAI.PartitionConsistency.Completeness.IsHenkin line 307
Source documentation
A filter meeting every decision and every local quantifier-witness request.
```
def IsHenkin (G : GenericFilter) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Completeness.GenericFilter
theorem OAI.PartitionConsistency.Completeness.exists_henkin line 313
Source documentation
The countable Henkin construction, using only syntactic consistency.
```
theorem exists_henkin (p₀ : Condition) :
    ∃ G : GenericFilter, p₀ ∈ G ∧ IsHenkin G := by
…
```
Mentions: OAI.PartitionConsistency.Completeness.Condition, OAI.PartitionConsistency.Completeness.GenericFilter, OAI.PartitionConsistency.Completeness.IsHenkin
def OAI.PartitionConsistency.Completeness.Proven line 333
Source documentation
Eventual derivability in the directed filter, with all free variables interpreted as natural-number constant codes.
```
def Proven (G : GenericFilter) {n} (φ : Formula n) (v : Fin n → ℕ) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Completeness.GenericFilter, OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.Completeness.Proven.at_condition line 343
Source documentation
Any existing representation of the tuple can be extended to one carrying the given derivation. Directedness, not an assumed complete theory, is used.
```
theorem at_condition (h : Proven G φ v) {p : Condition} (hp : p ∈ G)
    (w : Fin n → Fin p.size) (hw : ∀ i, (w i).val = v i) :
    ∃ q : Condition, q ∈ G ∧ ∃ hqp : q ≤ p,
      Derives q.context (φ.rename (Condition.emb hqp ∘ w)) := by
…
```
Mentions: OAI.PartitionConsistency.Completeness.Proven, OAI.PartitionConsistency.Completeness.Condition, OAI.PartitionConsistency.Derives, OAI.PartitionConsistency.Completeness.Condition.emb
theorem OAI.PartitionConsistency.Completeness.Proven.joint line 358
Source documentation
Two eventual derivations with the same tuple can be put into a single consistent context with exactly the same variable map.
```
theorem joint (hφ : Proven G φ v) (hψ : Proven G ψ v) :
    ∃ p ∈ G, ∃ w : Fin n → Fin p.size, (∀ i, (w i).val = v i) ∧
      Derives p.context (φ.rename w) ∧ Derives p.context (ψ.rename w) := by
…
```
Mentions: OAI.PartitionConsistency.Completeness.Proven, OAI.PartitionConsistency.Derives
theorem OAI.PartitionConsistency.Completeness.Proven.not_bot line 366
theorem OAI.PartitionConsistency.Completeness.Proven.conjunction line 370
theorem OAI.PartitionConsistency.Completeness.Proven.apply_imp line 378
theorem OAI.PartitionConsistency.Completeness.Proven.contradict line 382
theorem OAI.PartitionConsistency.Completeness.Proven.tuple line 390
Source documentation
This also supplies a filter condition containing any prescribed finite collection of constant codes, including codes not used by a formula.
```
theorem tuple (v : Fin n → ℕ) :
    ∃ p ∈ G, ∃ w : Fin n → Fin p.size, ∀ i, (w i).val = v i := by
…
```
theorem OAI.PartitionConsistency.Completeness.Proven.decision line 395
theorem OAI.PartitionConsistency.Completeness.Proven.negation line 401
theorem OAI.PartitionConsistency.Completeness.Proven.rename_iff line 409
Source documentation
Full substitution of finite variable tuples, in both directions. The reverse implication includes variables unused in the substituted formula.
```
theorem rename_iff {m} (φ : Formula n) (r : Fin n → Fin m) (v : Fin m → ℕ) :
    Proven G (φ.rename r) v ↔ Proven G φ (v ∘ r) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Completeness.Proven
theorem OAI.PartitionConsistency.Completeness.Proven.implication line 421
theorem OAI.PartitionConsistency.Completeness.Proven.disjunction line 434
theorem OAI.PartitionConsistency.Completeness.Proven.all_instance line 452
Source documentation
Universal elimination is a derivable operation on the eventual theory.
```
theorem all_instance {φ : Formula (n+1)} (h : Proven G (.all φ) v) (t : Fin n) :
    Proven G (φ.instantiate t) v := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Completeness.Proven
theorem OAI.PartitionConsistency.Completeness.Proven.exists_iff line 460
Source documentation
The Henkin requests turn existence into an actual constant-code witness.
```
theorem exists_iff (φ : Formula (n+1)) (v : Fin n → ℕ) :
    Proven G (.ex φ) v ↔ ∃ a : ℕ, Proven G φ (Fin.snoc v a) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Completeness.Proven
theorem OAI.PartitionConsistency.Completeness.Proven.all_iff line 478
Source documentation
Universal truth is equivalent to truth for every constant code. The counterexample requests are essential to the reverse implication.
```
theorem all_iff (φ : Formula (n+1)) (v : Fin n → ℕ) :
    Proven G (.all φ) v ↔ ∀ a : ℕ, Proven G φ (Fin.snoc v a) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Completeness.Proven
def OAI.PartitionConsistency.Completeness.EqRel line 500
Source documentation
Equality and membership of constant codes in the canonical term model.
```
def EqRel (G : GenericFilter) (a b : ℕ) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Completeness.GenericFilter
def OAI.PartitionConsistency.Completeness.MemRel line 503
theorem OAI.PartitionConsistency.Completeness.equal_iff line 509
theorem OAI.PartitionConsistency.Completeness.mem_iff line 518
theorem OAI.PartitionConsistency.Completeness.eqRel_refl line 527
theorem OAI.PartitionConsistency.Completeness.eqRel_symm line 536
theorem OAI.PartitionConsistency.Completeness.eqRel_trans line 542
theorem OAI.PartitionConsistency.Completeness.memRel_congr line 551
def OAI.PartitionConsistency.Completeness.termSetoid line 567
Source documentation
Quotient of the natural-number constant codes by their syntactically provable equality.
```
def termSetoid (G : GenericFilter) (hG : IsHenkin G) : Setoid ℕ where
…
```
Mentions: OAI.PartitionConsistency.Completeness.GenericFilter, OAI.PartitionConsistency.Completeness.IsHenkin
def OAI.PartitionConsistency.Completeness.TermModel line 571
def OAI.PartitionConsistency.Completeness.termClass line 573
instance OAI.PartitionConsistency.Completeness.termModel_nonempty line 576
instance OAI.PartitionConsistency.Completeness.termModel_countable line 577
def OAI.PartitionConsistency.Completeness.termMem line 582
Source documentation
Membership is independent of representatives because first-order equality has its actual substitution rule.
```
def termMem (G : GenericFilter) (hG : IsHenkin G) :
    TermModel G hG → TermModel G hG → Prop :=
…
```
Mentions: OAI.PartitionConsistency.Completeness.GenericFilter, OAI.PartitionConsistency.Completeness.IsHenkin, OAI.PartitionConsistency.Completeness.TermModel
theorem OAI.PartitionConsistency.Completeness.term_truth line 589
Source documentation
Truth in the countable term model, for every formula and every tuple of constant codes. This is syntactic completeness, not compactness assumed as a premise or semantic consistency used as a definition.
```
theorem term_truth {n} (φ : Formula n) (v : Fin n → ℕ) :
    Formula.Realize (termMem G hG) (termClass G hG ∘ v) φ ↔ Proven G φ v := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.Realize, OAI.PartitionConsistency.Completeness.termMem, OAI.PartitionConsistency.Completeness.termClass, OAI.PartitionConsistency.Completeness.Proven
theorem OAI.PartitionConsistency.Completeness.exists_countable_model line 625
Source documentation
Countable-model completeness for the actual finite-derivation consistency predicate used in the target. No transitive or externally well-founded model is asserted. The domain is concretely a quotient of ℕ.
```
theorem exists_countable_model {T : Theory} (hT : Consistent T) :
    ∃ M : Type, Nonempty M ∧ Countable M ∧ ∃ E : M → M → Prop, Models E T := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.Models
theorem OAI.PartitionConsistency.Completeness.consistent_iff_has_countable_model line 643
Source documentation
Equivalence of syntactic consistency and countable nonempty models for this first-order language. This does not perform the constructible or symmetric-forcing interpretations required in main_consistency.
```
theorem consistent_iff_has_countable_model (T : Theory) :
    Consistent T ↔
      ∃ M : Type, Nonempty M ∧ Countable M ∧ ∃ E : M → M → Prop, Models E T := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Consistent, OAI.PartitionConsistency.Models