Interpretability logic IL does not have finite subtree property
Vedran Čačić, Mladen Vuković · Hrčak Portal of scientific journals of Croatia (University Computing Centre) · 2014
Usually, when a logic has finite model property (fmp), it also has a stronger, finite submodel property: every model can be reduced to a finite submodel.Or, at least, it has a finite subtree property, which is restricted to models that are trees.We prove that interpretability logic IL does not have finite subtree property.