1st Order Logic Encoding

Encoding by Wrapping

• As done also by Fitelson
• Represent the modal theorem X by is_a_theorem(X)
• Use 1st order functors for modal connectives
• Use 1st order variables for generalizing over modal formulae
• Use 1st order ⇒ to implement modal entailment
• Use 1st order equality to implement substitution or equivalents

Some Examples

• ∀X∀Y ( ( is_a_theorem(X) & is_a_theorem(implies(X,Y)) ) ⇒ is_a_theorem(Y) )
• ∀X ( is_a_theorem(X) ⇒ is_a_theorem(□(X)) )
• ∀X ( ◊(X) = not(□(not(X))) )