The Translational Approach

• Two mutually recursive translation functions
  • The translation tr captures a formula being T or B
  • The anti-translation atr captures a formula being F or B
  • For an RM3 formula F ...
    • F is T in RM3 if tr(F) is true and atr(F) is false in FOL
    • F is B in RM3 if tr(F) is true and atr(F) is true in FOL
    • F is F in RM3 if tr(F) is false and atr(F) is true in FOL
    • tr(F) and atr(F) cannot both be false in FOL

• Example translation rules

  F		tr(F)		atr(F)
  φ		φ+		φ-
  ¬φ		atr(φ)		tr(φ)
  φ→ψ		¬tr(φ) ∨ ¬atr(ψ) ∨ (tr(φ) ∧ atr(φ) ∧ tr(ψ) ∧ atr(ψ))		tr(φ) ∧ atr(ψ)
  ∀X φ		∀X tr(φ)		∃X atr(φ)

• Additional axioms
  • Exhaustion axiom for each predicate ∀ (φ⁺ ∨ φ^-)

• Axioms ⊨_RM3 Conjecture
      iff
  (tr(Axioms) ∪ Exhaustion) ⊨_FOL tr(Conjecture)
  • Proof based on isomorphism between RM3 and FOL interpretations