ForcingTruth.lean`

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.force_symmetry line 14
Source documentation
Induction through the defined logical forcing relation propagates a condition/name automorphism from the atomic cases to each fixed formula. The existential clause remains density of local witnesses.
```
theorem force_symmetry (e : P ≃o P) (f : N ≃ N)
    (heq : ∀ p a b, A.EqF p a b ↔ A.EqF (e p) (f a) (f b))
    (hmem : ∀ p a b, A.MemF p a b ↔ A.MemF (e p) (f a) (f b))
    {n} (φ : BasicFormula n) (v : Fin n → N) (p : P) :
    A.Force v p φ ↔ A.Force (f ∘ v) (e p) φ := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.BasicFormula
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.Regular line 55
Source documentation
The ordinary forcing relation is regular: density of atomic forcing below p already implies forcing at p. This property is separately verified by the actual name recursion, not assumed for any target axiom.
```
def Regular : Prop :=
…
```
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.force_of_dense line 60
Source documentation
Dense closure extends from the atomic relations to every fixed formula.
```
theorem force_of_dense (hA : A.Regular) {n} (φ : BasicFormula n) (v : Fin n → N)
    (p : P) (h : ∀ q, q ≤ p → ∃ r, r ≤ q ∧ A.Force v r φ) : A.Force v p φ := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.BasicFormula
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.exists_force_neg line 84
def OAI.PartitionConsistency.ForcingQuotient.AtomicData.ForceFormula line 98
Source documentation
Forcing in the full syntax of the statement is the previously defined Boolean/existential-basis forcing, with no change of quantifier domain.
```
def ForceFormula {n} (v : Fin n → N) (p : P) (φ : Formula n) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_mono line 101
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_of_dense line 105
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_bot line 109
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_mem line 112
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_equal line 115
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_conj line 118
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_imp line 121
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_neg line 132
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_disj line 136
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_ex line 150
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_all line 154
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_rename line 168
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_raise line 186
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_instantiate line 193
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.force_tuple_congr line 203
Source documentation
Equality substitution for all formulas follows from the atomic laws.
```
theorem force_tuple_congr {n} (φ : BasicFormula n) (v w : Fin n → N) (p : P)
    (hvw : ∀ i, A.EqF p (v i) (w i)) : A.Force v p φ ↔ A.Force w p φ := by
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.BasicFormula
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forceFormula_tuple_congr line 233
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.forcing_sound line 240
Source documentation
Soundness for the actual classical calculus in forcing semantics. Unlike the quotient-model argument this needs no countability assumption on the full collection of names and constructs no generic over all names.
```
theorem forcing_sound (hA : A.Regular) {n} {Γ : Set (Formula n)} {φ : Formula n}
    (h : Derives Γ φ) (v : Fin n → N) (p : P)
    (hΓ : ∀ ψ ∈ Γ, A.ForceFormula v p ψ) : A.ForceFormula v p φ := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.Derives
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.consistent_of_regular_forcing line 332
Source documentation
A nonempty regular forcing semantics yields ordinary syntactic consistency for any theory whose axioms are all forced. Neither an externally generic filter nor a countable class of names is needed. This is not an assertion that the target axioms are forced in the constructed symmetric system.
```
theorem consistent_of_regular_forcing (hA : A.Regular) [Nonempty N] (p : P)
    {T : Theory} (hT : ∀ φ ∈ T, A.ForceFormula Fin.elim0 p φ) : Consistent T := by
…
```
Mentions: OAI.PartitionConsistency.Theory, OAI.PartitionConsistency.Consistent
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.data_regular line 351
Source documentation
Actual name forcing has all the regularity needed for classical logical soundness, as a theorem of the recursion on sets.
```
theorem data_regular (code : P → ZFSet.{u}) (N : Set ZFSet.{u}) : (data code N).Regular := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.data