MatchingLogic.EntryIII.Regression

inductive MatchingLogic.EntryIIIRegression.AuditSym : Type

The nullary and unary symbols used by the regression models.

• nullary : AuditSym
• unary : AuditSym

@[instance_reducible]

instance MatchingLogic.EntryIIIRegression.instDecidableEqAuditSym : DecidableEq AuditSym

Equations

• MatchingLogic.EntryIIIRegression.instDecidableEqAuditSym x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MatchingLogic.EntryIIIRegression.instFintypeAuditSym : Fintype AuditSym

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MatchingLogic.EntryIIIRegression.AuditSig : Signature

The regression signature with one constant and one unary operation.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MatchingLogic.EntryIIIRegression.auditModel : Model AuditSig

A Boolean model used to audit nullary and unary semantics.

Equations

• One or more equations did not get rendered due to their size.

def MatchingLogic.EntryIIIRegression.auditRho : ℕ → auditModel.carrier

The constant-false valuation in auditModel.

Equations

• MatchingLogic.EntryIIIRegression.auditRho x✝ = false

def MatchingLogic.EntryIIIRegression.nullaryPattern : Pattern AuditSig ℕ

The application of the nullary regression symbol.

Equations

• One or more equations did not get rendered due to their size.

def MatchingLogic.EntryIIIRegression.unaryPattern : Pattern AuditSig ℕ

The unary regression symbol applied to variable zero.

Equations

• One or more equations did not get rendered due to their size.

theorem MatchingLogic.EntryIIIRegression.bot_not_global_consequence : ¬GlobalCons ∅ Pattern.bot

Bottom is not even a semantic consequence of the empty theory.

theorem MatchingLogic.EntryIIIRegression.open_var_not_global_consequence : ¬GlobalCons ∅ (Pattern.var 0)

An open variable is not a semantic consequence of the empty theory.

theorem MatchingLogic.EntryIIIRegression.bot_not_empty_theorem : ¬Provable ∅ Pattern.bot

Soundness transfers the explicit bottom countermodel to non-provability.

theorem MatchingLogic.EntryIIIRegression.open_var_not_empty_theorem : ¬Provable ∅ (Pattern.var 0)

Soundness transfers the explicit open-variable countermodel to theoremhood.

theorem MatchingLogic.EntryIIIRegression.global_completeness_bottom_both_false : ¬GlobalCons ∅ Pattern.bot ∧ ¬Provable ∅ Pattern.bot ∧ (GlobalCons ∅ Pattern.bot ↔ Provable ∅ Pattern.bot)

At bottom, the final global-completeness equivalence relates two false sides.

theorem MatchingLogic.EntryIIIRegression.nullary_closed : Closed nullaryPattern

theorem MatchingLogic.EntryIIIRegression.nullary_not_empty_theorem : ¬Provable ∅ nullaryPattern

A closed constant pattern with singleton denotation is not theoremhood.

theorem MatchingLogic.EntryIIIRegression.unary_open : ¬Closed unaryPattern

theorem MatchingLogic.EntryIIIRegression.unary_not_empty_theorem : ¬Provable ∅ unaryPattern

A unary application of an open variable is likewise not theoremhood.

theorem MatchingLogic.EntryIIIRegression.locConsistent_of_semantic_point {Gamma : Set (Pattern AuditSig ℕ)} (M : Model AuditSig) (rho : ℕ → M.carrier) (u : M.carrier) (hu : u ∈ M.denoteSet rho Gamma) : LocConsistent Gamma

A concrete semantic point rules out local inconsistency.

theorem MatchingLogic.EntryIIIRegression.nullary_has_semantic_point : false ∈ auditModel.denoteSet auditRho {nullaryPattern}

theorem MatchingLogic.EntryIIIRegression.unary_has_semantic_point : false ∈ auditModel.denoteSet auditRho {unaryPattern}

theorem MatchingLogic.EntryIIIRegression.nullary_singleton_locConsistent : LocConsistent {nullaryPattern}

theorem MatchingLogic.EntryIIIRegression.unary_singleton_locConsistent : LocConsistent {unaryPattern}

theorem MatchingLogic.EntryIIIRegression.reflexive_local_antecedent : LocalCons {Pattern.var 0} (Pattern.var 0)

The semantic antecedent used below is inhabited by reflexivity.

theorem MatchingLogic.EntryIIIRegression.strong_completeness_has_nonempty_witness : ∃ (l : List (Pattern AuditSig ℕ)), l ≠ [] ∧ (∀ delta ∈ l, delta ∈ {Pattern.var 0}) ∧ Provable ∅ ((conj l).imp (Pattern.var 0))

Completeness at {x} ⊨loc x cannot escape via an empty finite witness.

theorem MatchingLogic.EntryIIIRegression.empty_list_locConsistent : LocConsistent {delta : Pattern AuditSig ℕ | delta ∈ []}

theorem MatchingLogic.EntryIIIRegression.top_list_locConsistent : LocConsistent {delta : Pattern AuditSig ℕ | delta ∈ [Pattern.tp]}

theorem MatchingLogic.EntryIIIRegression.finite_model_existence_returns_actual_point : ∃ (M : Model AuditSig) (rho : ℕ → M.carrier) (u : M.carrier), u ∈ M.denoteSet rho {delta : Pattern AuditSig ℕ | delta ∈ [Pattern.tp]}

Finite model existence returns a concrete model, valuation, and carrier point.

@[instance_reducible]

noncomputable def MatchingLogic.EntryIIIRegression.instEncodableAuditSym : Encodable AuditSym

The finite encoding used by the canonical-model regression tests.

Equations

• MatchingLogic.EntryIIIRegression.instEncodableAuditSym = Fintype.toEncodable MatchingLogic.EntryIIIRegression.AuditSym

theorem MatchingLogic.EntryIIIRegression.auditPatternCountable : Countable (Pattern AuditSig ℕ)

theorem MatchingLogic.EntryIIIRegression.canonical_existence_nullary_branch (Gamma : CanonicalCarrier AuditSig) (happ : nullaryPattern ∈ ↑Gamma) : ∃ (components : Fin (AuditSig.arity AuditSym.nullary) → CanonicalCarrier AuditSig), (∀ (i : Fin (AuditSig.arity AuditSym.nullary)), (fun (j : Fin (AuditSig.arity AuditSym.nullary)) => j.elim0) i ∈ ↑(components i)) ∧ Gamma ∈ canonicalInterp AuditSym.nullary components

theorem MatchingLogic.EntryIIIRegression.canonical_existence_unary_branch (Gamma : CanonicalCarrier AuditSig) (happ : unaryPattern ∈ ↑Gamma) : ∃ (components : Fin (AuditSig.arity AuditSym.unary) → CanonicalCarrier AuditSig), (∀ (i : Fin (AuditSig.arity AuditSym.unary)), Pattern.var 0 ∈ ↑(components i)) ∧ Gamma ∈ canonicalInterp AuditSym.unary components

theorem MatchingLogic.EntryIIIRegression.actual_canonical_nullary_branch : ∃ (root : CanonicalCarrier AuditSig) (components : Fin (AuditSig.arity AuditSym.nullary) → CanonicalCarrier AuditSig), root ∈ canonicalInterp AuditSym.nullary components

The nullary canonical-existence branch is invoked from an inhabited MCS premise.

theorem MatchingLogic.EntryIIIRegression.actual_canonical_unary_branch : ∃ (root : CanonicalCarrier AuditSig) (components : Fin (AuditSig.arity AuditSym.unary) → CanonicalCarrier AuditSig), Pattern.var 0 ∈ ↑(components ⟨0, ⋯⟩) ∧ root ∈ canonicalInterp AuditSym.unary components

The positive-arity canonical branch is likewise invoked from a real premise.

theorem MatchingLogic.EntryIIIRegression.canonical_constructions_are_inhabited : ∃ (root : CanonicalCarrier AuditSig), Nonempty (canonicalModel root).carrier ∧ Nonempty (generatedModel root).carrier ∧ Nonempty (completedModel root).carrier ∧ completedEmbed root (generatedRoot root) ∈ Set.univ

Canonical, generated, and completed model carriers all expose real points.

def MatchingLogic.EntryIIIRegression.HugeSig : Signature

An ambient symbol type with no countability assumption.

Equations

• MatchingLogic.EntryIIIRegression.HugeSig = { Sym := Set ℕ, arity := fun (x : Set ℕ) => 1 }

theorem MatchingLogic.EntryIIIRegression.arbitrary_ambient_signature_reduction_is_exercised : FiniteLocalModelExistence HugeSig ℕ ∧ StrongLocalCompleteness HugeSig ℕ

The finite-support reduction reaches the unconditional ambient result.