Model Checking Examples

Mathematical Logic · Axiom Academy

EXAMPLE Model Checking Examples Step-by-step walkthrough of model checking in first-order logic Example 2: Checking if Structure is a Model Example 3: Finding a Counterexample to Show Non-Validity Goal: Show this is not valid by finding a counterexample structure Example 4: Verifying Formula Satisfiability Goal: Determine if there exists a structure where this formula is true Excellent work! You've mastered the fundamentals of model checking in first-order logic. Here's what we learned: Evaluating Quantified Formulas: For ∀x∃y R(x,y), we must check that for every element x in the domain, there exists some y such that R(x,y) holds. All universal quantifiers must be satisfied. Model Verification: A structure is a model of a set of axioms if and only if every axiom evaluates to true in that structure. If even one axiom fails, the structure is not a model. Counterexamples for Non-Validity: To show a formula is not valid, we only need to find one structure where it evaluates to false. This single counterexample is sufficient to disprove validity. Satisfiability vs. Validity: Satisfiability requires finding at least one structure where the formula is true. Validity requires the formula to be true in all possible structures. Systematic Approach: When model checking, work systematically through quantifiers from outside to inside, keeping track of which elements satisfy the conditions at each step.

This is the written version of the interactive lesson above. See the full Mathematical Logic course.