[Merged by Bors] - feat(model_theory/terms_and_formulas): Define satisfiability and semantic equivalence of formulas #11928
Conversation
awainverse
added
the
awaiting-review
jcommelin
added
awaiting-author
awainverse
added
awaiting-review
| /-- Two (bounded) formulas are semantically equivalent over a theory `T` when they have the same | ||
| interpretation in every model of `T`. (This is also known as logical equivalence, which also has a | ||
| proof-theoretic definition.) -/ | ||
| def semantically_equivalent (T : L.Theory) (φ ψ : L.bounded_formula α n) : Prop := |
There was a problem hiding this comment.
Do we also want the predicate "φ and ψ are semantically equivalent in M"?
That might be more convenient, especially since that doesn't require a universe restriction on M.
There was a problem hiding this comment.
I've been studying flypitch more, and I'm now thinking that the right move for this is to define what it means for a theory to model a sentence, and then have this be defined as a theory modelling the implication. Thus I think I might remove semantic equivalence from this PR and revisit it shortly.
There was a problem hiding this comment.
I also think that means I'll require that the witnessing model be nonempty.
There was a problem hiding this comment.
I've done something like I suggested above. I could easily add some more basic API, but this probably is enough for this PR.
fpvandoorn
added
awaiting-author
awainverse
added
awaiting-review
src/model_theory/basic.lean
Outdated
| @@ -130,6 +133,11 @@ instance : has_coe_t L.const M := | |||
| lemma fun_map_eq_coe_const {c : L.const} {x : fin 0 → M} : | |||
| fun_map c x = c := congr rfl (funext fin.elim0) | |||
|
|
|||
| /-- This throws errors as an instance, but could be useful for showing that a particular class of | |||
| structures must be nonempty. -/ | |||
There was a problem hiding this comment.
Please describe the statement first, then explain why this can't be an instance.
There was a problem hiding this comment.
I've done my best to diagnose it. I believe the problem is that the assumptions depend on L but the conclusions do not. It however may still be useful later for a particular language.
|
bors merge |
github-actions
bot
added
ready-to-merge
…ntic equivalence of formulas (#11928) Defines satisfiability of theories Provides a default model of a satisfiable theory Defines semantic (logical) equivalence of formulas
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Defines satisfiability of theories
Provides a default model of a satisfiable theory
Defines semantic (logical) equivalence of formulas