expected quantifier syntax is not clear
rogpeppe opened this issue · 14 comments
Apologies if this is a stupid issue. I have no strong background in logic - I came here by way of the Incredible Proof Machine via a Stackoverflow question trying to explore possible solutions to a problem I was finding hard.
I was trying to re-enter Frank Hubeny's answer into proofs.openlogicproject.org, so I started by entering "¬∀x(P(x) → Q(x))" for the premise and "∃xP(x)" for the conclusion, but I always get an error popup saying "Premise 1 is not well formed".
This happens even when I copy and paste a premise from some of the examples here, which surely should work!
What am I doing wrong? Please could you fix the site so it's more obvious what the allowed syntax is - perhaps by adding an example of a premise with quantifiers expressed as text?
Thanks.
The problem with your example is that in the forall x syntax, atomic sentences don't have parentheses around arguments, i.e., it should be Px not P(x).
Don't forget to select "FOL". You'll get that error if "TFL" is selected and you have quantifiers. I assume that's the problem when you copy and paste from the sample exercises, which works for me.
I did select FOL. I still can't get the examples to work,..
Here's a screenshot to demonstrate the issue.
Ok this seems to be caused by the symReplaceNN function which converts every sequence "Ax" to "∀x" regardless of where it occurs.
Workaround: don't use A or E as predicate symbols.
Solution: disallow entering "∀x" as "Ax" and "∃x" as "Ex", and use some other easily-typable symbols for the quantifiers (eg @ and 3).
@frabjous what do you think?
Yes, that's right. Unfortunately, you cannot use A and E as predicates, since it always interprets them as ∀ and ∃. @rzach, you should probably change the syntax instructions to indicate this, since you use "A" as a predicate in one of your examples.
I'm opposed to changing this. This seems like a minor inconvenience, and using @ or something like that seems far uglier. A cleaner solution would involve doing the substitutions of A and E for ∀ and ∃ in a context-sensitive way, but this would increase the complexity of the parsing function by a significant magnitude. But if someone else wants to try, have at it!
K, leaving as is and changing instructions. Error dialog now displays the cleaned formula so should give additional hint what's wrong
6ff3795
One other naive syntax question: why is the syntax for this premise invalid?
∀x(Px→Q)
It works if Q is qualified with x, but why is that necessary?
Is it because all terms within a qualifier must be qualified with an identifier?
But this is also invalid:
(∀xPx)→Q
and Q isn't within the ∀ there.
FWIW I'm trying to express the following premise and conclusions:
(∀xPx)→Q ⊢ ∃xPx→Q
What would the correct syntax for that be in Fitch?
I fixed the FOL examples with A as a predicate in the git repo: Richard will need to make it live on the server. (Not sure how that happened: could have sword I had tested the examples!)
The book does not speak of "qualifiers" and "identifiers" but "predicates" and "subjects". The uppercase letters are predicates, and arguably predicates require subjects. Still, I guess the idea of a "zero-place" predicate is not necessarily completely unintelligible, which would basically be a statement without a subject. (I'm sure philosophers of language could have fun debating that.)
I interpreted the syntax of the language to require that all predicates have one or more subjects. But I just tried looking in the book to confirm that this is what the book authors intended, but I couldn't actually find a formal statement of the syntax. Maybe I didn't look hard enough.
I doubt it would take a lot of work to allow for zero-place predicates. (I can barely remember the code, however. I am old and forgetful.)
So I guess this is a question for the book authors: what did they intend?
The way we use parentheses, you'd need to have:
(∀xPx)→Q ⊢ ∃x(Px→Q)
With parentheses as such in the conclusion (or else it is invalid). I suspect most of the time someone would want to prove something like this, the "Q" is meant something more like a schematic metalanguage variable for any wff rather than a zero-place predicate of the object language. The checker is meant for object-language proofs only, as least is it is set up now, and "Q" simply isn't a well-formed statement of the syntax as I interpreted it.
See rzach/forallx-yyc#15 : we will allow zero-place predicate symbols. I hope to get to this before the Fall when I teach it. When that happens I'll look at he code and see if I can make that change in the proof checker. For now, you can always just use a well-formed senttence with a name that doesn't appear elsewhere, eg, Qa instead of Q.
I suppose it would be easy to add @ and 3 or somethings as additional ways for putting in quantifiers, and convert Ax to ∀x only if the input doesn't contain any other quantifier symbols. Then you can enter ∀xAx as @xax but also ∀xPx as AxPx.
For now, you can always just use a well-formed sentence with a name that doesn't appear elsewhere, eg, Qa instead of Q.
Ah, I hadn't realised that certain letters are special. When I use ∀xPx→Qa, it works but ∀xPx→Qy fails with "Premise 1 is not closed" (I'd already tried that). I don't see anything in the description that explains that there's a qualitative difference between "x" and "a" or which letters might belong to which set; perhaps that might be worth a sentence or two?
Still, I guess the idea of a "zero-place" predicate is not necessarily completely unintelligible, which would basically be a statement without a subject.
ISTM that FOL is essentially a superset of TFL, and TFL allows predicates without subjects, so it makes sense to allow them in FOL too.
BTW, by experiment, the only subject identifiers allowed are v, x, y and z.
I suppose it would be easy to add @ and 3 or somethings as additional ways for putting in quantifiers, and convert Ax to ∀x only if the input doesn't contain any other quantifier symbols. Then you can enter ∀xAx as @xax but also ∀xPx as AxPx.
I'm not sure that converting only in the absence of certain symbols is a great idea tbh. AFAICS that means that any statement that lacks quantifier symbols triggers a different grammar, which would seem potentially confusing to me.
It's not the job of the proof checker website to explain the syntax. That's the job of the book. If someone doesn't understand the difference between variables and constants when they come to use the system, they need to re-read the book, not get a tutorial on it. Things specific to the website, like how to recreate non-ASCII symbols, or why certain predicates cannot be used needs to be mentioned. But this is not the place to explain the syntax to the uninitiated.
The atomic statement letters in TFL are not "predicates without subjects". They are atomic statement letters.
Sorry if I'm getting a bit salty, but the github bug tracker is not a place to come and ask random questions because you haven't read the book.
I do notice, however, that the new version of the book uses a-r as constants and s-z as variables. I believe that's a change (?). Or did I draw the lines at the wrong places?
Firstly, thank you very much for providing both the book and the proof checker site.
It's not the job of the proof checker website to explain the syntax. That's the job of the book. If someone doesn't understand the difference between variables and constants when they come to use the system, they need to re-read the book, not get a tutorial on it.
Of course, as providers of this site, you have the freedom to make it do whatever you like, but it might be worth considering that the site is potentially providing a useful service to others that might be have come here via a different route than the book.
A link to a quick summary of the syntax would be useful for those people (I include myself in their number). Just a page number in the book might be sufficient.
For the record, from a quick skim, the relevant part of the book seems to be section 19, page 82 (Sentences of FOL). That also mentions subscripts, although it's not clear whether that's possible to do in the proof checker (also, italic font is used in the book, but presumably that's not relevant in the proof checker).
ISTM that a full short description of the allowed syntax might be useful even to those that have read the book.
One other tiny observation: when constants are introduced in section 14.2, they are "names" (the term "constant" is not used there); in section 19, the term "constant" is used (for the first time without explicitly connecting it to the "name" concept used previously). Then in section 36.1:
Names. In FOL, I have used ‘a’, ‘b’, ‘c’, for names. Some texts call these ‘constants’. Other
texts do not mark any difference between names and variables in the syntax. Those texts
focus simply on whether the symbol occurs bound or unbound.
ISTM that the text in section 14.2 could also mention the term "constant" (or the table in section 19 could mention "name").