Closed Jean-Luc-Picard-2021 closed 2 years ago
Thanks, this does look like a bug. I suspect the model construction doesn't assign a value to f(0) because the countermodel doesn't depend on that value. Need to look into this.
Thanks, looks much better now.
It could be that there is a small glitch in the counter model finder? Is it supposed to find counter models that are FOL models? This here gives me the following counter model:
∀x∀y(f(x)=y → (Px ∧ Qy)) → (R∧¬R) is invalid. https://www.umsu.de/trees/#~6x~6y%28f%28x%29=y~5Px~1Qy%29~5R~1~3R
But I don't think its a FOL model, because f is not total. What would be the value f(0)? On the other hand the system allows proving that function symbols are total over the universe of discourse:
∀x∃yf(x)=y is valid. https://www.umsu.de/trees/#~6x~7yf%28x%29=y
What does f={} mean, when domain={0}?