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))) )