The Truth Evaluation Approach
A recursive translation function
trs
For an RM3 formula F and target truth value V (one of
T
,
B
,
F
) ...
trs
(F,V) caputures the conditions for F to be V
Example translation rules (extracted from truth tables)
F
trs
(F,
T
)
trs
(F,
B
)
trs
(F,
F
)
φ
φ
+
∧ ¬φ
-
φ
+
∧ φ
-
¬φ
+
∧ φ
-
¬φ
trs
(φ,
F
)
trs
(φ,
B
)
trs
(φ,
T
)
φ→ψ
trs
(φ,
F
) ∨
trs
(ψ,
T
)
trs
(φ,
B
) ∧
trs
(ψ,
B
)
(complex)
∀X φ
∀X
trs
(φ,
T
)
∃X
trs
(φ,
B
∧ ¬∃X
trs
(φ,
F
))
∃X
trs
(φ,
F
)
Additional axioms
Exhaustion
axiom for each predicate ∀ (φ
+
∨ φ
-
)
Definition
axioms for each predicate ∀ (φ
++
↔ (φ
+
∧ ¬φ
-
)); ∀ (φ
+-
↔ (φ
+
∧ φ
-
)); ∀ (φ
--
↔ (¬φ
+
∧ φ
-
))
Define
des
(F) ≅
trs
(F,
T
) ∨
trs
(F,
B
).
Axioms ⊨
RM3
Conjecture
iff
(
des
(Axioms) ∪ Exhaustion ∪ Definition) ⊨
FOL
des
(Conjecture)
Proof based on isomorphism between RM3 and FOL interpretations
