Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorMarc da Costa Nunes
   • CommentTimeNov 13th 2011
   • PermaLink
   Author: Marc da Costa Nunes
   Format: TextI think I may have an alternative proof to Godel Incompletness that is quite simple. Not sure though and I'm a bit rusty on this. 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

   I think I may have an alternative proof to Godel Incompletness that is quite simple. Not sure though and I'm a bit rusty on this.
   
   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
2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeNov 14th 2011
   • (edited Nov 14th 2011)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexHi Marc, welcome to the nForum! this looks by a quick glance interesting. Without reading it (and so I can't really comment), may I make a suggestion which you are free to ignore: use [[locale]]s instead of topological spaces (or else use simplicial objects). This requires less strength in $(L,A,r)$. Also, to make things interesting, consider having excluded middle as a hypothesis, not a background assumption. This opens up the possibilities that 1) it could be removed or 2) it is essential, and therefore gives interesting examples where this result fails.

   Hi Marc, welcome to the nForum!

   this looks by a quick glance interesting. Without reading it (and so I can’t really comment), may I make a suggestion which you are free to ignore: use locales instead of topological spaces (or else use simplicial objects). This requires less strength in $(L,A,r)$. Also, to make things interesting, consider having excluded middle as a hypothesis, not a background assumption. This opens up the possibilities that 1) it could be removed or 2) it is essential, and therefore gives interesting examples where this result fails.

3. • CommentRowNumber3.
   • CommentAuthorMarc da Costa Nunes
   • CommentTimeNov 14th 2011
   • PermaLink
   Author: Marc da Costa Nunes
   Format: TextThanks a lot David. Will consider your suggestions on locals. On excluding law of excluded middle, yes, that might be interesting but in such a cash there isn't a Z2 action, there is a monoidal action of Non-negative integers by applying NOT n times. Could be interesting though. There are a number of things I wonder about in respect of how logical systems look from a categorical and then, possibly, some sort of meta-topological view. For example, a logic that admits a contradiction and for which the principle of explosion applies (for example if disjunctive syllogisms are allowed) trivially has a classifying space that is contractible to a point. It is trivial homotopically. If you relax that to include paraconsistent logics, then the space may have some...holes. I also very roughly believe that when you project the category onto the TRUE FALSE category in the way I described, you get a pair of monoids that are close to being generated by "words" in the inference rules. Anyway, I want to nail down Godel in this approach as an immediate task.

   Thanks a lot David. Will consider your suggestions on locals. On excluding law of excluded middle, yes, that might be interesting but in such a cash there isn't a Z2 action, there is a monoidal action of Non-negative integers by applying NOT n times. Could be interesting though.
   
   There are a number of things I wonder about in respect of how logical systems look from a categorical and then, possibly, some sort of meta-topological view. For example, a logic that admits a contradiction and for which the principle of explosion applies (for example if disjunctive syllogisms are allowed) trivially has a classifying space that is contractible to a point. It is trivial homotopically. If you relax that to include paraconsistent logics, then the space may have some...holes.
   
   I also very roughly believe that when you project the category onto the TRUE FALSE category in the way I described, you get a pair of monoids that are close to being generated by "words" in the inference rules.
   
   Anyway, I want to nail down Godel in this approach as an immediate task.
4. • CommentRowNumber4.
   • CommentAuthorMarc da Costa Nunes
   • CommentTimeNov 14th 2011
   • PermaLink
   Author: Marc da Costa Nunes
   Format: TextJust on the monoids generated by inference rules, if one breaks down a formal proof into "prime" elements, each on of those elements should be the application of a rule of inference. So a proof path has associated with it "word" in the inference rule alphabet. What makes this sloppy is the category I described doesn't work on propositions and specific iterations from one proposition to another via rules of inference, but, rather, equivalence classes of propositions and only the coarser arrows of provability. But there is probably something floating around in there.

   Just on the monoids generated by inference rules, if one breaks down a formal proof into "prime" elements, each on of those elements should be the application of a rule of inference. So a proof path has associated with it "word" in the inference rule alphabet. What makes this sloppy is the category I described doesn't work on propositions and specific iterations from one proposition to another via rules of inference, but, rather, equivalence classes of propositions and only the coarser arrows of provability. But there is probably something floating around in there.
5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeNov 15th 2011
   • (edited Nov 15th 2011)
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHi Marc! The idea of proving the Incompleteness theorem with group actions and topology is interesting. I haven't thought in detail about your proposal. But it's not clear to me that this outline is essentially different from the usual proof; it seems to me that the process of formalizing your statements NFP, Q, and R inside the given theory will be essentally the same as the way that logic is coded up more explicitly in the usual proof. But perhaps I am misunderstanding?

   Hi Marc! The idea of proving the Incompleteness theorem with group actions and topology is interesting. I haven’t thought in detail about your proposal. But it’s not clear to me that this outline is essentially different from the usual proof; it seems to me that the process of formalizing your statements NFP, Q, and R inside the given theory will be essentally the same as the way that logic is coded up more explicitly in the usual proof. But perhaps I am misunderstanding?

6. • CommentRowNumber6.
   • CommentAuthorMarc da Costa Nunes
   • CommentTimeNov 15th 2011
   • PermaLink
   Author: Marc da Costa Nunes
   Format: TextThanks for the welcome Mike. Yes, it could be the same thing. I do need to get through Lawvere's old paper as he talks about fixed points and Godel as well, although his result seems quite abstract.

   Thanks for the welcome Mike. Yes, it could be the same thing. I do need to get through Lawvere's old paper as he talks about fixed points and Godel as well, although his result seems quite abstract.
7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeNov 15th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex>a monoidal action of Non-negative integers by applying NOT n times In intuitionistic logic, it's a little simpler than this, since $\neg\neg\neg{p} = \neg{p}$ still. So it's an action of the $3$-element monoid of nonnegative integers modulo the relation $3 = 1$.

   a monoidal action of Non-negative integers by applying NOT n times

   In intuitionistic logic, it’s a little simpler than this, since $\neg\neg\neg{p} = \neg{p}$ still. So it’s an action of the $3$-element monoid of nonnegative integers modulo the relation $3 = 1$.

8. • CommentRowNumber8.
   • CommentAuthorDavidRoberts
   • CommentTimeNov 15th 2011
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex@Marc - I guess Mike could have pointed out as a warning the so-called topological proof of the infinitude of prime numbers ('so-called' because it uses _a_ topology, but the actual meat of the proof is still one of the classical ones, rewritten in terms of the topology). @Toby - I was going to say something similar. We have also $\neg\neg\neg\neg{p} = \neg\neg{p}$ - the double negation operator is an idempotent, but there is more structure, as you point out.

   @Marc - I guess Mike could have pointed out as a warning the so-called topological proof of the infinitude of prime numbers (’so-called’ because it uses a topology, but the actual meat of the proof is still one of the classical ones, rewritten in terms of the topology).

   @Toby - I was going to say something similar. We have also $\neg\neg\neg\neg{p} = \neg\neg{p}$ - the double negation operator is an idempotent, but there is more structure, as you point out.

9. • CommentRowNumber9.
   • CommentAuthorMarc da Costa Nunes
   • CommentTimeNov 15th 2011
   • PermaLink
   Author: Marc da Costa Nunes
   Format: TextInteresting. The monoidal action is a plain vanilla action, ie associative?

   Interesting. The monoidal action is a plain vanilla action, ie associative?
10. • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 16th 2011
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItex@Marc - yes. In fact, it can't be anything else.

    @Marc - yes. In fact, it can’t be anything else.

11. • CommentRowNumber11.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 18th 2011
    • PermaLink
    Author: Marc da Costa Nunes
    Format: Textyes, duh. I don't really need a Z2 action. NOT acts as an endofunctor and hence the statement that an inconsistency exists is still nothing more than this functor having a "fixed point". I did start to look at Lawvere's and John Bell's papers on this sort of crisp and clean categorical proof of Godel, but, I was looking for something more visual. My motivation was actually motivated by reading Penrose's crackpot books on the mind and computers ENM and SOTM. I wanted to see if the proof of Godel could be "visualized" in some sense, ie, if mathematical thinking could transcend turing machine/logical system architecture in ways that are easier to explain than a quixotic appeal to something like quantum gravity interacting with the brain. Now, under geometric realization, the endofunctor NOT becomes a continuous function. That might be too general, as of course there is much more structure. Fixed point property of the functor would imply fixed point property of the continuous function, but, is the converse true? My guess is this is true, but I haven't reflected on it much.

    yes, duh. I don't really need a Z2 action. NOT acts as an endofunctor and hence the statement that an inconsistency exists is still nothing more than this functor having a "fixed point". I did start to look at Lawvere's and John Bell's papers on this sort of crisp and clean categorical proof of Godel, but, I was looking for something more visual. My motivation was actually motivated by reading Penrose's crackpot books on the mind and computers ENM and SOTM. I wanted to see if the proof of Godel could be "visualized" in some sense, ie, if mathematical thinking could transcend turing machine/logical system architecture in ways that are easier to explain than a quixotic appeal to something like quantum gravity interacting with the brain.
    
    Now, under geometric realization, the endofunctor NOT becomes a continuous function. That might be too general, as of course there is much more structure. Fixed point property of the functor would imply fixed point property of the continuous function, but, is the converse true? My guess is this is true, but I haven't reflected on it much.
12. • CommentRowNumber12.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 18th 2011
    • PermaLink
    Author: Marc da Costa Nunes
    Format: Textsimilarly, path connectedness in this type of category means there is a sort of zig zagging (think of a childish drawing of a long winded w or m.) between objects to connect one object to another. path connectedness in this sense implies path connectedness in the continuous sense. the converse must be true, correct?

    similarly, path connectedness in this type of category means there is a sort of zig zagging (think of a childish drawing of a long winded w or m.) between objects to connect one object to another. path connectedness in this sense implies path connectedness in the continuous sense. the converse must be true, correct?
13. • CommentRowNumber13.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 20th 2011
    • (edited Nov 20th 2011)
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextOk. The condition I need on the logical system is that ¬^n=¬^m for some n, m. WLOG n>m. In such a case, I claim that if n-m is odd or equal to 2, then inconsistency means that there is a fixed point in the corresponding (continuous, but even more structure preserving) function |¬|:|C|->|C|. The case of n-m odd is actually fairly interesting geometrically. If you work out the case in which n-m is 5, you get a pentagon shape with a star inscribed that is invariant. The best I can do if n-m is even and above 2 is that inconsistency implies that there exists a subset of the 1-skeleton of |C| that is homeomorphic to the circle and that is invariant under |¬|. In fact, that subset can be visualized as an 2N-gon where (2N=n-m) and the invariance is simply a rotation of the 2N-gon so that a vertex moves to the next vertex,ie, essentially equivalent to a rotation by a certain angle. The question is whether the converse is true in the case of n-m>2 even. Odd or 2 it's obvious, at least to me.

    Ok. The condition I need on the logical system is that ¬^n=¬^m for some n, m. WLOG n>m.
    
    In such a case, I claim that if n-m is odd or equal to 2, then inconsistency means that there is a fixed point in the corresponding (continuous, but even more structure preserving) function |¬|:|C|->|C|. The case of n-m odd is actually fairly interesting geometrically. If you work out the case in which n-m is 5, you get a pentagon shape with a star inscribed that is invariant.
    
    The best I can do if n-m is even and above 2 is that inconsistency implies that there exists a subset of the 1-skeleton of |C| that is homeomorphic to the circle and that is invariant under |¬|. In fact, that subset can be visualized as an 2N-gon where (2N=n-m) and the invariance is simply a rotation of the 2N-gon so that a vertex moves to the next vertex,ie, essentially equivalent to a rotation by a certain angle.
    
    
    The question is whether the converse is true in the case of n-m>2 even. Odd or 2 it's obvious, at least to me.
14. • CommentRowNumber14.
    • CommentAuthorSridharRamesh
    • CommentTimeNov 20th 2011
    • (edited Nov 20th 2011)
    • PermaLink
    Author: SridharRamesh
    Format: MarkdownItexR is essentially the statement "Q is not provable in system A". Your theorem is "If A is consistent (and furthermore sound), then either Q is not provable in system A or Q is true". The parenthetical is because, in proving your theorem, you invoke the soundness of system A. But then there's hardly anything to this theorem; it does not seem like Goedel's incompleteness theorem. It seems like just recalling the very definition of soundness. What would be more like Goedel's (2nd) incompleteness theorem (since Q is essentially the statement "A does not prove its own consistency") would be a theorem of the form "If A is consistent, then Q is true", with both a weaker assumption and a stronger conclusion. But you haven't really sketched out how to prove this stronger statement, and it's not clear to me yet how anything would be gained from the topological formulation in doing so.

    R is essentially the statement “Q is not provable in system A”. Your theorem is “If A is consistent (and furthermore sound), then either Q is not provable in system A or Q is true”. The parenthetical is because, in proving your theorem, you invoke the soundness of system A. But then there’s hardly anything to this theorem; it does not seem like Goedel’s incompleteness theorem. It seems like just recalling the very definition of soundness.

    What would be more like Goedel’s (2nd) incompleteness theorem (since Q is essentially the statement “A does not prove its own consistency”) would be a theorem of the form “If A is consistent, then Q is true”, with both a weaker assumption and a stronger conclusion. But you haven’t really sketched out how to prove this stronger statement, and it’s not clear to me yet how anything would be gained from the topological formulation in doing so.

15. • CommentRowNumber15.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 20th 2011
    • (edited Nov 20th 2011)
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextYes, thanks. In fact my theorem is if A is sound, it isn't complete (and in fact incomplete in a way that either it can't prove its consistency or it can't prove that it cant prove its consistency). And, actually, i suppose it is in fact naively a triviality- if the system is sound and LEM applies, then either it can't prove that it can't prove its consistency or it CAN prove that it can't prove its consistency. That is, it's a triviality if it can be framed as a proposition within the context of the logical system itself. Godel represented propositions and proofs as numbers and his context was Peano Arithmetic. In my case, I wanted to represent propositions of non-provability as propositions that would be well formed statements about topological spaces, not about natural numbers. But the category of simplicial sets or possibly CW complexes (not topological spaces) is probably more suitable. Non provability in this case means that a proposition P is not contained in the same n-simplex as any element of A^ for any n. Again, I wanted to see if there were a way to "visualize" Godel. Correct that it's weaker than Godel 2. Happened upon this blog.....http://www.scottaaronson.com/blog/?p=710

    Yes, thanks. In fact my theorem is if A is sound, it isn't complete (and in fact incomplete in a way that either it can't prove its consistency or it can't prove that it cant prove its consistency). And, actually, i suppose it is in fact naively a triviality- if the system is sound and LEM applies, then either it can't prove that it can't prove its consistency or it CAN prove that it can't prove its consistency. That is, it's a triviality if it can be framed as a proposition within the context of the logical system itself. Godel represented propositions and proofs as numbers and his context was Peano Arithmetic. In my case, I wanted to represent propositions of non-provability as propositions that would be well formed statements about topological spaces, not about natural numbers. But the category of simplicial sets or possibly CW complexes (not topological spaces) is probably more suitable. Non provability in this case means that a proposition P is not contained in the same n-simplex as any element of A^ for any n.
    
    Again, I wanted to see if there were a way to "visualize" Godel.
    
    Correct that it's weaker than Godel 2.
    
    Happened upon this blog.....http://www.scottaaronson.com/blog/?p=710
16. • CommentRowNumber16.
    • CommentAuthorSridharRamesh
    • CommentTimeNov 20th 2011
    • (edited Nov 20th 2011)
    • PermaLink
    Author: SridharRamesh
    Format: MarkdownItexRegardless of whether the system is sound, if LEM applies, then either it can't prove X or it CAN prove X, for any X. I don't see why you would call this incompleteness; incompleteness normally means that (if the system is consistent/sound, then) the system both can't prove X _and_ can't prove NOT X, for some X. Or, slightly differently, the more primary form of Goedelian incompleteness is that (if the system is consistent, then) X is true _and_ the system cannot prove X, for some X. Put another way, let's look at your description "incomplete in a way that either it can't prove its consistency or it can't prove that it cant prove its consistency". This applies even to the (not effectively axiomatized, purely ideal) theory comprising all and only the true sentences of arithmetic/topology/whatever! That is, suppose you had a theory which both _could_ prove its consistency, but _couldn't_ prove (the therefore false statement that) it can't prove its consistency. Why would this be considered a form of incompleteness? I see no reason why it should be, but you seem to be doing so.

    Regardless of whether the system is sound, if LEM applies, then either it can’t prove X or it CAN prove X, for any X. I don’t see why you would call this incompleteness; incompleteness normally means that (if the system is consistent/sound, then) the system both can’t prove X and can’t prove NOT X, for some X. Or, slightly differently, the more primary form of Goedelian incompleteness is that (if the system is consistent, then) X is true and the system cannot prove X, for some X.

    Put another way, let’s look at your description “incomplete in a way that either it can’t prove its consistency or it can’t prove that it cant prove its consistency”. This applies even to the (not effectively axiomatized, purely ideal) theory comprising all and only the true sentences of arithmetic/topology/whatever! That is, suppose you had a theory which both could prove its consistency, but couldn’t prove (the therefore false statement that) it can’t prove its consistency. Why would this be considered a form of incompleteness? I see no reason why it should be, but you seem to be doing so.

17. • CommentRowNumber17.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 20th 2011
    • (edited Nov 20th 2011)
    • PermaLink
    Author: Marc da Costa Nunes
    Format: Text"Regardless of whether the system is sound, if LEM applies, then either it can't prove X or it CAN prove X, for any X." but if it weren't sound, you'd have no idea whether the proof of it proving X were proving something that is true. In any event, I was simply articulating what the original statement of the "theorem" I posted was. But as pointed out, it's fine to relax the condition of LEM in the sense that consistency still has a geometric/topological interpretation. More specifically, inconsistency has an interpretation of fixed points or at least "invariant" polytopes that live in the classifying space. suppose a->¬a and suppose ¬^(5)=Id, in other words, iterating negation 5 times brings you to the identity. then you'd have: a--->¬a<---¬¬a--->¬¬¬a<---¬¬¬¬a--->a here, the arrows mean "proves". if you look at the 1-skeleton of the associated classifying space, this is a pentagon and it is invariant under |¬|. But you can also see that there will be 2 cells that glue in etc and you will end up basically with a is the same as ¬a, ie, there is a fixed point. suppose ¬^(4)=Id. Then, a--->¬a<---¬¬a--->¬¬¬a<---a in the 1-skeleton, this is a square that is invariant under |¬|. Not obvious that one can conclude that something is fixed, but the square, which is homeomorphic to a circle, is invariant under |¬|. It makes me wonder if there is a difference between even and odd periodicity of ¬. It also doesn't matter if we have ¬^n=¬^m for some n or m. same principles apply. Again, what I'm trying to accomplish is a sort of visual approach to Godel. Maybe it doesn't work, or maybe it's been thought of before but agreed that there is still a work to do.

    "Regardless of whether the system is sound, if LEM applies, then either it can't prove X or it CAN prove X, for any X."
    
    but if it weren't sound, you'd have no idea whether the proof of it proving X were proving something that is true.
    
    In any event, I was simply articulating what the original statement of the "theorem" I posted was. But as pointed out, it's fine to relax the condition of LEM in the sense that consistency still has a geometric/topological interpretation. More specifically, inconsistency has an interpretation of fixed points or at least "invariant" polytopes that live in the classifying space. suppose a->¬a and suppose ¬^(5)=Id, in other words, iterating negation 5 times brings you to the identity. then you'd have:
    
    a--->¬a<---¬¬a--->¬¬¬a<---¬¬¬¬a--->a
    
    here, the arrows mean "proves".
    
    if you look at the 1-skeleton of the associated classifying space, this is a pentagon and it is invariant under |¬|. But you can also see that there will be 2 cells that glue in etc and you will end up basically with a is the same as ¬a, ie, there is a fixed point.
    
    suppose ¬^(4)=Id.
    
    Then,
    
    a--->¬a<---¬¬a--->¬¬¬a<---a
    
    in the 1-skeleton, this is a square that is invariant under |¬|. Not obvious that one can conclude that something is fixed, but the square, which is homeomorphic to a circle, is invariant under |¬|. It makes me wonder if there is a difference between even and odd periodicity of ¬. It also doesn't matter if we have ¬^n=¬^m for some n or m. same principles apply.
    
    Again, what I'm trying to accomplish is a sort of visual approach to Godel. Maybe it doesn't work, or maybe it's been thought of before but agreed that there is still a work to do.
18. • CommentRowNumber18.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 21st 2011
    • (edited Nov 21st 2011)
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextEdit: I did check what Godel/Lawvere et al mean by fixed points. It's different; it pertains to formulas being fixed by a function of a formula, ie f=F(f), f being some formula relating to arithmetic. I'm envisaging something different- If the system is NOT consistent, the negation functor of the logical system, under geometric realization, should at least leave some piece of the CW complex (I do recall, but I need to recheck that the classifying space is in fact a CW complex at least under certain conditions) invariant and that piece is a circle homeomorphically. Otherwise, it leaves a point fixed. I wonder whether there is some interpretation of inconsistency that could be framed topologically as the fundamental group, or the first homology group not being zero OR there existing a fixed point to some map from the space to itself. This is still a far cry from Godel 2, since my original thoughts are certainly too trivial. A thought: and this may be best placed in the Math/Philosophy section, but to what degree can topology in all of its forms with structure (all of which I suppose are right adjoints to forgetfulness), be systematized with a formal logical system? Can every proof in a very arcane subject such as Chern Simons or Floer Homology or some other topic be reduced to formal logic? Can Kirby Calculus be systemtized? perhaps as it seems computational. Can a given proof by Gromov or Thurston (two mathematicians who seem to prove things almost purely with pure geometrical arguments) be decomposed into something purely computational with a formal system? I think this is quite relevant to the whole pathos of this forum, which appears to bring together in one spot some confluence of category theory and topology. And category theory must be just a stone's throw away from logic. At the same time, I'm almost asserting the converse here- to what extent can logic be framed purely topologically? again, I'm sure it's not a totally original idea.

    Edit: I did check what Godel/Lawvere et al mean by fixed points. It's different; it pertains to formulas being fixed by a function of a formula, ie f=F(f), f being some formula relating to arithmetic. I'm envisaging something different- If the system is NOT consistent, the negation functor of the logical system, under geometric realization, should at least leave some piece of the CW complex (I do recall, but I need to recheck that the classifying space is in fact a CW complex at least under certain conditions) invariant and that piece is a circle homeomorphically. Otherwise, it leaves a point fixed. I wonder whether there is some interpretation of inconsistency that could be framed topologically as the fundamental group, or the first homology group not being zero OR there existing a fixed point to some map from the space to itself. This is still a far cry from Godel 2, since my original thoughts are certainly too trivial.
    
    A thought: and this may be best placed in the Math/Philosophy section, but to what degree can topology in all of its forms with structure (all of which I suppose are right adjoints to forgetfulness), be systematized with a formal logical system? Can every proof in a very arcane subject such as Chern Simons or Floer Homology or some other topic be reduced to formal logic? Can Kirby Calculus be systemtized? perhaps as it seems computational. Can a given proof by Gromov or Thurston (two mathematicians who seem to prove things almost purely with pure geometrical arguments) be decomposed into something purely computational with a formal system? I think this is quite relevant to the whole pathos of this forum, which appears to bring together in one spot some confluence of category theory and topology. And category theory must be just a stone's throw away from logic. At the same time, I'm almost asserting the converse here- to what extent can logic be framed purely topologically? again, I'm sure it's not a totally original idea.
19. • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 22nd 2011
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexThere are a number of things I want to address. First is that $\neg$ acts contravariantly, not covariantly. In other words, if $P$ is a Heyting algebra (whose elements $p$ we'll think of as propositions or predicates), then $\neg$ is a functor $P^{op} \to P$, not a functor $P \to P$. So the statement that there is an induced continuous function $|\neg|: |P| \to |P|$ should be clarified. It is indeed true that for any category $C$, there is a [canonical homeomorphism](http://ncatlab.org/toddtrimble/published/Nerve+of+opposite+category) $|C| \cong |C^{op}|$, ultimately due to the fact that the unit interval is interval-homeomorphic to the "opposite" topological interval (i.e., with reverse ordering), via $t \mapsto 1-t$. So what we get is a composite $$|P| \cong |P^{op}| \stackrel{|\neg|}{\to} |P|$$ but it's not at all clear to me what consequences fixed points of this _hybrid_ (i.e., this mix of logic and $t \mapsto 1-t$ stuff) would have for logic. Next, in intuitionistic logic, if $\neg^n = 1$ for any $n$, then $\neg^2 = 1$. For we have $p \leq \neg \neg p$ for any (predicate) $p$, and since $\neg$ is contravariant, we have also $\neg \neg \neg p \leq \neg p$. From these two facts, we conclude $\neg p = \neg \neg \neg p$ for all $p$, as someone said earlier. Now if $\neg$ were a bijection (as would follow from any equation of the form $\neg^n = 1$), we conclude from that last equation that $p = \neg \neg p$ for all $p$, or that $\neg^2 = 1$. It follows in particular that $n$ cannot be odd, else we reach the absurdity $\neg = 1$. Actually, maybe I'm not understanding this $\neg$ to begin with. Is it supposed to mean the negation operator on a Heyting algebra, or is it something more modal like "not provable in a formal system", or, ...? Some of the ideas outlined above look interesting to me, and most of the earlier replies have viewed the outline on a somewhat broader distance scale. This comment could be said to have to do with up-close details.

    There are a number of things I want to address. First is that $\neg$ acts contravariantly, not covariantly. In other words, if $P$ is a Heyting algebra (whose elements $p$ we’ll think of as propositions or predicates), then $\neg$ is a functor $P^{op} \to P$, not a functor $P \to P$. So the statement that there is an induced continuous function $|\neg|: |P| \to |P|$ should be clarified. It is indeed true that for any category $C$, there is a canonical homeomorphism $|C| \cong |C^{op}|$, ultimately due to the fact that the unit interval is interval-homeomorphic to the “opposite” topological interval (i.e., with reverse ordering), via $t \mapsto 1-t$. So what we get is a composite

    $$|P| \cong |P^{op}| \stackrel{|\neg|}{\to} |P|$$

    but it’s not at all clear to me what consequences fixed points of this hybrid (i.e., this mix of logic and $t \mapsto 1-t$ stuff) would have for logic.

    Next, in intuitionistic logic, if $\neg^n = 1$ for any $n$, then $\neg^2 = 1$. For we have $p \leq \neg \neg p$ for any (predicate) $p$, and since $\neg$ is contravariant, we have also $\neg \neg \neg p \leq \neg p$. From these two facts, we conclude $\neg p = \neg \neg \neg p$ for all $p$, as someone said earlier. Now if $\neg$ were a bijection (as would follow from any equation of the form $\neg^n = 1$), we conclude from that last equation that $p = \neg \neg p$ for all $p$, or that $\neg^2 = 1$. It follows in particular that $n$ cannot be odd, else we reach the absurdity $\neg = 1$.

    Actually, maybe I’m not understanding this $\neg$ to begin with. Is it supposed to mean the negation operator on a Heyting algebra, or is it something more modal like “not provable in a formal system”, or, …?

    Some of the ideas outlined above look interesting to me, and most of the earlier replies have viewed the outline on a somewhat broader distance scale. This comment could be said to have to do with up-close details.

20. • CommentRowNumber20.
    • CommentAuthorSridharRamesh
    • CommentTimeNov 22nd 2011
    • (edited Nov 22nd 2011)
    • PermaLink
    Author: SridharRamesh
    Format: MarkdownItexWell, a fixed point of that hybrid is still a proposition $p$ such that $p = \neg p$. Intuitionistically, a fixed point of that hybrid still amounts to the same thing as the presence of a contradiction (i.e., that hybrid has a fixed point if and only if $P$ is the one-element Heyting algebra). The contravariance of $\neg$ doesn't seem to me a problem for the use being made of its fixed points, but perhaps I am misunderstanding the issue which concerns you. [On edit: Oh, I see, on the topological account, there may be fixed points which are not actual propositions (and thus are of unclear significance); there could be a fixed point living somewhere in the middle of an arrow connecting two propositions. Is that the concern?] (As someone else responding to details, I am still concerned that I don't see anything in the original argument with NFP, Q, and R that has anything to do with "incompleteness". [E.g., an argument that $P$ could not be the two-element Heyting algebra])

    Well, a fixed point of that hybrid is still a proposition $p$ such that $p = \neg p$. Intuitionistically, a fixed point of that hybrid still amounts to the same thing as the presence of a contradiction (i.e., that hybrid has a fixed point if and only if $P$ is the one-element Heyting algebra). The contravariance of $\neg$ doesn’t seem to me a problem for the use being made of its fixed points, but perhaps I am misunderstanding the issue which concerns you. [On edit: Oh, I see, on the topological account, there may be fixed points which are not actual propositions (and thus are of unclear significance); there could be a fixed point living somewhere in the middle of an arrow connecting two propositions. Is that the concern?]

    (As someone else responding to details, I am still concerned that I don’t see anything in the original argument with NFP, Q, and R that has anything to do with “incompleteness”. [E.g., an argument that $P$ could not be the two-element Heyting algebra])

21. • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 22nd 2011
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex> there may be fixed points which are not actual propositions (and thus are of unclear significance); there could be a fixed point living somewhere in the middle of an arrow connecting two propositions. Is that the concern? Well, yeah. Let's take maybe the easiest possible example: the negation on the Boolean algebra $2 = \{0 \leq 1\}$, where $\neg: 2^{op} \to 2$ is an isomorphism. The geometric realization is the unit interval $I$, and the corresponding map is $t \mapsto 1-t$. There's a fixed point at $t = 1/2$. And so? To make matters slightly worse, I said there was a "canonical" order-reversing homeomorphism $I \to I$ which is used to exhibit $|C| \cong |C^{op}|$, but I lied. There is nothing, as far as I can tell, that makes the order-reversing homeomorphism $t \mapsto 1-t$ (as used on the [page](http://ncatlab.org/toddtrimble/published/Nerve+of+opposite+category) I referred to) particularly canonical, and therefore I don't see a "canonical" homeomorphism $|C| \cong |C^{op}|$. So the fixed point $t = 1/2$ above isn't particularly meaningful to me. You're right that fixed points of the underlying function $\neg: P \to P$ transfer to fixed points under $|P| \to |P|$, but that doesn't account for all of them.

    there may be fixed points which are not actual propositions (and thus are of unclear significance); there could be a fixed point living somewhere in the middle of an arrow connecting two propositions. Is that the concern?

    Well, yeah. Let’s take maybe the easiest possible example: the negation on the Boolean algebra $2 = \{0 \leq 1\}$, where $\neg: 2^{op} \to 2$ is an isomorphism. The geometric realization is the unit interval $I$, and the corresponding map is $t \mapsto 1-t$. There’s a fixed point at $t = 1/2$. And so?

    To make matters slightly worse, I said there was a “canonical” order-reversing homeomorphism $I \to I$ which is used to exhibit $|C| \cong |C^{op}|$, but I lied. There is nothing, as far as I can tell, that makes the order-reversing homeomorphism $t \mapsto 1-t$ (as used on the page I referred to) particularly canonical, and therefore I don’t see a “canonical” homeomorphism $|C| \cong |C^{op}|$. So the fixed point $t = 1/2$ above isn’t particularly meaningful to me.

    You’re right that fixed points of the underlying function $\neg: P \to P$ transfer to fixed points under $|P| \to |P|$, but that doesn’t account for all of them.

22. • CommentRowNumber22.
    • CommentAuthorSridharRamesh
    • CommentTimeNov 22nd 2011
    • (edited Nov 23rd 2011)
    • PermaLink
    Author: SridharRamesh
    Format: MarkdownItexRight, right, I understand you now. In fact, we're guaranteed fixed points in the topological setting, regardless of consistency or completeness, because, as you note, we will always have an arrow from False to True which negates into itself (and every continuous map from the unit interval to itself has a fixed point). Although I am also confused as to what exactly is being done in the topological setting: are we losing information about the directedness of arrows by regarding $C$ topologically? Or are we meant to be working with some notion of directed topological spaces? If we're going to be generalizing in this fashion, why not just work directly with the concept of categories/preorders and thus not have to worry about the idea of fixed points "within" arrows? [Full disclosure: My (slowly being written...) thesis work is on a category-theoretic account of the Goedel-Loeb modal logic of provability (including the "incompleteness" phenomena) and associated fixed point theorems]

    Right, right, I understand you now. In fact, we’re guaranteed fixed points in the topological setting, regardless of consistency or completeness, because, as you note, we will always have an arrow from False to True which negates into itself (and every continuous map from the unit interval to itself has a fixed point).

    Although I am also confused as to what exactly is being done in the topological setting: are we losing information about the directedness of arrows by regarding $C$ topologically? Or are we meant to be working with some notion of directed topological spaces? If we’re going to be generalizing in this fashion, why not just work directly with the concept of categories/preorders and thus not have to worry about the idea of fixed points “within” arrows? [Full disclosure: My (slowly being written…) thesis work is on a category-theoretic account of the Goedel-Loeb modal logic of provability (including the “incompleteness” phenomena) and associated fixed point theorems]

23. • CommentRowNumber23.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 23rd 2011
    • (edited Nov 23rd 2011)
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextThanks for the comments Todd and sorry but I'm on iPad so no proper symbols here or at least I'm too lazy to do so. Yes, understood on contravariance, I knew that but was being sloppy. I too wondered what one means with iterating NOT, ie, maybe modal is the right way to go and in fact there is a side of me that thinks the best generalization that keeps some degree of geometric/topological flavor would be that values of "truth" vary on the unit circle, ie U(1) or a subgroup thereof, and, in particular possibly a finite group of certain order. There must be some degree to which a fairly wide variety of categories arise from logical systems. Furthermore, I think a fairly wide variety of topological spaces are naturally associated with classifying spaces of categories. Take the simplest example of a circle, which arises as the geometric realization of a four point poset. add an initial object on top and you get a disk topologically. There is an obvious involution, covariant that is, which fixes the initial point and which corresponds to a rotation of the disk by pi. In that case, the fixed point is one of the objects- the initial object. But, agreed, it gets weird to think of a fixed point lying not only on the interior of a 1 simplex but how about on the interior of an n simplex. And yet, if the map left that simplex invariant, I guess by compactness and convexity there would be some point fixed and maybe not a vertex.

    Thanks for the comments Todd and sorry but I'm on iPad so no proper symbols here or at least I'm too lazy to do so. Yes, understood on contravariance, I knew that but was being sloppy. I too wondered what one means with iterating NOT, ie, maybe modal is the right way to go and in fact there is a side of me that thinks the best generalization that keeps some degree of geometric/topological flavor would be that values of "truth" vary on the unit circle, ie U(1) or a subgroup thereof, and, in particular possibly a finite group of certain order.
    
    There must be some degree to which a fairly wide variety of categories arise from logical systems. Furthermore, I think a fairly wide variety of topological spaces are naturally associated with classifying spaces of categories. Take the simplest example of a circle, which arises as the geometric realization of a four point poset. add an initial object on top and you get a disk topologically. There is an obvious involution, covariant that is, which fixes the initial point and which corresponds to a rotation of the disk by pi. In that case, the fixed point is one of the objects- the initial object. But, agreed, it gets weird to think of a fixed point lying not only on the interior of a 1 simplex but how about on the interior of an n simplex. And yet, if the map left that simplex invariant, I guess by compactness and convexity there would be some point fixed and maybe not a vertex.
24. • CommentRowNumber24.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 23rd 2011
    • (edited Nov 23rd 2011)
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextAnd to answer the question on Top, Top is certainly too general and doesn't posses enough structure. There are well known wikipedia documented facts that the image of geometric realization is better characterized as CGH. But even that might be too general. In Top, there are those who subscribe to Analog computation that would say a program or a proof is just a continuous function or perhaps a curve. It would be nice to say non provability means that P isn't in the path connected component of the axioms. But surely that would be silly; maybe P proves Q, P isn't provable, but Q is also provable from the axioms. Then P IS in the same path component as the axioms. But there might be some homology floating around here..... But I think order is important and so is combinatorics, ie, the simplicial nature of this beast is sort of closer to the original Godelian spirit. Downside is that it might reduce exactly to Godel's ideas that way, ie, natural number disguised as simplices etc.

    And to answer the question on Top, Top is certainly too general and doesn't posses enough structure. There are well known wikipedia documented facts that the image of geometric realization is better characterized as CGH. But even that might be too general. In Top, there are those who subscribe to Analog computation that would say a program or a proof is just a continuous function or perhaps a curve. It would be nice to say non provability means that P isn't in the path connected component of the axioms. But surely that would be silly; maybe P proves Q, P isn't provable, but Q is also provable from the axioms. Then P IS in the same path component as the axioms. But there might be some homology floating around here.....
    
    But I think order is important and so is combinatorics, ie, the simplicial nature of this beast is sort of closer to the original Godelian spirit. Downside is that it might reduce exactly to Godel's ideas that way, ie, natural number disguised as simplices etc.
25. • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 23rd 2011
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItex> There must be some degree to which a fairly wide variety of categories arise from logical systems. Certainly! There is a _lot_ of material out there on this; the phrase "propositions as types" refers to a sort of paradigm where structured categories (not just structured posets) correspond to various parts or fragments of logic. One basic instance of this is cartesian closed categories, seen as categorical generalizations of Heyting algebras. I'm not good at making tables, but we have basically a series of analogies * Heyting algebra: cartesian closed category * meet $a \wedge b$: cartesian product $A \times B$ * implication $a \Rightarrow b$: exponentials/internal homs $B^A$ * join $a \vee b$: coproduct $A + B$ (we'll assume our cartesian closed category has coproducts, okay?) so that a Heyting algebra, which is the algebraic concept corresponding to intuitionistic propositional logic (as Boolean algebra corresponds to clasical propositional logic), is just the posetal special case of a cartesian closed category. We can go on and interpret formal deductions in intuitionistic propositional logic as morphisms in cartesian closed categories: there is a formal semantics for doing this. People around here could talk about this stuff all day long... > There are well known wikipedia documented facts that the image of geometric realization is better characterized as CGH. Hey, you're at the nLab, where the facts are even better documented. :-) For example, check out what we have over at [[geometric realization]] (and related articles), and [[convenient category of topological spaces]] (and related articles). When you see the phrase "convenient category of spaces" around here, that's code for a cartesian closed category of spaces (like CGH) having other nice properties, and people here are very familiar with the technical convenience of such things. Speaking of logic and topological spaces, there's another big area of study under the general rubric of "domain theory". I don't think we have too much on that yet here at the Lab, but there one finds aspects of computation modeled by suitable spaces and continuous functions, so it's something you'd probably be interested in.

    There must be some degree to which a fairly wide variety of categories arise from logical systems.

    Certainly! There is a lot of material out there on this; the phrase “propositions as types” refers to a sort of paradigm where structured categories (not just structured posets) correspond to various parts or fragments of logic.

    One basic instance of this is cartesian closed categories, seen as categorical generalizations of Heyting algebras. I’m not good at making tables, but we have basically a series of analogies

    • Heyting algebra: cartesian closed category

    • meet $a \wedge b$: cartesian product $A \times B$

    • implication $a \Rightarrow b$: exponentials/internal homs $B^A$

    • join $a \vee b$: coproduct $A + B$ (we’ll assume our cartesian closed category has coproducts, okay?)

    so that a Heyting algebra, which is the algebraic concept corresponding to intuitionistic propositional logic (as Boolean algebra corresponds to clasical propositional logic), is just the posetal special case of a cartesian closed category. We can go on and interpret formal deductions in intuitionistic propositional logic as morphisms in cartesian closed categories: there is a formal semantics for doing this.

    People around here could talk about this stuff all day long…

    There are well known wikipedia documented facts that the image of geometric realization is better characterized as CGH.

    Hey, you’re at the nLab, where the facts are even better documented. :-) For example, check out what we have over at geometric realization (and related articles), and convenient category of topological spaces (and related articles). When you see the phrase “convenient category of spaces” around here, that’s code for a cartesian closed category of spaces (like CGH) having other nice properties, and people here are very familiar with the technical convenience of such things.

    Speaking of logic and topological spaces, there’s another big area of study under the general rubric of “domain theory”. I don’t think we have too much on that yet here at the Lab, but there one finds aspects of computation modeled by suitable spaces and continuous functions, so it’s something you’d probably be interested in.

26. • CommentRowNumber26.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 23rd 2011
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextHaha, yes, I am very impressed with the detailed knowledge on nLab! Thanks for the domain theory reference. Never heard of it but I'll lok it up.

    Haha, yes, I am very impressed with the detailed knowledge on nLab! Thanks for the domain theory reference. Never heard of it but I'll lok it up.
27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeNov 23rd 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItex> I'm not good at making tables, It's at [[types and logic - table]].

    I’m not good at making tables,

    It’s at types and logic - table.

28. • CommentRowNumber28.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 23rd 2011
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextYes! Heyting or orthocomplemented lattice, like in Quantum Logic. The endofunctor is selfadjoint in a sort of trivial way for classical logic at least. A more general case has that the functor's adjoint is the functor raised to an odd power. You think that's sort of a trivial adjunction or is there something interesting behind it? Maybe a homology theory? Anyway, thanks. This is a good site and i see category theory has come a long way in 20 years....

    Yes! Heyting or orthocomplemented lattice, like in Quantum Logic. The endofunctor is selfadjoint in a sort of trivial way for classical logic at least. A more general case has that the functor's adjoint is the functor raised to an odd power. You think that's sort of a trivial adjunction or is there something interesting behind it? Maybe a homology theory? Anyway, thanks. This is a good site and i see category theory has come a long way in 20 years....
29. • CommentRowNumber29.
    • CommentAuthorMarc da Costa Nunes
    • CommentTimeNov 23rd 2011
    • PermaLink
    Author: Marc da Costa Nunes
    Format: TextBut seriously, just draw a few diagrams of what inconsistency implies...it's kind of interesting. In other words, draw a simplex of implications as I mentioned above. They are polygons with an even number of sides, but just the boundary. The question is whether it makes sense to say that the vertices, all of which are propositions, are "covered" by a suitable proposition that is deemed to be true. You can always take the conjunction (todd's second bullet point) of the propositions and that will imply all of the propositions, but I think we want that to be the case only if every proposition is true. I'll try to articulate this better later, as this issue of taking "meets" of true and untrue things is sort of confusing me. Classically, those meets would be false.

    But seriously, just draw a few diagrams of what inconsistency implies...it's kind of interesting. In other words, draw a simplex of implications as I mentioned above. They are polygons with an even number of sides, but just the boundary. The question is whether it makes sense to say that the vertices, all of which are propositions, are "covered" by a suitable proposition that is deemed to be true. You can always take the conjunction (todd's second bullet point) of the propositions and that will imply all of the propositions, but I think we want that to be the case only if every proposition is true. I'll try to articulate this better later, as this issue of taking "meets" of true and untrue things is sort of confusing me. Classically, those meets would be false.