One can prove (∃xPx)→(∀xPx)

[Quelklef]

│ 1.                   assumed
├──────────
││ 2. ∃xPx             assumed
│├──────────
│││ 3. [x]             assumed
│││ 4. Px              assumed
││├──────────
││││ 5. [y]            assumed
│││├──────────
││││ 6. Px             RI:4
│││ 7. ∀xPx            ∀I:5-6[y→x]
││ 8. ∀xPx             ∃E:2,3-7
│ 9. (∃xPx)→(∀xPx)     →I:2-8

Line 7 is the erroneous one.

Related to https://github.com/Quelklef/fitch/issues/10; I think they would share a similar solution.

Not positive what that solution is, though. Something about identity of variables.

[Quelklef]

I think one solution would be to disallow ∀I[y→x] on a formula F if x is already free within F

[Quelklef]

Note that the fix https://github.com/Quelklef/fitch/commit/de84eb8bfd867aa69996e8cb12ecdda28083a9ec also disallows using variable shadowing in ∀-intro; see changes to app/Test/Edge.purs

[Quelklef]

Possible solutions:

1. when performing a ∀-intro to conclude ∀x A[a/x], x must not be free in A.
2. when performing a ∀-intro to conclude ∀x A[a/x], the chosen name variable x may not appear as a declared variable in any surrounding block
3. make the set of variables disjoint from the set of name variables
4. distinguish name variables from variables (from propositions/predicates)

Details:

In general, a ∀-intro takes the form

│ [χ]
├──────
│ ...
│ A
∀σ A[χ/σ]

Where χ and σ represent arbitrary names (the current code conflates variables and name variables).

Solution (1) disallows using ∀-intro when σ appears free in A. In the given proof, this would disallow line 7 because the chosen variable is σ=x, and x appears free in A=Pa.

This is the currently implemented solution.

Solution (2) disallows choosing a σ which is already declared in some enclosing block. In the given proof, this would disallow line 7 because the chosen variable σ=x is declared already on line 3.

I would prefer this solution over solution (1), because this solution only restricts what variable names you may choose, and variable names are contentless, anyway.

Solution (3) would be to choose a set of characters allowed to be used in declarations (i.e, name variables), and a set of characters allowed to be used in bindings (i.e., ∀/∃, i.e., non-name variables), and to make these sets disjoint. For instance, we could allow the characters a..m in declarations and n..z in bindings. Then in the given proof, this would disallow line 3 because the declared variable x is not in a..m.

This solution effectively implies solution (2). This solution also has the benefit of increasing proof readability and pedagogy by better distinguishing variables from name variables.

Solution (4) is to make the code more precise. Currently we have a single AST node Name which is used for propositions and predicates (in the literature, names) and variables in declarations (in the literature, name variables) and variables in bindings (in the literature, variables). The issue with line 7 is that, really, in the conclusion ∀xPx, the x in ∀x, which has just been introduced, is a variable, but the x in Px is a name variable, and is not the same x. So line number 7 is a valid (but not useful) conclusion with arcane semantics. If we got all these details right, the issue should go away.

[Quelklef]

Of these choices, I think I like solution (3) best. Solution (3) and solution (4) are essentially the same in nature, in that the function of both is to correctly distinguish between propositions/predicates, name variables, and variables.

Where they differ is flexibility. In order to achieve this distinguishing, solution (3) imposes restrictions on names. These restrictions are indicative of the underlying structure of how proofs work, which is good for pedagogy and readability. In other words, it's much more obvious that a variable and name variable are different if you're forced to choose from different name sets for them. On the contrary, solution (4) wants to retain full flexibility, allowing the use of the same name for a proposition/predicate, for a name variable, and for a variable. While that would be cool, it would be much more difficult to implement and much more arcane for users.

Maybe we go with solution (3) now and can explore solution (4) some other time.

[Quelklef]

Reopening this as I want to switch from solution (1), which is currently implemented, into solution (3).

[Quelklef]

I'm thinking that A..Z → proposition/predicate; a..m → name variable; n..z → variable.

Probably the most proper implementation would be to split the Name node into Var, NameVar, and Name. Then the consumers (justification algorithms) will have to be updated to look for the appropriate node.

I guess that would be like solution (4), but we use the character to infer which kind of name is intended. (Maybe I can implement an opt-in mode which tries to allow a..zA..Z for all name types, and infer what is meant in a formula.)

Also, maybe worth giving special attention to error messages here. It's not really intuitive that ∀xPx would be fine but not ∀aPa.

[Quelklef]

So, solution (4) might not be as difficult as I thought. Consider parsing the formula ∀x Pxy. We know that P is a proposition/predicate because it appears in a "function" position. We know that x is a variable because it appears in an argument position and is bound. We know that y is a name variable because it appears in an argument position and is unbound.

[Quelklef]

Also, we could prettify user input differently based on name kind. For instance, variables would become greek letters (a → α) but name variables would remain ascii.

The serialization reduced charset would have to expand. If this is done after kids are using the app, probably a new vertex should be created.

[Quelklef]

Gonna call this closed as of https://github.com/Quelklef/fitch/commit/4abd0a3234e59d2d6aa2ea5d3d8a246b545a95a2

Current solution:

1. Within the code, distinguish predicate names from name variables from variables
2. In a formula like ∀x Pxy, parse P as a predicate name, x as a variable, and y as a name variable
3. Optionally (and by default), restrict predicate names to A-Z, variable names to n-z, and name variables to a-m