Parsing problems equality and numbers

[Jean-Luc-Picard-2021]

I can do:

a=b → f(a)=f(b) is valid. https://www.umsu.de/trees/#a=b~5f%28a%29=f%28b%29

But I cannot do:

Input 0=1 → f(0)=f(1), I then get: =01 → f(0)=f(1) is invalid. https://www.umsu.de/trees/#0=1~5f%280%29=f%281%29

But I guess its a parsing problem, because this works:

Input instead =(0,1) → f(0)=f(1), I then get 0=1 → f(0)=f(1) is valid. https://www.umsu.de/trees/#=%280,1%29~5f%280%29=f%281%29

[wo]

Officially, you're not supposed to use numerals as individual constants, because I want to allow for numerals as predicate "subscripts": P1a, P2a etc. If numerals can be constants as well as predicate subscripts, these are ambiguous. But I wonder if anyone wants to use the numerical subscripts.

[medovina]

I agree that having numerals as constants would be convenient. Given the choice, I'd probably take these over predicate subscripts.

[medovina]

Thanks for the fix! In my opinion this is a nice change.

[medovina]

Of course, it is now slightly confusing that in a countermodel the integers in the domain might not match the names of constants. For example, if I type

x = 0

then I see

x=0 is invalid.

Countermodel:
Domain: { 0, 1 }
x: 0
0: 1

It would be nicer if the system found a countermodel in which integer constants had their actual values, e.g.

x=0 is invalid.

Countermodel:
Domain: { 0, 1 }
x: 1

However, I recognize that that might be a non-trivial change.

[wo]

Hmm, right. One would have to think of a general rule. For example, if there's a premise '0=1', we can't have '0' denote 0 and '1' 1.

[medovina]

Hm - yes, that's a tricky example.

As one possible workaround, the domain in a countermodel could contain distinct values d₀, d₁ and so on, rather than integers. Then in response to

x = 0

the user might see this:

x=0 is invalid.

Countermodel: Domain: { d₀, d₁ } x: d₀ 0: d₁

You could display the countermodel elements in this way if the query includes any integer constants. Otherwise, you could just use integers as you do today.

Perhaps that would be slightly clearer than the current behavior.

[wo]

That looks like a good idea, thanks.