Proofs.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Logical and set-forcing foundations

inductive OAI.PartitionConsistency.Formula line 30
Source documentation
Pure first-order membership syntax with equality. n variables are in scope. A quantifier binds the last variable in its body. There are no atoms/urelements, function symbols, constants, semantic predicates, or mathematical assumptions in this syntax.
Also declared: ComparatorChallenges/PartitionConsistency.lean:11 (same declaration text).
```
inductive Formula : ℕ → Type where
…
```
abbrev OAI.PartitionConsistency.Formula.neg line 42
Also declared: ComparatorChallenges/PartitionConsistency.lean:23 (same declaration text).
abbrev OAI.PartitionConsistency.Formula.iff line 43
Also declared: ComparatorChallenges/PartitionConsistency.lean:24 (same declaration text).
def OAI.PartitionConsistency.Formula.liftRen line 46
Source documentation
Under a binder, a renaming leaves the newly bound variable bound.
Also declared: ComparatorChallenges/PartitionConsistency.lean:27 (same declaration text).
```
def liftRen {n m} (r : Fin n → Fin m) : Fin (n + 1) → Fin (m + 1) :=
…
```

def OAI.PartitionConsistency.Formula.rename line 50

Source documentation

Capture-avoiding renaming; in this relational language all terms are variables.

Also declared: ComparatorChallenges/PartitionConsistency.lean:31 (same declaration text).

def rename {n m} (r : Fin n → Fin m) : Formula n → Formula m
  | .bot => .bot
  | .mem x y => .mem (r x) (r y)
  | .equal x y => .equal (r x) (r y)
  | .imp p q => .imp (rename r p) (rename r q)
  | .conj p q => .conj (rename r p) (rename r q)
  | .disj p q => .disj (rename r p) (rename r q)
  | .all p => .all (rename (liftRen r) p)
  | .ex p => .ex (rename (liftRen r) p)

Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Formula.liftRen

abbrev OAI.PartitionConsistency.Formula.raise line 60
Also declared: ComparatorChallenges/PartitionConsistency.lean:41 (same declaration text).
def OAI.PartitionConsistency.Formula.instantiate line 63
Source documentation
Substitution of a variable term for the variable just quantified.
Also declared: ComparatorChallenges/PartitionConsistency.lean:44 (same declaration text).
```
def instantiate {n} (p : Formula (n + 1)) (x : Fin n) : Formula n :=
…
```
Mentions: OAI.PartitionConsistency.Formula

def OAI.PartitionConsistency.Formula.close line 67

Source documentation

Universal closure of all the free variables.

Also declared: ComparatorChallenges/PartitionConsistency.lean:48 (same declaration text).

def close : {n : ℕ} → Formula n → Formula 0
  | 0, p => p
  | _ + 1, p => close (.all p)

/-- Satisfaction in an arbitrary relational structure, not necessarily externally
well founded or transitive. In particular, `E` need not be Lean's membership. -/

Mentions: OAI.PartitionConsistency.Formula

def OAI.PartitionConsistency.Formula.Realize line 73

Source documentation

Satisfaction in an arbitrary relational structure, not necessarily externally well founded or transitive. In particular, E need not be Lean's membership.

def Realize {M : Type*} (E : M → M → Prop) {n} (v : Fin n → M) : Formula n → Prop
  | .bot => False
  | .mem x y => E (v x) (v y)
  | .equal x y => v x = v y
  | .imp p q => Realize E v p → Realize E v q
  | .conj p q => Realize E v p ∧ Realize E v q
  | .disj p q => Realize E v p ∨ Realize E v q
  | .all p => ∀ x : M, Realize E (Fin.snoc v x) p
  | .ex p => ∃ x : M, Realize E (Fin.snoc v x) p

Mentions: OAI.PartitionConsistency.Formula

theorem OAI.PartitionConsistency.Formula.snoc_comp_liftRen line 83
theorem OAI.PartitionConsistency.Formula.realize_rename line 89
theorem OAI.PartitionConsistency.Formula.realize_raise line 102
theorem OAI.PartitionConsistency.Formula.realize_instantiate line 111
abbrev OAI.PartitionConsistency.Sentence line 122
Also declared: ComparatorChallenges/PartitionConsistency.lean:54 (same declaration text).
abbrev OAI.PartitionConsistency.Theory line 123
Also declared: ComparatorChallenges/PartitionConsistency.lean:55 (same declaration text).
inductive OAI.PartitionConsistency.Derives line 129
Source documentation
Classical first-order natural deduction with equality. Hypotheses may be an infinite theory, but a derivation is a finite inductive proof. The allI and exE rules use a fresh last variable, and shift all assumptions to avoid capture. We allow finitely many free variables in proofs of closed sentences.
Also declared: ComparatorChallenges/PartitionConsistency.lean:61 (same declaration text).
```
inductive Derives : {n : ℕ} → Set (Formula n) → Formula n → Prop where
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.Theory.at line 170
Source documentation
Sentences are usable as open hypotheses with any finite supply of variables.
Also declared: ComparatorChallenges/PartitionConsistency.lean:102 (same declaration text).
```
def Theory.at (T : Theory) (n : ℕ) : Set (Formula n) :=
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.Consistent line 175
Source documentation
Ordinary syntactic consistency: there is no finite natural-deduction proof of falsity from the theory, with any finite supply of free variables.
Also declared: ComparatorChallenges/PartitionConsistency.lean:107 (same declaration text).
```
def Consistent (T : Theory) : Prop := ∀ n, ¬ Derives (T.at n) .bot
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Derives
def OAI.PartitionConsistency.Models line 179
Source documentation
A model here is an arbitrary membership structure. This definition places no external well-foundedness, transitivity, or cardinal assumptions on the model.
```
def Models {M : Type*} (E : M → M → Prop) (T : Theory) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Theory
theorem OAI.PartitionConsistency.Derives.sound line 183
Source documentation
Soundness of the explicitly specified proof calculus.
```
theorem Derives.sound {n} {Γ : Set (Formula n)} {p : Formula n} (h : Derives Γ p)
    {M : Type*} (E : M → M → Prop) (v : Fin n → M)
    (hΓ : ∀ q ∈ Γ, Formula.Realize E v q) : Formula.Realize E v p := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Derives, OAI.PartitionConsistency.Formula.Realize
theorem OAI.PartitionConsistency.consistent_of_model line 251
Source documentation
The final soundness step of the source's metatheoretic argument. Unlike main_consistency, this helper does not construct any model.
```
theorem consistent_of_model {M : Type*} [Nonempty M] (E : M → M → Prop)
    {T : Theory} (h : Models E T) : Consistent T := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Models, OAI.PartitionConsistency.Consistent
theorem OAI.PartitionConsistency.Derives.drop_subset line 268
Source documentation
Removing an introduced assumption from a support leaves a subset of the original context.
```
private theorem drop_subset {α : Type*} {S Γ : Set α} {p : α}
    (h : S ⊆ insert p Γ) : S \ {p} ⊆ Γ := by
…
```
theorem OAI.PartitionConsistency.Derives.subset_insert_drop line 275
theorem OAI.PartitionConsistency.Derives.finite_support line 285
Source documentation
Every natural-deduction proof uses only finitely many assumptions, even though its context is allowed to be an arbitrary set. This statement covers both variable renaming and the fresh-variable quantifier rules.
```
theorem finite_support {n} {Γ : Set (Formula n)} {p : Formula n} (h : Derives Γ p) :
    ∃ Δ : Set (Formula n), Δ.Finite ∧ Δ ⊆ Γ ∧ Derives Δ p := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Derives
theorem OAI.PartitionConsistency.Consistent.mono line 382
Source documentation
Restricting the axioms of a consistent theory preserves consistency.
```
theorem Consistent.mono {T S : Theory} (h : Consistent T) (hST : S ⊆ T) :
    Consistent S := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Consistent
theorem OAI.PartitionConsistency.consistent_iff_finite line 391
Source documentation
A finite contradiction from a theory already follows from a finite subtheory. This formulates the finite-axiom step needed by the source's proof-translation alternative, without assuming that translation exists.
```
theorem consistent_iff_finite {T : Theory} :
    Consistent T ↔ ∀ S : Theory, S.Finite → S ⊆ T → Consistent S := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Consistent