Changes

: ''p''(''x'', ''y'') = ''p''′(''x'')(''y'') = ''p''(''x'')′(''y'').

: ''p''(''x'', ''y'') = ''p''′(''x'')(''y'') = ''p''(''x'')′(''y'').

The "x" in p(x)'(y) would ordinarily be subscripted as a parameter in the form px', but this does not explain the difference between a parameter and a variable.  Here the difference is marked by the position of the prime ('), which serves as a kind of "run-time marker".  The prime locates the point of inflexion in a piece of notation that is the boundary between local and global responsibilities of interpretation.  It tells the intended division between individual identity of functions (a name and a local habitation) and "socially" defined roles (signs falling to the duty of a global interpreter).  In the phrase p'(x) the p' names the function while the parenthetical (x) is part of the function notation, to be understood by a global interpreter.  In p(x)' the parenthetical (x) figures into the name of an individual function, having a local significance but only when x is specified.

The "''x''" in ''p''(''x'')′(''y'') would ordinarily be subscripted as a parameter in the form ''p''_''x''′ , but this does not explain the difference between a parameter and a variable.  Here the difference is marked by the position of the prime (′), which serves as a kind of "run-time marker".  The prime locates the point of inflexion in a piece of notation that is the boundary between local and global responsibilities of interpretation.  It tells the intended division between individual identity of functions (a name and a local habitation) and "socially" defined roles (signs falling to the duty of a global interpreter).  In the phrase ''p''′(''x'') the ''p''′ names the function while the parenthetical (''x'') is part of the function notation, to be understood by a global interpreter.  In ''p''(''x'')′ the parenthetical (''x'') figures into the name of an individual function, having a local significance but only when ''x'' is specified.

I am not yet happy with my understanding of these issues.  The most general form of the question at hand appears to be bound up with the need to achieve mechanisms of functional abstraction and application for propositions.  It seems further that implementing moderate and practical forms of this functionality would have to be a major goal of the research projected here.  On the one hand Curry's paradox warns that this is a non-trivial problem, that only approximate and temporizing forms of success can reasonably be expected.  See (Lambek & Scott, 1986), but (Smullyan, chapt. 14) is probably more suitable for summer reading.  On the other hand the work of (Spencer-Brown, 1969), (Aczel, 1988), and (Barwise & Etchemendy, 1989) seems to suggest that logic can be extended to include "fixed points of negation" without disastrous results.  I can only hope that time and work will untie the mystery.

I am not yet happy with my understanding of these issues.  The most general form of the question at hand appears to be bound up with the need to achieve mechanisms of functional abstraction and application for propositions.  It seems further that implementing moderate and practical forms of this functionality would have to be a major goal of the research projected here.  On the one hand Curry's paradox warns that this is a non-trivial problem, that only approximate and temporizing forms of success can reasonably be expected.  See (Lambek & Scott, 1986), but (Smullyan, chapt. 14) is probably more suitable for summer reading.  On the other hand the work of (Spencer-Brown, 1969), (Aczel, 1988), and (Barwise & Etchemendy, 1989) seems to suggest that logic can be extended to include "fixed points of negation" without disastrous results.  I can only hope that time and work will untie the mystery.