MatchingLogic.Completeness #
Theorem 14 and Corollary 15 #
theorem
MatchingLogic.proof_theoretic_localization
{S : Signature}
{Var : Type}
[DecidableEq Var]
(hL : StrongLocalCompleteness S Var)
(hS : Soundness S Var)
{Γ : Set (Pattern S Var)}
{φ : Pattern S Var}
(hΓ : ∀ γ ∈ Γ, Closed γ)
(hφ : Closed φ)
:
Theorem 14 (proof-theoretic localization). Γ ⊢ φ ↔ Δ_Γ ⊨loc φ.
theorem
MatchingLogic.global_completeness
{S : Signature}
{Var : Type}
[DecidableEq Var]
(hL : StrongLocalCompleteness S Var)
(hS : Soundness S Var)
{Γ : Set (Pattern S Var)}
{φ : Pattern S Var}
(hΓ : ∀ γ ∈ Γ, Closed γ)
(hφ : Closed φ)
:
Corollary 15 (one-sorted global completeness). Γ ⊨ φ ↔ Γ ⊢ φ.
This is the paper's main positive result, and entry point (ii) of its mechanization challenge: Corollary 15 with (L) and (S) assumed.