Constrained Conditional (→_con)

• Constraints on conditional's properties
  • Modus ponens holds
  • Agrees with classical logic for T and F
  • Antecedent F or consequent T, then T
  • Undesignated antecedent, then designated (T or B)
  • Designated antecedent above or equal to consequent
    in either diamond, then consequent
  • For TV₁ ≠ TV₂, TV₁ ↔ TV₂ ≠ T (for →_cmi, (N ↔ F) = T)

• Automated generation of the conditional
  • Encode ∧, ∨ ¬, diamonds, and constraints in FOL
  • Generate finite model, read off conditional, deny and repeat
  • Left to decide ... (N → B) and (N → N), either T or B

• Final decisions
  • (N → N) = T, so that (N ↔ N) = T (else (N ↔ N) = B)
  • (N → B) = B, so that (N → N) ≠ (N → B)

• Strange feature ...
  • ¬(p → q) ⊭ p