Supporting results for pointwise provable equality.

Soundness theorem for first-order classical logic

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.sound {L : Language} {M : Type u_1} [s : Tarski.Structure L M] [Nonempty M] (f : ℕ → M) {Γ : Sequent L} : ∀ (a : ⊢ᴸᴷ¹ Γ), ∃ φ ∈ Γ, (Semiformula.Evalf f) φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.LK.Derivation.nil_empty {L : Language} : IsEmpty (⊢ᴸᴷ¹ 0)

theorem PointwiseComposition.FFL.FirstOrder.LK.Proof.sound {L : Language} {M : Type u_1} [s : Tarski.Structure L M] [Nonempty M] {φ : Proposition L} (f : ℕ → M) : 𝐋𝐊¹ ⊢ φ → (Semiformula.Evalf f) φ

theorem PointwiseComposition.FFL.FirstOrder.Theory.Proof.sound_proposition {L : Language} {T : Theory L} {φ : Sentence L} {M : Type u_1} [s : Tarski.Structure L M] [Nonempty M] : T ⊢ φ → M↓[L] ⊧* T → (Semiformula.Realize M) φ

theorem PointwiseComposition.FFL.FirstOrder.Theory.Proof.sound {L : Language} {T : Theory L} {φ : Sentence L} : T ⊢ φ → T ⊨[Tarski.Struc L] φ

Soundness theorem for first-order logic.

theorem PointwiseComposition.FFL.FirstOrder.Theory.Proof.sound_small {L : Language} {T : Theory L} {φ : Sentence L} : T ⊢ φ → Consequence T φ

instance PointwiseComposition.FFL.FirstOrder.Theory.instSoundSentenceSetStrucModels {L : Language} (T : Theory L) : Sound T (Semantics.models (Tarski.Struc L) T)

theorem PointwiseComposition.FFL.FirstOrder.Theory.consistent_of_satisfiable {L : Language} {T : Theory L} (h : Semantics.Satisfiable (Tarski.Struc L) T) : Entailment.Consistent T

theorem PointwiseComposition.FFL.FirstOrder.consistent_of_model {L : Language} (T : Theory L) (M : Type u_1) [Nonempty M] [Tarski.Structure L M] [hM : M↓[L] ⊧* T] : Entailment.Consistent T

theorem PointwiseComposition.FFL.FirstOrder.unprovable_of_countermodel {L : Language} (T : Theory L) {M : Type u_1} [Nonempty M] [Tarski.Structure L M] [hM : M↓[L] ⊧* T] {φ : Sentence L} : M↓[L] ⊭ φ → T ⊬ φ

theorem PointwiseComposition.FFL.FirstOrder.models_of_provable {L : Language} {T : Theory L} {M : Type u_1} [Nonempty M] [Tarski.Structure L M] (hT : M↓[L] ⊧* T) {φ : Sentence L} (h : T ⊢ φ) : M↓[L] ⊧ φ

theorem PointwiseComposition.FFL.FirstOrder.models_of_subtheory {L : Language} {T U : Theory L} {M : Type u_1} [Nonempty M] [Tarski.Structure L M] [T ≼ U] : M↓[L] ⊧* U → M↓[L] ⊧* T