I'll leave the details of how I happened upon this to another time, and I warn that I fear this may be encapsulated in a more general form in Lawvere's work on Diagonal Arguments and Cartesian Closed Categories.

Fix a logical system (L,A, r) that has a set of axioms, rules of inference and for which (and this is a slight detour from Peano) can prove statements about a) topology and b) groups. In particular, it should handle statements concerning actions of groups on (topological spaces). As is well known, the logical system can be thought of as a category C with objects being equivalence classes of well formed statements in which statements are equivalent if they imply each other and there is an arrow between two statements if one statement can be proved from the assumption of the other. I will veer from the usual assumption of having TRUTH represent an initial object. Rather, I will assume that TRUTH is represented by the number 1 and FALSE by the number 0.

I will also assume that the Law of the Excluded Middle applies. Finally, I will assume the logical connectives AND, OR, NOT and, of course, IMPLIES. By the assumption of the LAW of the Excluded Middle, then connective NOT gives rise to an action of Z2 on the category described, sending objects P to NOT_P and reversing arrows. There is a projection Pi from C to the set {0,1} such that if P is true, then Pi(P)=1. If the logical system is consistent, then it is easy to see that there are no fixed points of C under the action of Z2 and the action Z of Z2 on C commutes with Pi as long as arithmetic is consistent as well.

If A is the set of axioms, then we denote by A^ the set of statements given by finite expressions in A involving the logical connectives AND and OR. A well formed statement P is provable iff there is a finite path a0->...->P in this category. This means provability can be expressed in terms of statements about finite paths emanating from A^ to P in C, which I believe can be re-expressed topologically, perhaps in terms of nerves/simplicial sets. We note that A^ maps to 1, ie, all statements in A^ are true by assumption.

Consider the statement NFP= there isn't a fixed point of Z on C. This statement should live in C, since the system was assumed to handle topology and groups and in particular actions of groups on topological spaces.

I also note that, of necessity, there are an infinite number of objects in C.

Consider the statement Q = there is no finite path from A^ to NFP. That means there is no proof of NFP. I also believe, but I think precision is needed, that this statement is a well formed statement within the context of the logical system, should it handle statements about topology.

Consider the statement R=there is no finite path from A^ to Q. same ideas apply as for Q.

Theorem: If the system is consistent, ie, if there are no fixed points of Z on C, then either R is true or Q is true.

proof: if R is true, we are done. If not, then it is false. If if is false, then there is a finite path a0->....->Q where a0 is in A^. Note by the assumption that the system is consistent, a0 is maps to 1, ie, it is true. Consider the image of this finite path under the involution. That image is Not_Q->.....->Not_a0. If Q were false, then Not_Q would be true. But then (and here I may need to appeal to an assumed soundness), Not_a0 would be true, which would contradict the fact that the system was assumed to be consistent.

QED.

In any event, this is a sketch and there are surely details. Let me know what you think; I am a bit rusty, but I did engage in some related topics some time ago.

Marc ]]>