The Truth Evaluation Approach

A recursive translation function trs
- For a logic XYZ, formula F and target truth value TV (of XYZ) ...
  trs(F,TV) captures the conditions for F to be TV

Example translation rules

Rules for atoms are fixed
Rules for unary and binary connectives generated from truth tables
Rules for quantified formulae based on the Truth Diamond

F trs(F,T) trs(F,B) trs(F,N) trs(F,F)

φ φ^cT ∧ ¬φ^cF φ^cT ∧ φ^cF ¬φ^cT ∧ ¬φ^cF ¬φ^cT ∧ φ^cF
¬φ trs(φ,F) trs(φ,B) trs(φ,N) trs(φ,T)
φ →_cmi ψ trs(φ,N) ∨
trs(φ,F) ∨
trs(ψ,T) (trs(φ,T) ∨
trs(φ,B)) ∧
trs(ψ,B) (trs(φ,T) ∨
trs(φ,B)) ∧
trs(ψ,N) (trs(φ,T) ∨
trs(φ,B)) ∧
trs(ψ,F)
∀X φ ∀X trs(φ,T) ∃X trs(φ,B ∧
¬∃X trs(φ,F)) ∃X trs(φ,N ∧
¬∃X trs(φ,F)) ∃X trs(φ,F)

Additional axioms
- Definition axioms (for truth values of XYZ)
  ∀ (φ^T ↔ (φ^cT ∧ ¬φ^cF)); ∀ (φ^B ↔ (φ^cT ∧ φ^cF));
  ∀ (φ^N ↔ (¬φ^cT ∧ ¬φ^cF)); ∀ (φ^F ↔ (¬φ^cT ∧ φ^cF))
- Exhaustion axiom (for truth values of XYZ)
  ∀ (φ^T ∨ φ^B ∨ φ^N ∨ φ^F)
Define des(F) ≅ Disjunction of trs(F,DTV) for Designated Truth Values of XYZ
Axioms ⊨_XYZ Conjecture
iff
(des(Axioms) ∪ Exhaustion ∪ Definition) ⊨_FOL des(Conjecture)
- Proof based on isomorphism between XYZ and FOL interpretations

F	trs(F,T)	trs(F,B)	trs(F,N)	trs(F,F)

φ	φ^cT ∧ ¬φ^cF	φ^cT ∧ φ^cF	¬φ^cT ∧ ¬φ^cF	¬φ^cT ∧ φ^cF
¬φ	trs(φ,F)	trs(φ,B)	trs(φ,N)	trs(φ,T)
φ →_cmi ψ	trs(φ,N) ∨ trs(φ,F) ∨ trs(ψ,T)	(trs(φ,T) ∨ trs(φ,B)) ∧ trs(ψ,B)	(trs(φ,T) ∨ trs(φ,B)) ∧ trs(ψ,N)	(trs(φ,T) ∨ trs(φ,B)) ∧ trs(ψ,F)
∀X φ	∀X trs(φ,T)	∃X trs(φ,B ∧ ¬∃X trs(φ,F))	∃X trs(φ,N ∧ ¬∃X trs(φ,F))	∃X trs(φ,F)